Equalizers and coequalizers

This file defines (co)equalizers as special cases of (co)limits.

An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known from abelian groups or modules. It is a limit cone over the diagram formed by f and g.

A coequalizer is the dual concept.

Main definitions

• WalkingParallelPair is the indexing category used for (co)equalizer diagrams
• parallelPair is a functor from WalkingParallelPair to our category C.
• a fork is a cone over a parallel pair.
  • there is really only one interesting morphism in a fork: the arrow from the vertex of the fork to the domain of f and g. It is called fork.ι.
• an equalizer is now just a limit (parallelPair f g)

Each of these has a dual.

Main statements

• equalizer.ι_mono states that every equalizer map is a monomorphism
• isIso_limit_cone_parallelPair_of_self states that the identity on the domain of f is an equalizer of f and f.

Implementation notes

As with the other special shapes in the limits library, all the definitions here are given as abbrevs of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

References

• [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1]

inductive CategoryTheory.Limits.WalkingParallelPair : Type

The type of objects for the diagram indexing a (co)equalizer.

• zero : WalkingParallelPair
• one : WalkingParallelPair

@[implicit_reducible]

instance CategoryTheory.Limits.instDecidableEqWalkingParallelPair : DecidableEq WalkingParallelPair

@[implicit_reducible]

instance CategoryTheory.Limits.instInhabitedWalkingParallelPair : Inhabited WalkingParallelPair

def CategoryTheory.Limits.instInhabitedWalkingParallelPair.default : WalkingParallelPair

inductive CategoryTheory.Limits.WalkingParallelPairHom : WalkingParallelPair → WalkingParallelPair → Type

The type family of morphisms for the diagram indexing a (co)equalizer.

• left : WalkingParallelPairHom WalkingParallelPair.zero WalkingParallelPair.one
• right : WalkingParallelPairHom WalkingParallelPair.zero WalkingParallelPair.one
• id (X : WalkingParallelPair) : WalkingParallelPairHom X X

@[implicit_reducible]

instance CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom {a✝ a✝¹ : WalkingParallelPair} : DecidableEq (WalkingParallelPairHom a✝ a✝¹)

def CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom.decEq {a✝ a✝¹ : WalkingParallelPair} (x✝ x✝¹ : WalkingParallelPairHom a✝ a✝¹) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance CategoryTheory.Limits.instInhabitedWalkingParallelPairHomZeroOne : Inhabited (WalkingParallelPairHom WalkingParallelPair.zero WalkingParallelPair.one)

Satisfying the inhabited linter

def CategoryTheory.Limits.WalkingParallelPairHom.comp {X Y Z : WalkingParallelPair} : WalkingParallelPairHom X Y → WalkingParallelPairHom Y Z → WalkingParallelPairHom X Z

Composition of morphisms in the indexing diagram for (co)equalizers.

theorem CategoryTheory.Limits.WalkingParallelPairHom.id_comp {X Y : WalkingParallelPair} (g : WalkingParallelPairHom X Y) : (id X).comp g = g

theorem CategoryTheory.Limits.WalkingParallelPairHom.comp_id {X Y : WalkingParallelPair} (f : WalkingParallelPairHom X Y) : f.comp (id Y) = f

theorem CategoryTheory.Limits.WalkingParallelPairHom.assoc {X Y Z W : WalkingParallelPair} (f : WalkingParallelPairHom X Y) (g : WalkingParallelPairHom Y Z) (h : WalkingParallelPairHom Z W) : (f.comp g).comp h = f.comp (g.comp h)

@[implicit_reducible]

instance CategoryTheory.Limits.walkingParallelPairHomCategory : SmallCategory WalkingParallelPair

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairHom_id (X : WalkingParallelPair) : WalkingParallelPairHom.id X = CategoryStruct.id X

def CategoryTheory.Limits.walkingParallelPairOp : Functor WalkingParallelPair WalkingParallelPairᵒᵖ

The functor WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to right.

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOp_zero : walkingParallelPairOp.obj WalkingParallelPair.zero = Opposite.op WalkingParallelPair.one

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOp_one : walkingParallelPairOp.obj WalkingParallelPair.one = Opposite.op WalkingParallelPair.zero

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOp_left : walkingParallelPairOp.map WalkingParallelPairHom.left = Quiver.Hom.op WalkingParallelPairHom.left

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOp_right : walkingParallelPairOp.map WalkingParallelPairHom.right = Quiver.Hom.op WalkingParallelPairHom.right

def CategoryTheory.Limits.walkingParallelPairOpEquiv : WalkingParallelPair ≌ WalkingParallelPairᵒᵖ

