# 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} [] {X : C} (S : ) :

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

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Presieve.EffectiveEpimorphic {C : Type u_1} [] {X : C} (S : ) :

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

Equations
• S.EffectiveEpimorphic = .EffectiveEpimorphic
Instances For
def CategoryTheory.Sieve.generateSingleton {C : Type u_1} [] {X : C} {Y : C} (f : Y 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.

Equations
• = { arrows := fun (Z : C) => {g : Z X | ∃ (e : Z Y), }, downward_closed := }
Instances For
theorem CategoryTheory.Sieve.generateSingleton_eq {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
def CategoryTheory.isColimitOfEffectiveEpiStruct {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.effectiveEpiStructOfIsColimit {C : Type u_1} [] {X : C} {Y : C} (f : Y X) (Hf : CategoryTheory.Limits.IsColimit .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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Sieve.effectiveEpimorphic_singleton {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
.EffectiveEpimorphic
def CategoryTheory.Sieve.generateFamily {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a 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.

Equations
• = { arrows := fun (Y : C) => {f : Y B | ∃ (a : α) (g : Y X a), = f}, downward_closed := }
Instances For
theorem CategoryTheory.Sieve.generateFamily_eq {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
def CategoryTheory.isColimitOfEffectiveEpiFamilyStruct {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsColimit {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (H : CategoryTheory.Limits.IsColimit .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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Sieve.effectiveEpimorphic_family {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
.EffectiveEpimorphic