Effective epimorphic sieves

We define the notion of effective epimorphic (pre)sieves and provide some API for relating the notion with the notions of effective epimorphism and effective epimorphic family.

More precisely, if f is a morphism, then f is an effective epi if and only if the sieve it generates is effective epimorphic; see CategoryTheory.Sieve.effectiveEpimorphic_singleton. The analogous statement for a family of morphisms is in the theorem CategoryTheory.Sieve.effectiveEpimorphic_family.

def CategoryTheory.Sieve.EffectiveEpimorphic {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (S : Sieve X) : Prop

A sieve is effective epimorphic if the associated cocone is a colimit cocone.

@[reducible, inline]

abbrev CategoryTheory.Presieve.EffectiveEpimorphic {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (S : Presieve X) : Prop

A presieve is effective epimorphic if the cocone associated to the sieve it generates is a colimit cocone.

def CategoryTheory.Sieve.generateSingleton {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) : Sieve X

The sieve of morphisms which factor through a given morphism f. This is equal to Sieve.generate (Presieve.singleton f), but has more convenient definitional properties.

theorem CategoryTheory.Sieve.generateSingleton_eq {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) : generate (Presieve.singleton f) = generateSingleton f

def CategoryTheory.isColimitOfEffectiveEpiStruct {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) (Hf : EffectiveEpiStruct f) : Limits.IsColimit (Sieve.generateSingleton f).arrows.cocone

Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

noncomputable def CategoryTheory.effectiveEpiStructOfIsColimit {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) (Hf : Limits.IsColimit (Sieve.generateSingleton f).arrows.cocone) : EffectiveEpiStruct f

Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

theorem CategoryTheory.Sieve.effectiveEpimorphic_singleton {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) : (Presieve.singleton f).EffectiveEpimorphic ↔ EffectiveEpi f

def CategoryTheory.Sieve.generateFamily {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) : Sieve B

The sieve of morphisms which factor through a morphism in a given family. This is equal to Sieve.generate (Presieve.ofArrows X π), but has more convenient definitional properties.

theorem CategoryTheory.Sieve.generateFamily_eq {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) : generate (Presieve.ofArrows X π) = generateFamily X π

def CategoryTheory.isColimitOfEffectiveEpiFamilyStruct {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (H : EffectiveEpiFamilyStruct X π) : Limits.IsColimit (Sieve.generateFamily X π).arrows.cocone

Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsColimit {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (H : Limits.IsColimit (Sieve.generateFamily X π).arrows.cocone) : EffectiveEpiFamilyStruct X π

Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

theorem CategoryTheory.Sieve.effectiveEpimorphic_family {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) : (Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π