The equivalence WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to right.

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_functor : walkingParallelPairOpEquiv.functor = walkingParallelPairOp

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_inverse : walkingParallelPairOpEquiv.inverse = walkingParallelPairOp.leftOp

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero : walkingParallelPairOpEquiv.unitIso.app WalkingParallelPair.zero = Iso.refl WalkingParallelPair.zero

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one : walkingParallelPairOpEquiv.unitIso.app WalkingParallelPair.one = Iso.refl WalkingParallelPair.one

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero : walkingParallelPairOpEquiv.counitIso.app (Opposite.op WalkingParallelPair.zero) = Iso.refl (Opposite.op WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one : walkingParallelPairOpEquiv.counitIso.app (Opposite.op WalkingParallelPair.one) = Iso.refl (Opposite.op WalkingParallelPair.one)

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero : walkingParallelPairOpEquiv.unitIso.hom.app WalkingParallelPair.zero = CategoryStruct.id WalkingParallelPair.zero

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one : walkingParallelPairOpEquiv.unitIso.hom.app WalkingParallelPair.one = CategoryStruct.id WalkingParallelPair.one

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero : walkingParallelPairOpEquiv.unitIso.inv.app WalkingParallelPair.zero = CategoryStruct.id WalkingParallelPair.zero

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one : walkingParallelPairOpEquiv.unitIso.inv.app WalkingParallelPair.one = CategoryStruct.id WalkingParallelPair.one

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero : walkingParallelPairOpEquiv.counitIso.hom.app (Opposite.op WalkingParallelPair.zero) = CategoryStruct.id (Opposite.op WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one : walkingParallelPairOpEquiv.counitIso.hom.app (Opposite.op WalkingParallelPair.one) = CategoryStruct.id (Opposite.op WalkingParallelPair.one)

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero : walkingParallelPairOpEquiv.counitIso.inv.app (Opposite.op WalkingParallelPair.zero) = CategoryStruct.id (Opposite.op WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one : walkingParallelPairOpEquiv.counitIso.inv.app (Opposite.op WalkingParallelPair.one) = CategoryStruct.id (Opposite.op WalkingParallelPair.one)

def CategoryTheory.Limits.parallelPair {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : Functor WalkingParallelPair C

parallelPair f g is the diagram in C consisting of the two morphisms f and g with common domain and codomain.

@[simp]

theorem CategoryTheory.Limits.parallelPair_obj_zero {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : (parallelPair f g).obj WalkingParallelPair.zero = X

@[simp]

theorem CategoryTheory.Limits.parallelPair_obj_one {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : (parallelPair f g).obj WalkingParallelPair.one = Y

@[simp]

theorem CategoryTheory.Limits.parallelPair_map_left {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : (parallelPair f g).map WalkingParallelPairHom.left = f

@[simp]

theorem CategoryTheory.Limits.parallelPair_map_right {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : (parallelPair f g).map WalkingParallelPairHom.right = g

@[simp]

theorem CategoryTheory.Limits.parallelPair_functor_obj {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (j : WalkingParallelPair) : (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).obj j = F.obj j

def CategoryTheory.Limits.diagramIsoParallelPair {C : Type u} [Category.{v, u} C] (F : Functor WalkingParallelPair C) : F ≅ parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)

Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a parallelPair

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelPair_hom_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingParallelPair C) (X : WalkingParallelPair) : (diagramIsoParallelPair F).hom.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelPair_inv_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingParallelPair C) (X : WalkingParallelPair) : (diagramIsoParallelPair F).inv.app X = eqToHom ⋯

def CategoryTheory.Limits.parallelPairHomMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (p : F.obj WalkingParallelPair.zero ⟶ G.obj WalkingParallelPair.zero) (q : F.obj WalkingParallelPair.one ⟶ G.obj WalkingParallelPair.one) (hl : CategoryStruct.comp (F.map WalkingParallelPairHom.left) q = CategoryStruct.comp p (G.map WalkingParallelPairHom.left) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingParallelPairHom.right) q = CategoryStruct.comp p (G.map WalkingParallelPairHom.right) := by cat_disch) : F ⟶ G

Constructor for natural transformations between parallel pairs.

@[simp]

theorem CategoryTheory.Limits.parallelPairHomMk_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (p : F.obj WalkingParallelPair.zero ⟶ G.obj WalkingParallelPair.zero) (q : F.obj WalkingParallelPair.one ⟶ G.obj WalkingParallelPair.one) (hl : CategoryStruct.comp (F.map WalkingParallelPairHom.left) q = CategoryStruct.comp p (G.map WalkingParallelPairHom.left) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingParallelPairHom.right) q = CategoryStruct.comp p (G.map WalkingParallelPairHom.right) := by cat_disch) (X✝ : WalkingParallelPair) : (parallelPairHomMk p q hl hr).app X✝ = WalkingParallelPair.casesOn X✝ p q

def CategoryTheory.Limits.parallelPairIsoMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (p : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (q : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (hl : CategoryStruct.comp (F.map WalkingParallelPairHom.left) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingParallelPairHom.right) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.right) := by cat_disch) : F ≅ G

Constructor for natural isomorphisms between parallel pairs.

@[simp]

theorem CategoryTheory.Limits.parallelPairIsoMk_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (p : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (q : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (hl : CategoryStruct.comp (F.map WalkingParallelPairHom.left) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingParallelPairHom.right) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.right) := by cat_disch) (X : WalkingParallelPair) : (parallelPairIsoMk p q hl hr).inv.app X = (WalkingParallelPair.rec p q X).inv

@[simp]

theorem CategoryTheory.Limits.parallelPairIsoMk_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (p : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (q : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (hl : CategoryStruct.comp (F.map WalkingParallelPairHom.left) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingParallelPairHom.right) q.hom = CategoryStruct.comp p.hom (G.map WalkingParallelPairHom.right) := by cat_disch) (X : WalkingParallelPair) : (parallelPairIsoMk p q hl hr).hom.app X = (WalkingParallelPair.rec p q X).hom

def CategoryTheory.Limits.parallelPairHom {C : Type u} [Category.{v, u} C] {X Y X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryStruct.comp f q = CategoryStruct.comp p f') (wg : CategoryStruct.comp g q = CategoryStruct.comp p g') : parallelPair f g ⟶ parallelPair f' g'

Construct a morphism between parallel pairs.

def CategoryTheory.Limits.parallelPairIso {C : Type u} [Category.{v, u} C] {X Y X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ≅ X') (q : Y ≅ Y') (wf : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') (wg : CategoryStruct.comp g q.hom = CategoryStruct.comp p.hom g') : parallelPair f g ≅ parallelPair f' g'

Construct a isomorphism between parallel pairs.

@[simp]

theorem CategoryTheory.Limits.parallelPairHom_app_zero {C : Type u} [Category.{v, u} C] {X Y X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryStruct.comp f q = CategoryStruct.comp p f') (wg : CategoryStruct.comp g q = CategoryStruct.comp p g') : (parallelPairHom f g f' g' p q wf wg).app WalkingParallelPair.zero = p

@[simp]

theorem CategoryTheory.Limits.parallelPairHom_app_one {C : Type u} [Category.{v, u} C] {X Y X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryStruct.comp f q = CategoryStruct.comp p f') (wg : CategoryStruct.comp g q = CategoryStruct.comp p g') : (parallelPairHom f g f' g' p q wf wg).app WalkingParallelPair.one = q

def CategoryTheory.Limits.parallelPair.ext {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (left : CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right) := by cat_disch) : F ≅ G

Construct a natural isomorphism between functors out of the walking parallel pair from its components.

@[simp]

theorem CategoryTheory.Limits.parallelPair.ext_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (left : CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right) := by cat_disch) (X : WalkingParallelPair) : (ext zero one left right).inv.app X = (WalkingParallelPair.rec zero one X).inv

@[simp]

theorem CategoryTheory.Limits.parallelPair.ext_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingParallelPair C} (zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero) (one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one) (left : CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left) := by cat_disch) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right) := by cat_disch) (X : WalkingParallelPair) : (ext zero one left right).hom.app X = (WalkingParallelPair.rec zero one X).hom

