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 are equivalent, see effectiveEpiStructOfRegularEpi, regularEpiOfEffectiveEpi, and effectiveEpiOfKernelPair. See nlab: Effective Epimorphism and Stacks 00WP for the standard definitions. Note that our notion of EffectiveEpi is often called "strict epi" in the literature.

References #

[Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
nlab: Effective Epimorphism and
Stacks 00WP for the standard definitions.

TODO #

Find sufficient conditions on functors to preserve/reflect effective epis.

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

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

Equations

CategoryTheory.Sieve.EffectiveEpimorphic S = Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone S.arrows))

Instances For

@[inline, reducible]

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

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

Equations

CategoryTheory.Presieve.EffectiveEpimorphic S = CategoryTheory.Sieve.EffectiveEpimorphic (CategoryTheory.Sieve.generate S)

Instances For

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

CategoryTheory.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.

Equations

CategoryTheory.Sieve.generateSingleton f = { arrows := fun (Z : C) => {g : Z ⟶ X | ∃ (e : Z ⟶ Y), CategoryTheory.CategoryStruct.comp e f = g}, downward_closed := ⋯ }

Instances For

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

CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = CategoryTheory.Sieve.generateSingleton f

structure CategoryTheory.EffectiveEpiStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {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.

desc : {W : C} → (e : Y ⟶ W) → (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) → (X ⟶ W)
fac : ∀ {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e), CategoryTheory.CategoryStruct.comp f (self.desc e ⋯) = e
uniq : ∀ {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = self.desc e ⋯

Instances For

class CategoryTheory.EffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :

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.

effectiveEpi : Nonempty (CategoryTheory.EffectiveEpiStruct f)

Instances

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

CategoryTheory.EffectiveEpiStruct f

Some chosen EffectiveEpiStruct associated to an effective epi.

Equations

CategoryTheory.EffectiveEpi.getStruct f = Nonempty.some ⋯

Instances For

noncomputable def CategoryTheory.EffectiveEpi.desc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) :

X ⟶ W

Descend along an effective epi.

Equations

CategoryTheory.EffectiveEpi.desc f e h = (CategoryTheory.EffectiveEpi.getStruct f).desc e ⋯

Instances For

@[simp]

theorem CategoryTheory.EffectiveEpi.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) {Z : C} (h : W ⟶ Z) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpi.desc f e ⋯) h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem CategoryTheory.EffectiveEpi.fac {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.EffectiveEpi.desc f e ⋯) = e

theorem CategoryTheory.EffectiveEpi.uniq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) (m : X ⟶ W) (hm : CategoryTheory.CategoryStruct.comp f m = e) :

m = CategoryTheory.EffectiveEpi.desc f e ⋯

instance CategoryTheory.epiOfEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] :

CategoryTheory.Epi f

Equations

⋯ = ⋯

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

CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateSingleton f).arrows)

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} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) (Hf : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateSingleton f).arrows)) :

CategoryTheory.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.

Equations

One or more equations did not get rendered due to their size.

Instances For

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

CategoryTheory.Presieve.EffectiveEpimorphic (CategoryTheory.Presieve.singleton f) ↔ CategoryTheory.EffectiveEpi f

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

CategoryTheory.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.

Equations

CategoryTheory.Sieve.generateFamily X π = { arrows := fun (Y : C) => {f : Y ⟶ B | ∃ (a : α) (g : Y ⟶ X a), CategoryTheory.CategoryStruct.comp g (π a) = f}, downward_closed := ⋯ }

Instances For

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

CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows X π) = CategoryTheory.Sieve.generateFamily X π

structure CategoryTheory.EffectiveEpiFamilyStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {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.

desc : {W : C} → (e : (a : α) → X a ⟶ W) → (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) → (B ⟶ W)
fac : ∀ {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α), CategoryTheory.CategoryStruct.comp (π a) (self.desc e ⋯) = e a
uniq : ∀ {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = self.desc e ⋯

Instances For

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

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₂ : α.

effectiveEpiFamily : Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)

Instances

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

CategoryTheory.EffectiveEpiFamilyStruct X π

Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.

Equations

CategoryTheory.EffectiveEpiFamily.getStruct X π = Nonempty.some ⋯

Instances For

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

B ⟶ W

Descend along an effective epi family.

Equations

CategoryTheory.EffectiveEpiFamily.desc X π e h = (CategoryTheory.EffectiveEpiFamily.getStruct X π).desc e ⋯

Instances For

@[simp]

theorem CategoryTheory.EffectiveEpiFamily.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α) {Z : C} (h : W ⟶ Z) :

CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) h) = CategoryTheory.CategoryStruct.comp (e a) h

@[simp]

theorem CategoryTheory.EffectiveEpiFamily.fac {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α) :

CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) = e a

def CategoryTheory.effectiveEpiFamilyStructId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {α : Unit → C} :

CategoryTheory.EffectiveEpiFamilyStruct α fun (x : Unit) => CategoryTheory.CategoryStruct.id (α ())

The effective epi family structure on the identity

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiFamilyUnitIdToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} :

CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => CategoryTheory.CategoryStruct.id X

Equations

⋯ = ⋯

theorem CategoryTheory.EffectiveEpiFamily.uniq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (m : B ⟶ W) (hm : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) :

m = CategoryTheory.EffectiveEpiFamily.desc X π e ⋯

theorem CategoryTheory.EffectiveEpiFamily.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (m₁ : B ⟶ W) (m₂ : B ⟶ W) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m₁ = CategoryTheory.CategoryStruct.comp (π a) m₂) :

m₁ = m₂

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

CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateFamily X π).arrows)

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} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateFamily X π).arrows)) :

CategoryTheory.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.

Equations

One or more equations did not get rendered due to their size.

Instances For

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

CategoryTheory.Presieve.EffectiveEpimorphic (CategoryTheory.Presieve.ofArrows X π) ↔ CategoryTheory.EffectiveEpiFamily X π

noncomputable def CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] :

CategoryTheory.EffectiveEpiStruct (hc.desc (CategoryTheory.Limits.Cofan.mk B π))

Given an EffectiveEpiFamily X π and a corresponding coproduct cocone, the family descends to an EffectiveEpi from the coproduct.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] :

CategoryTheory.EffectiveEpiStruct (CategoryTheory.Limits.Sigma.desc π)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiSigmaObjDesc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] :

CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)

Equations

⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} {X : α → C} {π : (a : α) → X a ⟶ B} [CategoryTheory.Limits.HasCoproduct X] [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst)] {W : C} {e : (a : α) → X a ⟶ W} (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} {g₁ : Z ⟶ ∐ fun (b : α) => X b} {g₂ : Z ⟶ ∐ fun (b : α) => X b} (hg : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π)) :

CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc e) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc e)

This is an auxiliary lemma used twice in the definition of EffectiveEpiFamilyOfEffectiveEpiDesc. It is the h hypothesis of EffectiveEpi.desc and EffectiveEpi.fac.

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)] [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst)] :

CategoryTheory.EffectiveEpiFamilyStruct X π

If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of the coproduct is effective epimorphic whenever Sigma.desc induces an effective epimorphism from the coproduct itself.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpiFamilyStruct (fun (x : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f

An EffectiveEpiFamily consisting of a single EffectiveEpi

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f

Equations

⋯ = ⋯

noncomputable def CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f] :

CategoryTheory.EffectiveEpiStruct f

A single element EffectiveEpiFamily constists of an EffectiveEpi

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f] :

CategoryTheory.EffectiveEpi f

Equations

⋯ = ⋯

theorem CategoryTheory.effectiveEpi_iff_effectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) :

CategoryTheory.EffectiveEpi f ↔ CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)] :

CategoryTheory.EffectiveEpiFamilyStruct X π

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

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiFamily_1 {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)] :

CategoryTheory.EffectiveEpiFamily X π

Equations

⋯ = ⋯

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

CategoryTheory.EffectiveEpiStruct f

The identity is an effective epi.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpi_1 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

CategoryTheory.EffectiveEpi f

Equations

⋯ = ⋯

