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 abbreviations 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

inductive CategoryTheory.Limits.WalkingParallelPair : Type

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

• zero : WalkingParallelPair
• one : WalkingParallelPair

instance CategoryTheory.Limits.instDecidableEqWalkingParallelPair : DecidableEq WalkingParallelPair

Equations

• CategoryTheory.Limits.instDecidableEqWalkingParallelPair x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CategoryTheory.Limits.instInhabitedWalkingParallelPair : Inhabited WalkingParallelPair

Equations

• CategoryTheory.Limits.instInhabitedWalkingParallelPair = { default := CategoryTheory.Limits.WalkingParallelPair.zero }

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

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

Equations

• CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom = CategoryTheory.Limits.decEqWalkingParallelPairHom✝

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

Satisfying the inhabited linter

Equations

• CategoryTheory.Limits.instInhabitedWalkingParallelPairHomZeroOne = { default := CategoryTheory.Limits.WalkingParallelPairHom.left }

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.

Equations

• One or more equations did not get rendered due to their size.
• (CategoryTheory.Limits.WalkingParallelPairHom.id x✝²).comp x✝ = x✝

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)

instance CategoryTheory.Limits.walkingParallelPairHomCategory : SmallCategory WalkingParallelPair

Equations

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

@[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.

Equations

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

@[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.

Equations

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

@[simp]

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

@[simp]

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

@[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)

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.

Equations

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

@[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

Equations

• CategoryTheory.Limits.diagramIsoParallelPair F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WalkingParallelPair) => CategoryTheory.eqToIso ⋯) ⋯

@[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.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.

Equations

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

@[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)) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right)) : F ≅ G

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

Equations

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

@[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)) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right)) (X : WalkingParallelPair) : (ext zero one left right).hom.app X = (WalkingParallelPair.rec zero one X).hom

@[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)) (right : CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right)) (X : WalkingParallelPair) : (ext zero one left right).inv.app X = (WalkingParallelPair.rec zero one X).inv

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

Equations

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

@[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).

Equations

• CategoryTheory.Limits.Fork f g = CategoryTheory.Limits.Cone (CategoryTheory.Limits.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).

Equations

• CategoryTheory.Limits.Cofork f g = CategoryTheory.Limits.Cocone (CategoryTheory.Limits.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) : ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.zero ⟶ (parallelPair f g).obj WalkingParallelPair.zero

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.

Equations

• t.ι = t.π.app CategoryTheory.Limits.WalkingParallelPair.zero

@[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) : (parallelPair f g).obj WalkingParallelPair.one ⟶ ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.one

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.

Equations

• t.π = t.ι.app CategoryTheory.Limits.WalkingParallelPair.one