def CategoryTheory.Limits.parallelPair.eqOfHomEq {C : Type u} [Category.{v, u} C] {X Y : C} {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g') : parallelPair f g ≅ parallelPair f' g'

Construct a natural isomorphism between parallelPair f g and parallelPair f' g' given equalities f = f' and g = g'.

@[simp]

theorem CategoryTheory.Limits.parallelPair.eqOfHomEq_hom_app {C : Type u} [Category.{v, u} C] {X Y : C} {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g') (X✝ : WalkingParallelPair) : (eqOfHomEq hf hg).hom.app X✝ = (WalkingParallelPair.rec (Iso.refl X) (Iso.refl Y) X✝).hom

@[simp]

theorem CategoryTheory.Limits.parallelPair.eqOfHomEq_inv_app {C : Type u} [Category.{v, u} C] {X Y : C} {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g') (X✝ : WalkingParallelPair) : (eqOfHomEq hf hg).inv.app X✝ = (WalkingParallelPair.rec (Iso.refl X) (Iso.refl Y) X✝).inv

@[reducible, inline]

abbrev CategoryTheory.Limits.Fork {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : Type (max u v)

A fork on f and g is just a Cone (parallelPair f g).

@[reducible, inline]

abbrev CategoryTheory.Limits.Cofork {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : Type (max u v)

A cofork on f and g is just a Cocone (parallelPair f g).

def CategoryTheory.Limits.Fork.ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) : t.pt ⟶ X

A fork t on the parallel pair f g : X ⟶ Y consists of two morphisms t.π.app zero : t.pt ⟶ X and t.π.app one : t.pt ⟶ Y. Of these, only the first one is interesting, and we give it the shorter name Fork.ι t.

@[simp]

theorem CategoryTheory.Limits.Fork.app_zero_eq_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) : t.π.app WalkingParallelPair.zero = t.ι

def CategoryTheory.Limits.Cofork.π {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) : Y ⟶ t.pt

A cofork t on the parallelPair f g : X ⟶ Y consists of two morphisms t.ι.app zero : X ⟶ t.pt and t.ι.app one : Y ⟶ t.pt. Of these, only the second one is interesting, and we give it the shorter name Cofork.π t.

@[simp]

theorem CategoryTheory.Limits.Cofork.app_one_eq_π {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) : t.ι.app WalkingParallelPair.one = t.π

@[simp]

theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Fork f g) : s.π.app WalkingParallelPair.one = CategoryStruct.comp s.ι f

theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Fork f g) : s.π.app WalkingParallelPair.one = CategoryStruct.comp s.ι g

theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Fork f g) {Z : C} (h : (parallelPair f g).obj WalkingParallelPair.one ⟶ Z) : CategoryStruct.comp (s.π.app WalkingParallelPair.one) h = CategoryStruct.comp s.ι (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) : s.ι.app WalkingParallelPair.zero = CategoryStruct.comp f s.π

theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) : s.ι.app WalkingParallelPair.zero = CategoryStruct.comp g s.π

theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) {Z : C} (h : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ Z) : CategoryStruct.comp (s.ι.app WalkingParallelPair.zero) h = CategoryStruct.comp g (CategoryStruct.comp s.π h)

def CategoryTheory.Limits.Fork.ofι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) : Fork f g

A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.

@[simp]

theorem CategoryTheory.Limits.Fork.ofι_π_app {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (X✝ : WalkingParallelPair) : (ofι ι w).π.app X✝ = WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) => X✝ = t → (((Functor.const WalkingParallelPair).obj P).obj X✝ ⟶ (parallelPair f g).obj X✝)) X✝ (fun (h : X✝ = WalkingParallelPair.zero) => ⋯ ▸ ι) (fun (h : X✝ = WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp ι f) ⋯

@[simp]

theorem CategoryTheory.Limits.Fork.ofι_pt {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) : (ofι ι w).pt = P

def CategoryTheory.Limits.Cofork.ofπ {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) : Cofork f g

A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying f ≫ π = g ≫ π.

@[simp]

theorem CategoryTheory.Limits.Cofork.ofπ_pt {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) : (ofπ π w).pt = P

@[simp]

theorem CategoryTheory.Limits.Cofork.ofπ_ι_app {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (X✝ : WalkingParallelPair) : (ofπ π w).ι.app X✝ = WalkingParallelPair.casesOn X✝ (CategoryStruct.comp f π) π

@[simp]

theorem CategoryTheory.Limits.Fork.ι_ofι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) : (ofι ι w).ι = ι

@[simp]

theorem CategoryTheory.Limits.Cofork.π_ofπ {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) : (ofπ π w).π = π

theorem CategoryTheory.Limits.Fork.condition {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) : CategoryStruct.comp t.ι f = CategoryStruct.comp t.ι g

theorem CategoryTheory.Limits.Fork.condition_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp t.ι (CategoryStruct.comp f h) = CategoryStruct.comp t.ι (CategoryStruct.comp g h)

theorem CategoryTheory.Limits.Cofork.condition {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) : CategoryStruct.comp f t.π = CategoryStruct.comp g t.π

theorem CategoryTheory.Limits.Cofork.condition_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp t.π h) = CategoryStruct.comp g (CategoryStruct.comp t.π h)

theorem CategoryTheory.Limits.Fork.equalizer_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : CategoryStruct.comp k s.ι = CategoryStruct.comp l s.ι) (j : WalkingParallelPair) : CategoryStruct.comp k (s.π.app j) = CategoryStruct.comp l (s.π.app j)

To check whether two maps are equalized by both maps of a fork, it suffices to check it for the first map

theorem CategoryTheory.Limits.Cofork.coequalizer_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) {W : C} {k l : s.pt ⟶ W} (h : CategoryStruct.comp s.π k = CategoryStruct.comp s.π l) (j : WalkingParallelPair) : CategoryStruct.comp (s.ι.app j) k = CategoryStruct.comp (s.ι.app j) l

To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for the second map

theorem CategoryTheory.Limits.Fork.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} {k l : W ⟶ s.pt} (h : CategoryStruct.comp k s.ι = CategoryStruct.comp l s.ι) : k = l

theorem CategoryTheory.Limits.Cofork.IsColimit.hom_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} {k l : s.pt ⟶ W} (h : CategoryStruct.comp s.π k = CategoryStruct.comp s.π l) : k = l

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (hs : IsLimit s) : CategoryStruct.comp (hs.lift t) s.ι = t.ι

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (hs : IsLimit s) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (hs.lift t) (CategoryStruct.comp s.ι h) = CategoryStruct.comp t.ι h

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (hs : IsColimit s) : CategoryStruct.comp s.π (hs.desc t) = t.π

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (hs : IsColimit s) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp s.π (CategoryStruct.comp (hs.desc t) h) = CategoryStruct.comp t.π h