noncomputable def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) (i : X ⟶ Y) (hi : CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.id X) [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpiStruct (CategoryTheory.CategoryStruct.comp g f)

A split epi followed by an effective epi is an effective epi. This version takes an explicit section to the split epi, and is mainly used to define effectiveEpiStructCompOfEffectiveEpiSplitEpi, which takes a IsSplitEpi instance instead.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) [CategoryTheory.IsSplitEpi g] [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpiStruct (CategoryTheory.CategoryStruct.comp g f)

A split epi followed by an effective epi is an effective epi.

Equations

CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi f g = CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi' f g (Nonempty.some ⋯).section_ ⋯

Instances For

instance CategoryTheory.instEffectiveEpiCompToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) [CategoryTheory.IsSplitEpi g] [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp g f)

Equations

⋯ = ⋯

def CategoryTheory.effectiveEpiStructOfRegularEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.RegularEpi f] :

CategoryTheory.EffectiveEpiStruct f

The data of an EffectiveEpi structure on a RegularEpi.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpi_2 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.RegularEpi f] :

CategoryTheory.EffectiveEpi f

Equations

⋯ = ⋯

theorem CategoryTheory.effectiveEpiOfKernelPair {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.Limits.HasPullback f f] (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)) :

CategoryTheory.EffectiveEpi f

A morphism which is a coequalizer for its kernel pair is an effective epi.

noncomputable instance CategoryTheory.regularEpiOfEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.Limits.HasPullback f f] [CategoryTheory.EffectiveEpi f] :

CategoryTheory.RegularEpi f

An effective epi which has a kernel pair is a regular epi.

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.effectiveEpi_iff_epi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasFiniteCoproducts C] (h : ∀ {α : Type} [inst : Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B), CategoryTheory.EffectiveEpiFamily X π ↔ CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π)) {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.EffectiveEpi f ↔ CategoryTheory.Epi f

theorem CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) {B : C} {α : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B) {W : D} (ε : (a : α) → e.functor.obj (X a) ⟶ W) (h : ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)), CategoryTheory.CategoryStruct.comp g₁ (e.functor.map (π a₁)) = CategoryTheory.CategoryStruct.comp g₂ (e.functor.map (π a₂)) → CategoryTheory.CategoryStruct.comp g₁ (ε a₁) = CategoryTheory.CategoryStruct.comp g₂ (ε a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) :

CategoryTheory.CategoryStruct.comp g₁ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₁) = CategoryTheory.CategoryStruct.comp g₂ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₂)

def CategoryTheory.effectiveEpiFamilyStructOfEquivalence {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) {B : C} {α : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] :

CategoryTheory.EffectiveEpiFamilyStruct (fun (a : α) => e.functor.obj (X a)) fun (a : α) => e.functor.map (π a)

Equivalences preserve effective epimorphic families

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiFamilyObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {B : C} {α : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] :

CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)

Equations

⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (i : B ⟶ B') {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) :

CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] :

CategoryTheory.EffectiveEpiFamilyStruct X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) i

An effective epi family followed by an iso is an effective epi family.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.instEffectiveEpiFamilyCompToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] :

CategoryTheory.EffectiveEpiFamily X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) i

Equations

⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] {W : C} (e : (a : α) → Y a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (i a₁) (π a₁)) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (i a₂) (π a₂)) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) :

CategoryTheory.CategoryStruct.comp g₁ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (i a)) (e a)) a₁) = CategoryTheory.CategoryStruct.comp g₂ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (i a)) (e a)) a₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructIsoComp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] :

CategoryTheory.EffectiveEpiFamilyStruct Y fun (a : α) => CategoryTheory.CategoryStruct.comp (i a) (π a)

An effective epi family preceded by a family of isos is an effective epi family.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.effectiveEpiFamilyIsoComp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] :

CategoryTheory.EffectiveEpiFamily Y fun (a : α) => CategoryTheory.CategoryStruct.comp (i a) (π a)

Equations

⋯ = ⋯

class CategoryTheory.Functor.PreservesEffectiveEpis {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) :

A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.

preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)
A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.

Instances

instance CategoryTheory.Functor.map_effectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesEffectiveEpis F] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f] :

CategoryTheory.EffectiveEpi (F.map f)

Equations

⋯ = ⋯

instance CategoryTheory.Functor.instPreservesEffectiveEpis {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] :

CategoryTheory.Functor.PreservesEffectiveEpis F

Equations

⋯ = ⋯