@[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.

Equations

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

@[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

@[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) ⋯

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 ≫ π.

Equations

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

@[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.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.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).π = π

@[simp]

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

@[simp]

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)

@[simp]

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

@[simp]

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 : ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.one ⟶ 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 : (parallelPair f g).obj WalkingParallelPair.zero ⟶ 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.

Equations

• CategoryTheory.Limits.Fork.IsLimit.lift hs k h = hs.lift (CategoryTheory.Limits.Fork.ofι k h)

@[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✝ : (parallelPair f g).obj WalkingParallelPair.zero ⟶ 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.

Equations

• CategoryTheory.Limits.Fork.IsLimit.lift' hs k h = ⟨CategoryTheory.Limits.Fork.IsLimit.lift hs 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) : 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.

Equations

• CategoryTheory.Limits.Cofork.IsColimit.desc hs k h = hs.desc (CategoryTheory.Limits.Cofork.ofπ k h)

@[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.

Equations

• CategoryTheory.Limits.Cofork.IsColimit.desc' hs k h = ⟨CategoryTheory.Limits.Cofork.IsColimit.desc hs k h, ⋯⟩

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

Equations

• CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

@[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 : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.zero // CategoryStruct.comp l t.ι = s.ι ∧ ∀ {m : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.zero}, 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.

Equations

• CategoryTheory.Limits.Fork.IsLimit.mk' t create = CategoryTheory.Limits.Fork.IsLimit.mk t (fun (s : CategoryTheory.Limits.Fork f g) => ↑(create s)) ⋯ ⋯

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

Equations

• CategoryTheory.Limits.Cofork.IsColimit.mk t desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }

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 : ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.one ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one}, 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.

Equations

• CategoryTheory.Limits.Cofork.IsColimit.mk' t create = CategoryTheory.Limits.Cofork.IsColimit.mk t (fun (s : CategoryTheory.Limits.Cofork f g) => ↑(create s)) ⋯ ⋯

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.

Equations

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

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.

Equations

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

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.

Equations

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

@[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.

Equations

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

@[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

@[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 ⋯)

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.

Equations

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

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.

Equations

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

@[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.

Equations

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

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.

Equations

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

@[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} : ι ((Cones.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'} : π ((Cocones.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.

Equations

• CategoryTheory.Limits.Fork.mkHom k w = { hom := k, w := ⋯ }

@[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 aesop_cat) : 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.

Equations

• CategoryTheory.Limits.Fork.ext i w = { hom := CategoryTheory.Limits.Fork.mkHom i.hom w, inv := CategoryTheory.Limits.Fork.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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 aesop_cat) : (ext i w).hom = mkHom i.hom w

@[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 aesop_cat) : (ext i w).inv = mkHom i.inv ⋯

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.

Equations

• CategoryTheory.Limits.ForkOfι.ext w w' h = CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fork.ofι ι w).pt) ⋯

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_ι _ _.

Equations

• c.isoForkOfι = CategoryTheory.Limits.Fork.ext (id (CategoryTheory.Iso.refl c.pt)) ⋯

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 aesop_cat) (comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by aesop_cat) (comm₃ : CategoryStruct.comp e.hom c'.ι = CategoryStruct.comp c.ι e₀.hom := by aesop_cat) : 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.

Equations

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

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.

Equations

• CategoryTheory.Limits.Cofork.mkHom k w = { hom := k, w := ⋯ }

@[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 : (parallelPair f g).obj WalkingParallelPair.zero ⟶ 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 aesop_cat) : 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.

Equations

• CategoryTheory.Limits.Cofork.ext i w = { hom := CategoryTheory.Limits.Cofork.mkHom i.hom w, inv := CategoryTheory.Limits.Cofork.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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 aesop_cat) : (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 aesop_cat) : (ext i w).hom = mkHom i.hom w

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π _ _.

Equations

• c.isoCoforkOfπ = CategoryTheory.Limits.Cofork.ext (id (CategoryTheory.Iso.refl c.pt)) ⋯

@[reducible, inline]

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

HasEqualizer f g represents a particular choice of limiting cone for the parallel pair of morphisms f and g.

Equations

• CategoryTheory.Limits.HasEqualizer f g = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair 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] : C

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

Equations

• CategoryTheory.Limits.equalizer f g = CategoryTheory.Limits.limit (CategoryTheory.Limits.parallelPair 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.

Equations

• CategoryTheory.Limits.equalizer.ι f g = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.parallelPair f g) CategoryTheory.Limits.WalkingParallelPair.zero

@[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

Equations

• CategoryTheory.Limits.equalizer.fork f g = CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair f 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.

Equations

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

@[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.

Equations

• CategoryTheory.Limits.equalizer.lift k h = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.Limits.Fork.ofι k h)

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.

Equations

• CategoryTheory.Limits.equalizer.lift' k h = ⟨CategoryTheory.Limits.equalizer.lift k h, ⋯⟩

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.

Equations

• CategoryTheory.Limits.idFork h = CategoryTheory.Limits.Fork.ofι (CategoryTheory.CategoryStruct.id X) ⋯

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.

Equations

• CategoryTheory.Limits.isLimitIdFork h = CategoryTheory.Limits.Fork.IsLimit.mk (CategoryTheory.Limits.idFork h) (fun (s : CategoryTheory.Limits.Fork f g) => s.ι) ⋯ ⋯

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.

Equations

• CategoryTheory.Limits.equalizer.isoSourceOfSelf f = CategoryTheory.asIso (CategoryTheory.Limits.equalizer.ι f f)

@[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) ⋯

@[reducible, inline]

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

HasCoequalizer f g represents a particular choice of colimiting cocone for the parallel pair of morphisms f and g.

Equations

• CategoryTheory.Limits.HasCoequalizer f g = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair 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] : C

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

Equations

• CategoryTheory.Limits.coequalizer f g = CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair 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.

Equations

• CategoryTheory.Limits.coequalizer.π f g = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f g) CategoryTheory.Limits.WalkingParallelPair.one

@[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.

Equations

• CategoryTheory.Limits.coequalizer.cofork f g = CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair f 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.

Equations

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

@[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.

Equations

• CategoryTheory.Limits.coequalizer.desc k h = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair f g) (CategoryTheory.Limits.Cofork.ofπ k h)

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.

Equations

• CategoryTheory.Limits.coequalizer.desc' k h = ⟨CategoryTheory.Limits.coequalizer.desc k h, ⋯⟩

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.

Equations

• CategoryTheory.Limits.idCofork h = CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.CategoryStruct.id Y) ⋯

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.

Equations

• CategoryTheory.Limits.isColimitIdCofork h = CategoryTheory.Limits.Cofork.IsColimit.mk (CategoryTheory.Limits.idCofork h) (fun (s : CategoryTheory.Limits.Cofork f g) => s.π) ⋯ ⋯

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.

Equations

• CategoryTheory.Limits.coequalizer.isoTargetOfSelf f = (CategoryTheory.asIso (CategoryTheory.Limits.coequalizer.π f f)).symm

@[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 CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean

Equations

• CategoryTheory.Limits.equalizerComparison f g G = CategoryTheory.Limits.equalizer.lift (G.map (CategoryTheory.Limits.equalizer.ι f g)) ⋯

@[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.

Equations

• CategoryTheory.Limits.coequalizerComparison f g G = CategoryTheory.Limits.coequalizer.desc (G.map (CategoryTheory.Limits.coequalizer.π 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

HasEqualizers represents a choice of equalizer for every pair of morphisms

Equations

• CategoryTheory.Limits.HasEqualizers C = CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C

@[reducible, inline]

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

HasCoequalizers represents a choice of coequalizer for every pair of morphisms

Equations

• CategoryTheory.Limits.HasCoequalizers C = CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair C

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.

Equations

• CategoryTheory.Limits.coneOfIsSplitMono f = CategoryTheory.Limits.Fork.ofι f ⋯

@[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.rec (motive := fun (t : WalkingParallelPair) => X✝ = t → (X ⟶ (parallelPair (CategoryStruct.id Y) (CategoryStruct.comp (retraction f) f)).obj X✝)) (fun (h : X✝ = WalkingParallelPair.zero) => ⋯ ▸ f) (fun (h : X✝ = WalkingParallelPair.one) => ⋯ ▸ f) X✝ ⋯

@[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).

Equations

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

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.

Equations

• CategoryTheory.Limits.splitMonoOfEqualizer C hr h = { retraction := r, id := ⋯ }

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] : let_fun this := ⋯; IsLimit (Fork.ofι c.ι ⋯)

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

Equations

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

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.

Equations

• CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i = { retraction := i.lift (CategoryTheory.Limits.Fork.ofι f ⋯), id := ⋯ }

@[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.

Equations

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

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.

Equations

• CategoryTheory.Limits.coconeOfIsSplitEpi f = CategoryTheory.Limits.Cofork.ofπ f ⋯

@[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.rec f f X✝

@[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).

Equations

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

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.

Equations

• CategoryTheory.Limits.splitEpiOfCoequalizer C hs h = { section_ := s, id := ⋯ }

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] : let_fun this := ⋯; IsColimit (Cofork.ofπ c.π this)

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

Equations

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

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.

Equations

• CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i = { section_ := i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯), id := ⋯ }

@[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.

Equations

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