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}
[Category.{u_2, u_1} C]
[Precoherent C]
{X : C}
(S : Sieve X)
:
(∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
S ∈ (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}
[Category.{u_2, u_1} C]
[Precoherent C]
{X : C}
{α : Type}
[Finite α]
{Y : α → C}
(π : (a : α) → Y a ⟶ X)
(h : EffectiveEpiFamily Y π)
{β : α → Type}
[∀ (a : α), Finite (β a)]
{Y_n : (a : α) → β a → C}
(π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a)
(H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a))
:
EffectiveEpiFamily (fun (c : (a : α) × β a) => Y_n c.fst c.snd) fun (c : (a : α) × β a) =>
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}
[Category.{u_2, u_1} C]
[Precoherent C]
{X : C}
{α : Type}
[Finite α]
{Y Z : α → C}
(π : (a : α) → Y a ⟶ X)
[EffectiveEpiFamily Y π]
(f : (a : α) → Z a ⟶ Y a)
[h : ∀ (a : α), EffectiveEpi (f a)]
:
EffectiveEpiFamily Z fun (a : α) => CategoryStruct.comp (f a) (π a)
theorem
CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
{C : Type u_1}
[Category.{u_2, u_1} C]
[Precoherent C]
{X : C}
(S : Sieve X)
:
S ∈ (coherentTopology C) X ↔ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
A sieve belongs to the coherent topology if and only if it contains a finite
EffectiveEpiFamily.