def CategoryTheory.Limits.Fork.IsLimit.lift {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : W ⟶ s.pt

If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : CategoryStruct.comp (lift hs k h) s.ι = k

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι'_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (lift hs k h) (CategoryStruct.comp s.ι h✝) = CategoryStruct.comp k h✝

def CategoryTheory.Limits.Fork.IsLimit.lift' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : { l : W ⟶ s.pt // CategoryStruct.comp l s.ι = k }

If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.

theorem CategoryTheory.Limits.Fork.IsLimit.mono {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) : Mono s.ι

def CategoryTheory.Limits.Cofork.IsColimit.desc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : s.pt ⟶ W

If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : CategoryStruct.comp s.π (desc hs k h) = k

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc'_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp s.π (CategoryStruct.comp (desc hs k h) h✝) = CategoryStruct.comp k h✝

def CategoryTheory.Limits.Cofork.IsColimit.desc' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : { l : s.pt ⟶ W // CategoryStruct.comp s.π l = k }

If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.

theorem CategoryTheory.Limits.Cofork.IsColimit.epi {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) : Epi s.π

theorem CategoryTheory.Limits.Fork.IsLimit.existsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : ∃! l : W ⟶ s.pt, CategoryStruct.comp l s.ι = k

theorem CategoryTheory.Limits.Cofork.IsColimit.existsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : ∃! d : s.pt ⟶ W, CategoryStruct.comp s.π d = k

def CategoryTheory.Limits.Fork.IsLimit.mk {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (lift : (s : Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), CategoryStruct.comp m t.ι = s.ι → m = lift s) : IsLimit t

This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.mk_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (lift : (s : Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), CategoryStruct.comp m t.ι = s.ι → m = lift s) (s : Fork f g) : (mk t lift fac uniq).lift s = lift s

def CategoryTheory.Limits.Fork.IsLimit.mk' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (create : (s : Fork f g) → { l : s.pt ⟶ t.pt // CategoryStruct.comp l t.ι = s.ι ∧ ∀ {m : s.pt ⟶ t.pt}, CategoryStruct.comp m t.ι = s.ι → m = l }) : IsLimit t

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

def CategoryTheory.Limits.Cofork.IsColimit.mk {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) (desc : (s : Cofork f g) → t.pt ⟶ s.pt) (fac : ∀ (s : Cofork f g), CategoryStruct.comp t.π (desc s) = s.π) (uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt), CategoryStruct.comp t.π m = s.π → m = desc s) : IsColimit t

This is a slightly more convenient method to verify that a cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

def CategoryTheory.Limits.Cofork.IsColimit.mk' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) (create : (s : Cofork f g) → { l : t.pt ⟶ s.pt // CategoryStruct.comp t.π l = s.π ∧ ∀ {m : t.pt ⟶ s.pt}, CategoryStruct.comp t.π m = s.π → m = l }) : IsColimit t

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

noncomputable def CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (hs : ∀ (s : Fork f g), ∃! l : s.pt ⟶ t.pt, CategoryStruct.comp l t.ι = s.ι) : IsLimit t

Noncomputably make a limit cone from the existence of unique factorizations.

noncomputable def CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (hs : ∀ (s : Cofork f g), ∃! d : t.pt ⟶ s.pt, CategoryStruct.comp t.π d = s.π) : IsColimit t

Noncomputably make a colimit cocone from the existence of unique factorizations.

def CategoryTheory.Limits.Fork.IsLimit.homIso {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) : (Z ⟶ t.pt) ≃ { h : Z ⟶ X // CategoryStruct.comp h f = CategoryStruct.comp h g }

Given a limit cone for the pair f g : X ⟶ Y, for any Z, morphisms from Z to its point are in bijection with morphisms h : Z ⟶ X such that h ≫ f = h ≫ g. Further, this bijection is natural in Z: see Fork.IsLimit.homIso_natural. This is a special case of IsLimit.homIso', often useful to construct adjunctions.

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) (h : { h : Z ⟶ X // CategoryStruct.comp h f = CategoryStruct.comp h g }) : (homIso ht Z).symm h = ↑(lift' ht ↑h ⋯)

@[simp]

theorem CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) (k : Z ⟶ t.pt) : ↑((homIso ht Z) k) = CategoryStruct.comp k t.ι

theorem CategoryTheory.Limits.Fork.IsLimit.homIso_natural {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) : ↑((homIso ht Z') (CategoryStruct.comp q k)) = CategoryStruct.comp q ↑((homIso ht Z) k)

The bijection of Fork.IsLimit.homIso is natural in Z.

def CategoryTheory.Limits.Cofork.IsColimit.homIso {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) : (t.pt ⟶ Z) ≃ { h : Y ⟶ Z // CategoryStruct.comp f h = CategoryStruct.comp g h }

Given a colimit cocone for the pair f g : X ⟶ Y, for any Z, morphisms from the cocone point to Z are in bijection with morphisms h : Y ⟶ Z such that f ≫ h = g ≫ h. Further, this bijection is natural in Z: see Cofork.IsColimit.homIso_natural. This is a special case of IsColimit.homIso', often useful to construct adjunctions.

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) (h : { h : Y ⟶ Z // CategoryStruct.comp f h = CategoryStruct.comp g h }) : (homIso ht Z).symm h = ↑(desc' ht ↑h ⋯)

@[simp]

theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) (k : t.pt ⟶ Z) : ↑((homIso ht Z) k) = CategoryStruct.comp t.π k

theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_natural {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} {Z Z' : C} (q : Z ⟶ Z') (ht : IsColimit t) (k : t.pt ⟶ Z) : ↑((homIso ht Z') (CategoryStruct.comp k q)) = CategoryStruct.comp (↑((homIso ht Z) k)) q

The bijection of Cofork.IsColimit.homIso is natural in Z.

def CategoryTheory.Limits.Cone.ofFork {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Fork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) : Cone F

This is a helper construction that can be useful when verifying that a category has all equalizers. Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right), and a fork on F.map left and F.map right, we get a cone on F.

If you're thinking about using this, have a look at hasEqualizers_of_hasLimit_parallelPair, which you may find to be an easier way of achieving your goal.

def CategoryTheory.Limits.Cocone.ofCofork {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) : Cocone F

This is a helper construction that can be useful when verifying that a category has all coequalizers. Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right), and a cofork on F.map left and F.map right, we get a cocone on F.

If you're thinking about using this, have a look at hasCoequalizers_of_hasColimit_parallelPair, which you may find to be an easier way of achieving your goal.

@[simp]

theorem CategoryTheory.Limits.Cone.ofFork_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Fork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) (j : WalkingParallelPair) : (ofFork t).π.app j = CategoryStruct.comp (t.π.app j) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.Limits.Cocone.ofCofork_ι {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) (j : WalkingParallelPair) : (ofCofork t).ι.app j = CategoryStruct.comp (eqToHom ⋯) (t.ι.app j)

def CategoryTheory.Limits.Fork.ofCone {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cone F) : Fork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)

Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right) and a cone on F, we get a fork on F.map left and F.map right.

def CategoryTheory.Limits.Cofork.ofCocone {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cocone F) : Cofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)

Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right) and a cocone on F, we get a cofork on F.map left and F.map right.

@[simp]

theorem CategoryTheory.Limits.Fork.ofCone_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cone F) (j : WalkingParallelPair) : (ofCone t).π.app j = CategoryStruct.comp (t.π.app j) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.Limits.Cofork.ofCocone_ι {C : Type u} [Category.{v, u} C] {F : Functor WalkingParallelPair C} (t : Cocone F) (j : WalkingParallelPair) : (ofCocone t).ι.app j = CategoryStruct.comp (eqToHom ⋯) (t.ι.app j)

@[simp]

theorem CategoryTheory.Limits.Fork.ι_postcompose {C : Type u} [Category.{v, u} C] {X Y : C} {f g f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parallelPair f' g'} {c : Fork f g} : ι ((Cone.postcompose α).obj c) = CategoryStruct.comp c.ι (α.app WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.Cofork.π_precompose {C : Type u} [Category.{v, u} C] {X Y : C} {f g f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parallelPair f' g'} {c : Cofork f' g'} : π ((Cocone.precompose α).obj c) = CategoryStruct.comp (α.app WalkingParallelPair.one) c.π

def CategoryTheory.Limits.Fork.mkHom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (k : s.pt ⟶ t.pt) (w : CategoryStruct.comp k t.ι = s.ι) : s ⟶ t

Helper function for constructing morphisms between equalizer forks.

@[simp]

theorem CategoryTheory.Limits.Fork.mkHom_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (k : s.pt ⟶ t.pt) (w : CategoryStruct.comp k t.ι = s.ι) : (mkHom k w).hom = k

def CategoryTheory.Limits.Fork.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : s ≅ t

To construct an isomorphism between forks, it suffices to give an isomorphism between the cone points and check that it commutes with the ι morphisms.

@[simp]

theorem CategoryTheory.Limits.Fork.ext_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (ext i w).inv = mkHom i.inv ⋯

@[simp]

theorem CategoryTheory.Limits.Fork.ext_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (ext i w).hom = mkHom i.hom w

def CategoryTheory.Limits.ForkOfι.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} {ι ι' : P ⟶ X} (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (w' : CategoryStruct.comp ι' f = CategoryStruct.comp ι' g) (h : ι = ι') : Fork.ofι ι w ≅ Fork.ofι ι' w'

Two forks of the form ofι are isomorphic whenever their ι's are equal.

def CategoryTheory.Limits.Fork.isoForkOfι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c ≅ ofι c.ι ⋯

Every fork is isomorphic to one of the form Fork.of_ι _ _.

@[simp]

theorem CategoryTheory.Limits.Fork.isoForkOfι_hom_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.isoForkOfι.hom.hom = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.Fork.isoForkOfι_inv_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.isoForkOfι.inv.hom = CategoryStruct.id c.pt

def CategoryTheory.Limits.Fork.equivOfIsos {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) : Fork f g ≌ Fork f' g'

If f, g : X ⟶ Y and f', g : X' ⟶ Y' pairwise form a commutative square with isomorphisms X ≅ X' and Y ≅ Y', the categories of forks are equivalent.

@[simp]

theorem CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (c : Fork f g) : ((equivOfIsos e₀ e₁ comm₁ comm₂).functor.obj c).ι = CategoryStruct.comp c.ι e₀.hom

@[simp]

theorem CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (c : Fork f' g') : ((equivOfIsos e₀ e₁ comm₁ comm₂).inverse.obj c).ι = CategoryStruct.comp c.ι e₀.inv

def CategoryTheory.Limits.Fork.isLimitEquivOfIsos {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} (c : Fork f g) {f' g' : X' ⟶ Y'} (c' : Fork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryStruct.comp e.hom c'.ι = CategoryStruct.comp c.ι e₀.hom := by cat_disch) : IsLimit c ≃ IsLimit c'

Given two forks with isomorphic components in such a way that the natural diagrams commute, then one is a limit if and only if the other one is.

def CategoryTheory.Limits.Fork.isLimitOfIsos {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} (c : Fork f g) (hc : IsLimit c) {f' g' : X' ⟶ Y'} (c' : Fork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryStruct.comp e.hom c'.ι = CategoryStruct.comp c.ι e₀.hom := by cat_disch) : IsLimit c'

Given two forks with isomorphic components in such a way that the natural diagrams commute, then if one is a limit, then the other one is as well.

def CategoryTheory.Limits.Cofork.mkHom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (k : s.pt ⟶ t.pt) (w : CategoryStruct.comp s.π k = t.π) : s ⟶ t

Helper function for constructing morphisms between coequalizer coforks.

@[simp]

theorem CategoryTheory.Limits.Cofork.mkHom_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (k : s.pt ⟶ t.pt) (w : CategoryStruct.comp s.π k = t.π) : (mkHom k w).hom = k

@[simp]

theorem CategoryTheory.Limits.Fork.hom_comp_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (f✝ : s ⟶ t) : CategoryStruct.comp f✝.hom t.ι = s.ι

@[simp]

theorem CategoryTheory.Limits.Fork.hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Fork f g} (f✝ : s ⟶ t) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp f✝.hom (CategoryStruct.comp t.ι h) = CategoryStruct.comp s.ι h

@[simp]

theorem CategoryTheory.Limits.Fork.π_comp_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (f✝ : s ⟶ t) : CategoryStruct.comp s.π f✝.hom = t.π

@[simp]

theorem CategoryTheory.Limits.Fork.π_comp_hom_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (f✝ : s ⟶ t) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp s.π (CategoryStruct.comp f✝.hom h) = CategoryStruct.comp t.π h

def CategoryTheory.Limits.Cofork.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp s.π i.hom = t.π := by cat_disch) : s ≅ t

To construct an isomorphism between coforks, it suffices to give an isomorphism between the cocone points and check that it commutes with the π morphisms.

@[simp]

theorem CategoryTheory.Limits.Cofork.ext_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp s.π i.hom = t.π := by cat_disch) : (ext i w).inv = mkHom i.inv ⋯

@[simp]

theorem CategoryTheory.Limits.Cofork.ext_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : Cofork f g} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp s.π i.hom = t.π := by cat_disch) : (ext i w).hom = mkHom i.hom w

