# Documentation

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

# Effective epimorphisms #

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

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.

We have defined the notion of effective epi for morphisms and families of morphisms in such a way that avoids requiring the existence of pullbacks. However, if the relevant pullbacks exist then these definitions should be equivalent (project: formalize this!). See nlab: Effective Epimorphism and Stacks 00WP for the standard definitions.

## References #

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

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

Instances For
@[inline, reducible]
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.

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.

Instances For
theorem CategoryTheory.Sieve.generateSingleton_eq {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
structure CategoryTheory.EffectiveEpiStruct {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
Type (max u_1 u_2)

This structure encodes the data required for a morphism to be an effective epimorphism.

Instances For
class CategoryTheory.EffectiveEpi {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
• effectiveEpi :

A morphism f : Y ⟶ X is an effective epimorphism provided that f exhibits X as a colimit of the diagram of all "relations" R ⇉ Y. If f has a kernel pair, then this is equivalent to showing that the corresponding cofork is a colimit.

Instances
noncomputable def CategoryTheory.EffectiveEpi.getStruct {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :

Some chosen EffectiveEpiStruct associated to an effective epi.

Instances For
noncomputable def CategoryTheory.EffectiveEpi.desc {C : Type u_1} [] {X : C} {Y : C} {W : C} (f : Y X) (e : Y W) (h : ∀ {Z : C} (g₁ g₂ : Z Y), ) :
X W

Descend along an effective epi.

Instances For
@[simp]
theorem CategoryTheory.EffectiveEpi.fac_assoc {C : Type u_1} [] {X : C} {Y : C} {W : C} (f : Y X) (e : Y W) (h : ∀ {Z : C} (g₁ g₂ : Z Y), ) {Z : C} (h : W Z) :
@[simp]
theorem CategoryTheory.EffectiveEpi.fac {C : Type u_1} [] {X : C} {Y : C} {W : C} (f : Y X) (e : Y W) (h : ∀ {Z : C} (g₁ g₂ : Z Y), ) :
theorem CategoryTheory.EffectiveEpi.uniq {C : Type u_1} [] {X : C} {Y : C} {W : C} (f : Y X) (e : Y W) (h : ∀ {Z : C} (g₁ g₂ : Z Y), ) (m : X W) (hm : ) :
m = CategoryTheory.EffectiveEpi.desc f e fun {Z} => h Z
instance CategoryTheory.epiOfEffectiveEpi {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.

Instances For
noncomputable def CategoryTheory.effectiveEpiStructOfIsColimit {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.

Instances For
theorem CategoryTheory.Sieve.effectiveEpimorphic_singleton {C : Type u_1} [] {X : C} {Y : C} (f : Y X) :
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.

Instances For
theorem CategoryTheory.Sieve.generateFamily_eq {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
structure CategoryTheory.EffectiveEpiFamilyStruct {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
Type (max (max u_1 u_2) u_3)

This structure encodes the data required for a family of morphisms to be effective epimorphic.

Instances For
class CategoryTheory.EffectiveEpiFamily {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
• effectiveEpiFamily :

A family of morphisms f a : X a ⟶ B indexed by α is effective epimorphic provided that the f a exhibit B as a colimit of the diagram of all "relations" R → X a₁, R ⟶ X a₂ for all a₁ a₂ : α.

Instances
noncomputable def CategoryTheory.EffectiveEpiFamily.getStruct {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :

Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.

Instances For
noncomputable def CategoryTheory.EffectiveEpiFamily.desc {C : Type u_1} [] {B : C} {W : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (e : (a : α) → X a W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), = = ) :
B W

Descend along an effective epi family.

Instances For
@[simp]
theorem CategoryTheory.EffectiveEpiFamily.fac_assoc {C : Type u_1} [] {B : C} {W : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (e : (a : α) → X a W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), = = ) (a : α) {Z : C} (h : W Z) :
@[simp]
theorem CategoryTheory.EffectiveEpiFamily.fac {C : Type u_1} [] {B : C} {W : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (e : (a : α) → X a W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), = = ) (a : α) :
def CategoryTheory.effectiveEpiFamilyStructId {C : Type u_1} [] {α : UnitC} :

The effective epi family structure on the identity

Instances For
theorem CategoryTheory.EffectiveEpiFamily.uniq {C : Type u_1} [] {B : C} {W : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (e : (a : α) → X a W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), = = ) (m : B W) (hm : ∀ (a : α), = e a) :
theorem CategoryTheory.EffectiveEpiFamily.hom_ext {C : Type u_1} [] {B : C} {W : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (m₁ : B W) (m₂ : B W) (h : ∀ (a : α), = ) :
m₁ = m₂
instance CategoryTheory.epiCoproductDescOfEffectiveEpiFamily {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.

Instances For
noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsColimit {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.

Instances For
theorem CategoryTheory.Sieve.effectiveEpimorphic_family {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
noncomputable def CategoryTheory.EffectiveEpiFamily_descStruct {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :

Given an EffectiveEpiFamily X π such that the coproduct of X exists, Sigma.desc π is an EffectiveEpi.

Instances For
instance CategoryTheory.instEffectiveEpiSigmaObjDesc {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :
noncomputable def CategoryTheory.EffectiveEpi_familyStruct {C : Type u_1} [] {B : C} {X : C} (f : X B) :
CategoryTheory.EffectiveEpiFamilyStruct (fun x => X) fun x => match x with | PUnit.unit => f

An EffectiveEpiFamily consisting of a single EffectiveEpi

Instances For
instance CategoryTheory.instEffectiveEpiFamily {C : Type u_1} [] {B : C} {X : C} (f : X B) :
CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => match x with | PUnit.unit => f
noncomputable def CategoryTheory.EffectiveEpiFamilyStruct_of_isIso_desc {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :

A family of morphisms with the same target inducing an isomorphism from the coproduct to the target is an EffectiveEpiFamily.

Instances For
instance CategoryTheory.instEffectiveEpiFamily_1 {C : Type u_1} [] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :