Description of the covering sieves of the coherent topology #
This file characterises the covering sieves of the coherent topology.
Main result #
coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily: a sieve is a covering sieve for the coherent topology if and only if it contains a finite effective epimorphic family.
theorem
CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Precoherent C]
{X : C}
(S : CategoryTheory.Sieve X)
:
(∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
S ∈ (CategoryTheory.coherentTopology C) X
For a precoherent category, any sieve that contains an EffectiveEpiFamily is a sieve of the
coherent topology.
Note: This is one direction of mem_sieves_iff_hasEffectiveEpiFamily, but is needed for the proof.
theorem
CategoryTheory.EffectiveEpiFamily.transitive_of_finite
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Precoherent C]
{X : C}
{α : Type}
[Finite α]
{Y : α → C}
(π : (a : α) → Y a ⟶ X)
(h : CategoryTheory.EffectiveEpiFamily Y π)
{β : α → Type}
[∀ (a : α), Finite (β a)]
{Y_n : (a : α) → β a → C}
(π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a)
(H : ∀ (a : α), CategoryTheory.EffectiveEpiFamily (Y_n a) (π_n a))
:
CategoryTheory.EffectiveEpiFamily (fun (c : (a : α) × β a) => Y_n c.fst c.snd) fun (c : (a : α) × β a) =>
CategoryTheory.CategoryStruct.comp (π_n c.fst c.snd) (π c.fst)
Effective epi families in a precoherent category are transitive, in the sense that an
EffectiveEpiFamily and an EffectiveEpiFamily over each member, the composition is an
EffectiveEpiFamily.
Note: The finiteness condition is an artifact of the proof and is probably unnecessary.
instance
CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Precoherent C]
{X : C}
{α : Type}
[Finite α]
{Y Z : α → C}
(π : (a : α) → Y a ⟶ X)
[CategoryTheory.EffectiveEpiFamily Y π]
(f : (a : α) → Z a ⟶ Y a)
[h : ∀ (a : α), CategoryTheory.EffectiveEpi (f a)]
:
CategoryTheory.EffectiveEpiFamily Z fun (a : α) => CategoryTheory.CategoryStruct.comp (f a) (π a)
theorem
CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Precoherent C]
{X : C}
(S : CategoryTheory.Sieve X)
:
S ∈ (CategoryTheory.coherentTopology C) X ↔ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
A sieve belongs to the coherent topology if and only if it contains a finite
EffectiveEpiFamily.