def CategoryTheory.Limits.CoforkOfπ.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {P : C} {π π' : Y ⟶ P} (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (w' : CategoryStruct.comp f π' = CategoryStruct.comp g π') (h : π = π') : Cofork.ofπ π w ≅ Cofork.ofπ π' w'

Two coforks of the form ofπ are isomorphic whenever their π's are equal.

def CategoryTheory.Limits.Cofork.isoCoforkOfπ {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (c : Cofork f g) : c ≅ ofπ c.π ⋯

Every cofork is isomorphic to one of the form Cofork.ofπ _ _.

def CategoryTheory.Limits.Cofork.isColimitEquivOfIsos {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} (c : Cofork f g) {f' g' : X' ⟶ Y'} (c' : Cofork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryStruct.comp e₁.inv (CategoryStruct.comp c.π e.hom) = c'.π := by cat_disch) : IsColimit c ≃ IsColimit c'

Given two coforks with isomorphic components in such a way that the natural diagrams commute, then one is a colimit if and only if the other one is.

def CategoryTheory.Limits.Cofork.isColimitOfIsos {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} (c : Cofork f g) (hc : IsColimit c) {f' g' : X' ⟶ Y'} (c' : Cofork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryStruct.comp e₁.inv (CategoryStruct.comp c.π e.hom) = c'.π := by cat_disch) : IsColimit c'

Given two coforks with isomorphic components in such a way that the natural diagrams commute, then if one is a colimit, then the other one is as well.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : Prop

Two parallel morphisms f and g have an equalizer if the diagram parallelPair f g has a limit.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.equalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : C

If an equalizer of f and g exists, we can access an arbitrary choice of such by saying equalizer f g.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.equalizer.ι {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : equalizer f g ⟶ X

If an equalizer of f and g exists, we can access the inclusion equalizer f g ⟶ X by saying equalizer.ι f g.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.equalizer.fork {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : Fork f g

An equalizer cone for a parallel pair f and g

@[simp]

theorem CategoryTheory.Limits.equalizer.fork_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : (fork f g).ι = ι f g

@[simp]

theorem CategoryTheory.Limits.equalizer.fork_π_app_zero {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : (fork f g).π.app WalkingParallelPair.zero = ι f g

theorem CategoryTheory.Limits.equalizer.condition {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : CategoryStruct.comp (ι f g) f = CategoryStruct.comp (ι f g) g

theorem CategoryTheory.Limits.equalizer.condition_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (ι f g) (CategoryStruct.comp f h) = CategoryStruct.comp (ι f g) (CategoryStruct.comp g h)

noncomputable def CategoryTheory.Limits.equalizerIsEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : IsLimit (Fork.ofι (equalizer.ι f g) ⋯)

The equalizer built from equalizer.ι f g is limiting.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.equalizer.lift {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : W ⟶ equalizer f g

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the equalizer of f and g via equalizer.lift : W ⟶ equalizer f g.

theorem CategoryTheory.Limits.equalizer.lift_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : CategoryStruct.comp (lift k h) (ι f g) = k

theorem CategoryTheory.Limits.equalizer.lift_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (lift k h) (CategoryStruct.comp (ι f g) h✝) = CategoryStruct.comp k h✝

noncomputable def CategoryTheory.Limits.equalizer.lift' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : { l : W ⟶ equalizer f g // CategoryStruct.comp l (ι f g) = k }

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ equalizer f g satisfying l ≫ equalizer.ι f g = k.

theorem CategoryTheory.Limits.equalizer.hom_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} {k l : W ⟶ equalizer f g} (h : CategoryStruct.comp k (ι f g) = CategoryStruct.comp l (ι f g)) : k = l

Two maps into an equalizer are equal if they are equal when composed with the equalizer map.

theorem CategoryTheory.Limits.equalizer.hom_ext_iff {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} {k l : W ⟶ equalizer f g} : k = l ↔ CategoryStruct.comp k (ι f g) = CategoryStruct.comp l (ι f g)

theorem CategoryTheory.Limits.equalizer.existsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = CategoryStruct.comp k g) : ∃! l : W ⟶ equalizer f g, CategoryStruct.comp l (ι f g) = k

instance CategoryTheory.Limits.equalizer.ι_mono {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] : Mono (ι f g)

An equalizer morphism is a monomorphism

theorem CategoryTheory.Limits.mono_of_isLimit_fork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Fork f g} (i : IsLimit c) : Mono c.ι

The equalizer morphism in any limit cone is a monomorphism.

def CategoryTheory.Limits.idFork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h : f = g) : Fork f g

The identity determines a cone on the equalizer diagram of f and g if f = g.

def CategoryTheory.Limits.isLimitIdFork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h : f = g) : IsLimit (idFork h)

The identity on X is an equalizer of (f, g), if f = g.

theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h₀ : f = g) {c : Fork f g} (h : IsLimit c) : IsIso c.ι

Every equalizer of (f, g), where f = g, is an isomorphism.

theorem CategoryTheory.Limits.equalizer.ι_of_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] (h : f = g) : IsIso (ι f g)

The equalizer of (f, g), where f = g, is an isomorphism.

theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {c : Fork f f} (h : IsLimit c) : IsIso c.ι

Every equalizer of (f, f) is an isomorphism.

theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Fork f g} (h : IsLimit c) [Epi c.ι] : IsIso c.ι

An equalizer that is an epimorphism is an isomorphism.

theorem CategoryTheory.Limits.eq_of_epi_fork_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Fork f g) [Epi t.ι] : f = g

Two morphisms are equal if there is a fork whose inclusion is epi.

theorem CategoryTheory.Limits.eq_of_epi_equalizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g] [Epi (equalizer.ι f g)] : f = g

If the equalizer of two morphisms is an epimorphism, then the two morphisms are equal.

instance CategoryTheory.Limits.hasEqualizer_of_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : HasEqualizer f f

instance CategoryTheory.Limits.equalizer.ι_of_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : IsIso (ι f f)

The equalizer inclusion for (f, f) is an isomorphism.

noncomputable def CategoryTheory.Limits.equalizer.isoSourceOfSelf {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : equalizer f f ≅ X

The equalizer of a morphism with itself is isomorphic to the source.

@[simp]

theorem CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : (isoSourceOfSelf f).hom = ι f f

@[simp]

theorem CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : (isoSourceOfSelf f).inv = lift (CategoryStruct.id X) ⋯

def CategoryTheory.Limits.precompFork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) (s : Fork f g) (c : PullbackCone s.ι h) : Fork (CategoryStruct.comp h f) (CategoryStruct.comp h g)

Given a fork s on morphisms f, g : X ⟶ Y and a pullback cone c on s.ι : s.pt ⟶ X and a morphism h : Z ⟶ X, the projection c.snd : c.pt ⟶ Z induces a fork on h ≫ f and h ≫ g.

c.pt → Z
|      |
v      v
s.pt → X ⇉ Y

def CategoryTheory.Limits.liftPrecomp {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) {s : Fork f g} (hs : IsLimit s) {c : PullbackCone s.ι h} (hc : IsLimit c) (s' : Fork (CategoryStruct.comp h f) (CategoryStruct.comp h g)) : s'.pt ⟶ (precompFork h s c).pt

Any fork on h ≫ f and h ≫ g lifts to a pullback along h of an equalizer of f and g.

def CategoryTheory.Limits.isLimitPrecompFork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) {s : Fork f g} (hs : IsLimit s) {c : PullbackCone s.ι h} (hc : IsLimit c) : IsLimit (precompFork h s c)

The pullback of an equalizer is an equalizer.

theorem CategoryTheory.Limits.hasEqualizer_precomp_of_equalizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) {s : Fork f g} (hs : IsLimit s) {c : PullbackCone s.ι h} (hc : IsLimit c) : HasEqualizer (CategoryStruct.comp h f) (CategoryStruct.comp h g)

instance CategoryTheory.Limits.hasEqualizer_precomp_of_hasEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) [HasEqualizer f g] [HasPullback (equalizer.ι f g) h] : HasEqualizer (CategoryStruct.comp h f) (CategoryStruct.comp h g)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoequalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) : Prop

Two parallel morphisms f and g have a coequalizer if the diagram parallelPair f g has a colimit.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coequalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : C

