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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.