Effective epimorphisms

We define the notion of effective epimorphism and effective epimorphic family of morphisms.

A morphism is an effective epi if it is a joint coequalizer of all pairs of morphisms which it coequalizes.

A family of morphisms with fixed target is effective epimorphic if it is initial among families of morphisms with its sources and a general fixed target, coequalizing every pair of morphisms it coequalizes (here, the pair of morphisms coequalized can have different targets among the sources of the 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 the file CategoryTheory/EffectiveEpi/RegularEpi.lean 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.

structure CategoryTheory.EffectiveEpiStruct {C : Type u_1} [Category.{u_2, u_1} C] {X 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), CategoryStruct.comp g₁ f = CategoryStruct.comp g₂ f → CategoryStruct.comp g₁ e = CategoryStruct.comp g₂ e) → (X ⟶ W)

  For every W with a morphism e : Y ⟶ W that coequalizes every pair of morphisms g₁ g₂ : Z ⟶ Y which f coequalizes, desc e h is a morphism X ⟶ W...

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

  ...factorizing e through f...

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

  ...and as such, unique.

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

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 (EffectiveEpiStruct f)

  f is an effective epimorphism if there exists an EffectiveEpiStruct for f.

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

Some chosen EffectiveEpiStruct associated to an effective epi.

Equations

• CategoryTheory.EffectiveEpi.getStruct f = ⋯.some

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

Descend along an effective epi.

Equations

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

@[simp]

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

@[simp]

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

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

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

structure CategoryTheory.EffectiveEpiFamilyStruct {C : Type u_1} [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₂), CategoryStruct.comp g₁ (π a₁) = CategoryStruct.comp g₂ (π a₂) → CategoryStruct.comp g₁ (e a₁) = CategoryStruct.comp g₂ (e a₂)) → (B ⟶ W)

  For every W with a family of morphisms e a : Y a ⟶ W that coequalizes every pair of morphisms g₁ : Z ⟶ Y a₁, g₂ : Z ⟶ Y a₂ which the family π coequalizes, desc e h is a morphism X ⟶ W...

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

  ...factorizing the components of e through the components of π...

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

  ...and as such, unique.

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

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

• effectiveEpiFamily : Nonempty (EffectiveEpiFamilyStruct X π)

  π is an effective epimorphic family if there exists an EffectiveEpiFamilyStruct for π

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

Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.

Equations

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

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

@[simp]

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

@[simp]

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

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

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

noncomputable def CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi {C : Type u_1} [Category.{u_2, u_1} C] {B X : C} (f : X ⟶ B) [EffectiveEpi f] : 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.

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

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

A single element EffectiveEpiFamily consists of an EffectiveEpi

Equations

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

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

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

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc {C : Type u_1} [Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [Limits.HasCoproduct X] [IsIso (Limits.Sigma.desc π)] : 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.

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

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

Any isomorphism is an effective epi.

Equations

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

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

def CategoryTheory.EffectiveEpiFamilyStruct.reindex {C : Type u_1} [Category.{u_4, u_1} C] {B : C} {α : Type u_2} {α' : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B) (e : α' ≃ α) (P : EffectiveEpiFamilyStruct (fun (a : α') => X (e a)) fun (a : α') => π (e a)) : EffectiveEpiFamilyStruct X π

Reindex the indexing type of an effective epi family struct.

Equations

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

theorem CategoryTheory.EffectiveEpiFamily.reindex {C : Type u_1} [Category.{u_4, u_1} C] {B : C} {α : Type u_2} {α' : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B) (e : α' ≃ α) (h : EffectiveEpiFamily (fun (a : α') => X (e a)) fun (a : α') => π (e a)) : EffectiveEpiFamily X π

Reindex the indexing type of an effective epi family.