If a coequalizer of f and g exists, we can access an arbitrary choice of such by saying coequalizer f g.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coequalizer.π {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : Y ⟶ coequalizer f g

If a coequalizer of f and g exists, we can access the corresponding projection by saying coequalizer.π f g.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coequalizer.cofork {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : Cofork f g

An arbitrary choice of coequalizer cocone for a parallel pair f and g.

@[simp]

theorem CategoryTheory.Limits.coequalizer.cofork_π {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : (cofork f g).π = π f g

theorem CategoryTheory.Limits.coequalizer.cofork_ι_app_one {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : (cofork f g).ι.app WalkingParallelPair.one = π f g

theorem CategoryTheory.Limits.coequalizer.condition {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : CategoryStruct.comp f (π f g) = CategoryStruct.comp g (π f g)

theorem CategoryTheory.Limits.coequalizer.condition_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] {Z : C} (h : coequalizer f g ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (π f g) h) = CategoryStruct.comp g (CategoryStruct.comp (π f g) h)

noncomputable def CategoryTheory.Limits.coequalizerIsCoequalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] : IsColimit (Cofork.ofπ (coequalizer.π f g) ⋯)

The cofork built from coequalizer.π f g is colimiting.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coequalizer.desc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : coequalizer f g ⟶ W

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k factors through the coequalizer of f and g via coequalizer.desc : coequalizer f g ⟶ W.

theorem CategoryTheory.Limits.coequalizer.π_desc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : CategoryStruct.comp (π f g) (desc k h) = k

theorem CategoryTheory.Limits.coequalizer.π_desc_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp (π f g) (CategoryStruct.comp (desc k h) h✝) = CategoryStruct.comp k h✝

theorem CategoryTheory.Limits.coequalizer.π_colimMap_desc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g'] (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryStruct.comp f q = CategoryStruct.comp p f') (wg : CategoryStruct.comp g q = CategoryStruct.comp p g') (h : Y' ⟶ Z) (wh : CategoryStruct.comp f' h = CategoryStruct.comp g' h) : CategoryStruct.comp (π f g) (CategoryStruct.comp (colimMap (parallelPairHom f g f' g' p q wf wg)) (desc h wh)) = CategoryStruct.comp q h

noncomputable def CategoryTheory.Limits.coequalizer.desc' {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : { l : coequalizer f g ⟶ W // CategoryStruct.comp (π f g) l = k }

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.

theorem CategoryTheory.Limits.coequalizer.hom_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} {k l : coequalizer f g ⟶ W} (h : CategoryStruct.comp (π f g) k = CategoryStruct.comp (π f g) l) : k = l

Two maps from a coequalizer are equal if they are equal when composed with the coequalizer map

theorem CategoryTheory.Limits.coequalizer.hom_ext_iff {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} {k l : coequalizer f g ⟶ W} : k = l ↔ CategoryStruct.comp (π f g) k = CategoryStruct.comp (π f g) l

theorem CategoryTheory.Limits.coequalizer.existsUnique {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = CategoryStruct.comp g k) : ∃! d : coequalizer f g ⟶ W, CategoryStruct.comp (π f g) d = k

instance CategoryTheory.Limits.coequalizer.π_epi {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] : Epi (π f g)

A coequalizer morphism is an epimorphism

theorem CategoryTheory.Limits.epi_of_isColimit_cofork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Cofork f g} (i : IsColimit c) : Epi c.π

The coequalizer morphism in any colimit cocone is an epimorphism.

def CategoryTheory.Limits.idCofork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h : f = g) : Cofork f g

The identity determines a cocone on the coequalizer diagram of f and g, if f = g.

def CategoryTheory.Limits.isColimitIdCofork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h : f = g) : IsColimit (idCofork h)

The identity on Y is a coequalizer of (f, g), where f = g.

theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (h₀ : f = g) {c : Cofork f g} (h : IsColimit c) : IsIso c.π

Every coequalizer of (f, g), where f = g, is an isomorphism.

theorem CategoryTheory.Limits.coequalizer.π_of_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] (h : f = g) : IsIso (π f g)

The coequalizer of (f, g), where f = g, is an isomorphism.

theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {c : Cofork f f} (h : IsColimit c) : IsIso c.π

Every coequalizer of (f, f) is an isomorphism.

theorem CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Cofork f g} (h : IsColimit c) [Mono c.π] : IsIso c.π

A coequalizer that is a monomorphism is an isomorphism.

theorem CategoryTheory.Limits.eq_of_mono_cofork_π {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : Cofork f g) [Mono t.π] : f = g

Two morphisms are equal if there is a cofork whose projection is mono.

theorem CategoryTheory.Limits.eq_of_mono_coequalizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] [Mono (coequalizer.π f g)] : f = g

If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal.

instance CategoryTheory.Limits.hasCoequalizer_of_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : HasCoequalizer f f

instance CategoryTheory.Limits.coequalizer.π_of_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : IsIso (π f f)

The coequalizer projection for (f, f) is an isomorphism.

noncomputable def CategoryTheory.Limits.coequalizer.isoTargetOfSelf {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : coequalizer f f ≅ Y

The coequalizer of a morphism with itself is isomorphic to the target.

@[simp]

theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : (isoTargetOfSelf f).hom = desc (CategoryStruct.id Y) ⋯

@[simp]

theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : (isoTargetOfSelf f).inv = π f f

noncomputable def CategoryTheory.Limits.equalizerComparison {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] : G.obj (equalizer f g) ⟶ equalizer (G.map f) (G.map g)

The comparison morphism for the equalizer of f,g. This is an isomorphism iff G preserves the equalizer of f,g; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean

@[simp]

theorem CategoryTheory.Limits.equalizerComparison_comp_π {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] : CategoryStruct.comp (equalizerComparison f g G) (equalizer.ι (G.map f) (G.map g)) = G.map (equalizer.ι f g)

@[simp]

theorem CategoryTheory.Limits.equalizerComparison_comp_π_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : D} (h : G.obj X ⟶ Z) : CategoryStruct.comp (equalizerComparison f g G) (CategoryStruct.comp (equalizer.ι (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (equalizer.ι f g)) h

@[simp]

theorem CategoryTheory.Limits.map_lift_equalizerComparison {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : CategoryStruct.comp h f = CategoryStruct.comp h g) : CategoryStruct.comp (G.map (equalizer.lift h w)) (equalizerComparison f g G) = equalizer.lift (G.map h) ⋯

@[simp]

theorem CategoryTheory.Limits.map_lift_equalizerComparison_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : CategoryStruct.comp h f = CategoryStruct.comp h g) {Z✝ : D} (h✝ : equalizer (G.map f) (G.map g) ⟶ Z✝) : CategoryStruct.comp (G.map (equalizer.lift h w)) (CategoryStruct.comp (equalizerComparison f g G) h✝) = CategoryStruct.comp (equalizer.lift (G.map h) ⋯) h✝

noncomputable def CategoryTheory.Limits.coequalizerComparison {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] : coequalizer (G.map f) (G.map g) ⟶ G.obj (coequalizer f g)

The comparison morphism for the coequalizer of f,g.

@[simp]

theorem CategoryTheory.Limits.ι_comp_coequalizerComparison {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] : CategoryStruct.comp (coequalizer.π (G.map f) (G.map g)) (coequalizerComparison f g G) = G.map (coequalizer.π f g)

@[simp]

theorem CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : D} (h : G.obj (coequalizer f g) ⟶ Z) : CategoryStruct.comp (coequalizer.π (G.map f) (G.map g)) (CategoryStruct.comp (coequalizerComparison f g G) h) = CategoryStruct.comp (G.map (coequalizer.π f g)) h

@[simp]

theorem CategoryTheory.Limits.coequalizerComparison_map_desc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z} (w : CategoryStruct.comp f h = CategoryStruct.comp g h) : CategoryStruct.comp (coequalizerComparison f g G) (G.map (coequalizer.desc h w)) = coequalizer.desc (G.map h) ⋯

@[simp]

theorem CategoryTheory.Limits.coequalizerComparison_map_desc_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z} (w : CategoryStruct.comp f h = CategoryStruct.comp g h) {Z✝ : D} (h✝ : G.obj Z ⟶ Z✝) : CategoryStruct.comp (coequalizerComparison f g G) (CategoryStruct.comp (G.map (coequalizer.desc h w)) h✝) = CategoryStruct.comp (coequalizer.desc (G.map h) ⋯) h✝

@[reducible, inline]

abbrev CategoryTheory.Limits.HasEqualizers (C : Type u) [Category.{v, u} C] : Prop

A category HasEqualizers if it has all limits of shape WalkingParallelPair, i.e. if it has an equalizer for every parallel pair of morphisms.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoequalizers (C : Type u) [Category.{v, u} C] : Prop

A category HasCoequalizers if it has all colimits of shape WalkingParallelPair, i.e. if it has a coequalizer for every parallel pair of morphisms.

theorem CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair (C : Type u) [Category.{v, u} C] [∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)] : HasEqualizers C

If C has all limits of diagrams parallelPair f g, then it has all equalizers

theorem CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair (C : Type u) [Category.{v, u} C] [∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)] : HasCoequalizers C

If C has all colimits of diagrams parallelPair f g, then it has all coequalizers

noncomputable def CategoryTheory.Limits.coneOfIsSplitMono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : Fork (CategoryStruct.id Y) (CategoryStruct.comp (retraction f) f)

A split mono f equalizes (retraction f ≫ f) and (𝟙 Y). Here we build the cone, and show in isSplitMonoEqualizes that it is a limit cone.

@[simp]

theorem CategoryTheory.Limits.coneOfIsSplitMono_pt {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : (coneOfIsSplitMono f).pt = X

@[simp]

theorem CategoryTheory.Limits.coneOfIsSplitMono_π_app {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] (X✝ : WalkingParallelPair) : (coneOfIsSplitMono f).π.app X✝ = WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) => X✝ = t → (((Functor.const WalkingParallelPair).obj X).obj X✝ ⟶ (parallelPair (CategoryStruct.id Y) (CategoryStruct.comp (retraction f) f)).obj X✝)) X✝ (fun (h : X✝ = WalkingParallelPair.zero) => ⋯ ▸ f) (fun (h : X✝ = WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp f (CategoryStruct.id Y)) ⋯

@[simp]

theorem CategoryTheory.Limits.coneOfIsSplitMono_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : (coneOfIsSplitMono f).ι = f

noncomputable def CategoryTheory.Limits.isSplitMonoEqualizes {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsLimit (coneOfIsSplitMono f)

A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).

def CategoryTheory.Limits.splitMonoOfEqualizer (C : Type u) [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : CategoryStruct.comp f (CategoryStruct.comp r f) = f) (h : IsLimit (Fork.ofι f ⋯)) : SplitMono f

We show that the converse to isSplitMonoEqualizes is true: Whenever f equalizes (r ≫ f) and (𝟙 Y), then r is a retraction of f.

def CategoryTheory.Limits.isEqualizerCompMono {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Fork f g} (i : IsLimit c) {Z : C} (h : Y ⟶ Z) [hm : Mono h] : have this := ⋯; IsLimit (Fork.ofι c.ι ⋯)

The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.

instance CategoryTheory.Limits.hasEqualizer_comp_mono (C : Type u) [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [Mono h] : HasEqualizer (CategoryStruct.comp f h) (CategoryStruct.comp g h)

def CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) {c : Fork (CategoryStruct.id X) f} (i : IsLimit c) : SplitMono c.ι

An equalizer of an idempotent morphism and the identity is split mono.

@[simp]

theorem CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) {c : Fork (CategoryStruct.id X) f} (i : IsLimit c) : (splitMonoOfIdempotentOfIsLimitFork C hf i).retraction = i.lift (Fork.ofι f ⋯)

noncomputable def CategoryTheory.Limits.splitMonoOfIdempotentEqualizer (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) [HasEqualizer (CategoryStruct.id X) f] : SplitMono (equalizer.ι (CategoryStruct.id X) f)

The equalizer of an idempotent morphism and the identity is split mono.

noncomputable def CategoryTheory.Limits.coconeOfIsSplitEpi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : Cofork (CategoryStruct.id X) (CategoryStruct.comp f (section_ f))

A split epi f coequalizes (f ≫ section_ f) and (𝟙 X). Here we build the cocone, and show in isSplitEpiCoequalizes that it is a colimit cocone.

@[simp]

theorem CategoryTheory.Limits.coconeOfIsSplitEpi_ι_app {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] (X✝ : WalkingParallelPair) : (coconeOfIsSplitEpi f).ι.app X✝ = WalkingParallelPair.casesOn X✝ (CategoryStruct.comp (CategoryStruct.id X) f) f

@[simp]

theorem CategoryTheory.Limits.coconeOfIsSplitEpi_pt {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : (coconeOfIsSplitEpi f).pt = Y

@[simp]

theorem CategoryTheory.Limits.coconeOfIsSplitEpi_π {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : (coconeOfIsSplitEpi f).π = f

noncomputable def CategoryTheory.Limits.isSplitEpiCoequalizes {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsColimit (coconeOfIsSplitEpi f)

A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).

def CategoryTheory.Limits.splitEpiOfCoequalizer (C : Type u) [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : CategoryStruct.comp f (CategoryStruct.comp s f) = f) (h : IsColimit (Cofork.ofπ f ⋯)) : SplitEpi f

We show that the converse to isSplitEpiEqualizes is true: Whenever f coequalizes (f ≫ s) and (𝟙 X), then s is a section of f.

def CategoryTheory.Limits.isCoequalizerEpiComp {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {c : Cofork f g} (i : IsColimit c) {W : C} (h : W ⟶ X) [hm : Epi h] : have this := ⋯; IsColimit (Cofork.ofπ c.π this)

The cofork obtained by precomposing a coequalizer cofork with an epimorphism is a coequalizer.

theorem CategoryTheory.Limits.hasCoequalizer_epi_comp {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [HasCoequalizer f g] {W : C} (h : W ⟶ X) [Epi h] : HasCoequalizer (CategoryStruct.comp h f) (CategoryStruct.comp h g)

def CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) {c : Cofork (CategoryStruct.id X) f} (i : IsColimit c) : SplitEpi c.π

A coequalizer of an idempotent morphism and the identity is split epi.

@[simp]

theorem CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_ (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) {c : Cofork (CategoryStruct.id X) f} (i : IsColimit c) : (splitEpiOfIdempotentOfIsColimitCofork C hf i).section_ = i.desc (Cofork.ofπ f ⋯)

noncomputable def CategoryTheory.Limits.splitEpiOfIdempotentCoequalizer (C : Type u) [Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryStruct.comp f f = f) [HasCoequalizer (CategoryStruct.id X) f] : SplitEpi (coequalizer.π (CategoryStruct.id X) f)

The coequalizer of an idempotent morphism and the identity is split epi.