# mathlib3documentation

category_theory.limits.shapes.equalizers

# Equalizers and coequalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• walking_parallel_pair is the indexing category used for (co)equalizer_diagrams
• parallel_pair is a functor from walking_parallel_pair 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 (parallel_pair f g)

Each of these has a dual.

## Main statements #

• equalizer.ι_mono states that every equalizer map is a monomorphism
• is_iso_limit_cone_parallel_pair_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 #

@[protected, instance]

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

Instances for category_theory.limits.walking_parallel_pair
@[protected, instance]
@[protected, instance]

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

Instances for category_theory.limits.walking_parallel_pair_hom
@[protected, instance]

Satisfying the inhabited linter

Equations
@[protected, instance]
Equations

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

Equations

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

Equations
def category_theory.limits.parallel_pair {C : Type u} {X Y : C} (f g : X Y) :

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

Equations
Instances for category_theory.limits.parallel_pair
@[simp]
theorem category_theory.limits.parallel_pair_obj_zero {C : Type u} {X Y : C} (f g : X Y) :
@[simp]
theorem category_theory.limits.parallel_pair_obj_one {C : Type u} {X Y : C} (f g : X Y) :
@[simp]
theorem category_theory.limits.parallel_pair_map_left {C : Type u} {X Y : C} (f g : X Y) :
@[simp]
theorem category_theory.limits.parallel_pair_map_right {C : Type u} {X Y : C} (f g : X Y) :
@[simp]
@[simp]
@[simp]

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

Equations
def category_theory.limits.parallel_pair_hom {C : Type u} {X Y X' Y' : C} (f g : X Y) (f' g' : X' Y') (p : X X') (q : Y Y') (wf : f q = p f') (wg : g q = p g') :

Construct a morphism between parallel pairs.

Equations
@[simp]
theorem category_theory.limits.parallel_pair_hom_app_zero {C : Type u} {X Y X' Y' : C} (f g : X Y) (f' g' : X' Y') (p : X X') (q : Y Y') (wf : f q = p f') (wg : g q = p g') :
@[simp]
theorem category_theory.limits.parallel_pair_hom_app_one {C : Type u} {X Y X' Y' : C} (f g : X Y) (f' g' : X' Y') (p : X X') (q : Y Y') (wf : f q = p f') (wg : g q = p g') :

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

Equations
@[simp]
theorem category_theory.limits.parallel_pair.ext_hom_app {C : Type u}  :
left right).hom.app X = (category_theory.limits.walking_parallel_pair.rec zero one X).hom
@[simp]
theorem category_theory.limits.parallel_pair.ext_inv_app {C : Type u}  :
left right).inv.app X = (category_theory.limits.walking_parallel_pair.rec zero one X).inv
@[simp]
theorem category_theory.limits.parallel_pair.eq_of_hom_eq_inv_app {C : Type u} {X Y : C} {f g f' g' : X Y} (hf : f = f') (hg : g = g')  :
= (category_theory.limits.walking_parallel_pair.rec X_1).inv
def category_theory.limits.parallel_pair.eq_of_hom_eq {C : Type u} {X Y : C} {f g f' g' : X Y} (hf : f = f') (hg : g = g') :

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

Equations
@[simp]
theorem category_theory.limits.parallel_pair.eq_of_hom_eq_hom_app {C : Type u} {X Y : C} {f g f' g' : X Y} (hf : f = f') (hg : g = g')  :
= (category_theory.limits.walking_parallel_pair.rec X_1).hom
@[reducible]
def category_theory.limits.fork {C : Type u} {X Y : C} (f g : X Y) :
Type (max u v)

A fork on f and g is just a cone (parallel_pair f g).

@[reducible]
def category_theory.limits.cofork {C : Type u} {X Y : C} (f g : X Y) :
Type (max u v)

A cofork on f and g is just a cocone (parallel_pair f g).

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

Equations
Instances for category_theory.limits.fork.ι
@[simp]
theorem category_theory.limits.fork.app_zero_eq_ι {C : Type u} {X Y : C} {f g : X Y} (t : g) :

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

Equations
@[simp]
theorem category_theory.limits.cofork.app_one_eq_π {C : Type u} {X Y : C} {f g : X Y} (t : g) :
@[simp]
theorem category_theory.limits.fork.app_one_eq_ι_comp_left {C : Type u} {X Y : C} {f g : X Y} (s : g) :
theorem category_theory.limits.fork.app_one_eq_ι_comp_right_assoc {C : Type u} {X Y : C} {f g : X Y} (s : g) {X' : C}  :
= s.ι g f'
theorem category_theory.limits.fork.app_one_eq_ι_comp_right {C : Type u} {X Y : C} {f g : X Y} (s : g) :
@[simp]
theorem category_theory.limits.cofork.app_zero_eq_comp_π_left {C : Type u} {X Y : C} {f g : X Y} (s : g) :
theorem category_theory.limits.cofork.app_zero_eq_comp_π_right_assoc {C : Type u} {X Y : C} {f g : X Y} (s : g) {X' : C}  :
= g s.π f'
theorem category_theory.limits.cofork.app_zero_eq_comp_π_right {C : Type u} {X Y : C} {f g : X Y} (s : g) :
@[simp]
theorem category_theory.limits.fork.of_ι_X {C : Type u} {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :
@[simp]
theorem category_theory.limits.fork.of_ι_π_app {C : Type u} {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g)  :
X_1 = X_1.cases_on ι f)
def category_theory.limits.fork.of_ι {C : Type u} {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :

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

Equations
def category_theory.limits.cofork.of_π {C : Type u} {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f π = g π) :

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

Equations
@[simp]
theorem category_theory.limits.cofork.of_π_X {C : Type u} {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f π = g π) :
@[simp]
theorem category_theory.limits.cofork.of_π_ι_app {C : Type u} {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f π = g π)  :
X_1 = X_1.cases_on (f π) π
@[simp]
theorem category_theory.limits.fork.ι_of_ι {C : Type u} {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :
@[simp]
theorem category_theory.limits.cofork.π_of_π {C : Type u} {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f π = g π) :
@[simp]
theorem category_theory.limits.fork.condition {C : Type u} {X Y : C} {f g : X Y} (t : g) :
t.ι f = t.ι g
@[simp]
theorem category_theory.limits.fork.condition_assoc {C : Type u} {X Y : C} {f g : X Y} (t : g) {X' : C} (f' : Y X') :
t.ι f f' = t.ι g f'
@[simp]
theorem category_theory.limits.cofork.condition_assoc {C : Type u} {X Y : C} {f g : X Y} (t : g) {X' : C}  :
f t.π f' = g t.π f'
@[simp]
theorem category_theory.limits.cofork.condition {C : Type u} {X Y : C} {f g : X Y} (t : g) :
f t.π = g t.π
theorem category_theory.limits.fork.equalizer_ext {C : Type u} {X Y : C} {f g : X Y} (s : g) {W : C} {k l : W s.X} (h : k s.ι = l s.ι)  :
k s.π.app j = 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 category_theory.limits.cofork.coequalizer_ext {C : Type u} {X Y : C} {f g : X Y} (s : g) {W : C} {k l : s.X W} (h : s.π k = s.π l)  :
s.ι.app j k = 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 category_theory.limits.fork.is_limit.hom_ext {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} {k l : W s.X} (h : k s.ι = l s.ι) :
k = l
theorem category_theory.limits.cofork.is_colimit.hom_ext {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} {k l : s.X W} (h : s.π k = s.π l) :
k = l
@[simp]
theorem category_theory.limits.fork.is_limit.lift_ι_assoc {C : Type u} {X Y : C} {f g : X Y} {s t : g} {X' : C}  :
hs.lift t s.ι f' = t.ι f'
@[simp]
theorem category_theory.limits.fork.is_limit.lift_ι {C : Type u} {X Y : C} {f g : X Y} {s t : g}  :
hs.lift t s.ι = t.ι
@[simp]
theorem category_theory.limits.cofork.is_colimit.π_desc_assoc {C : Type u} {X Y : C} {f g : X Y} {s t : g} {X' : C} (f' : t.X X') :
s.π hs.desc t f' = t.π f'
@[simp]
theorem category_theory.limits.cofork.is_colimit.π_desc {C : Type u} {X Y : C} {f g : X Y} {s t : g}  :
s.π hs.desc t = t.π
def category_theory.limits.fork.is_limit.lift' {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} (k : W X) (h : k f = k g) :
{l // 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.X such that l ≫ fork.ι s = k.

Equations
def category_theory.limits.cofork.is_colimit.desc' {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} (k : Y W) (h : f k = g k) :
{l // 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.X ⟶ W such that cofork.π s ≫ l = k.

Equations
theorem category_theory.limits.fork.is_limit.exists_unique {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} (k : W X) (h : k f = k g) :
∃! (l : W s.X), l s.ι = k
theorem category_theory.limits.cofork.is_colimit.exists_unique {C : Type u} {X Y : C} {f g : X Y} {s : g} {W : C} (k : Y W) (h : f k = g k) :
∃! (d : s.X W), s.π d = k
def category_theory.limits.fork.is_limit.mk {C : Type u} {X Y : C} {f g : X Y} (t : g) (lift : Π (s : , s.X t.X) (fac : (s : , lift s t.ι = s.ι) (uniq : (s : (m : s.X t.X), m t.ι = s.ι m = lift s) :

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
@[simp]
theorem category_theory.limits.fork.is_limit.mk_lift {C : Type u} {X Y : C} {f g : X Y} (t : g) (lift : Π (s : , s.X t.X) (fac : (s : , lift s t.ι = s.ι) (uniq : (s : (m : s.X t.X), m t.ι = s.ι m = lift s) (s : g) :
fac uniq).lift s = lift s
def category_theory.limits.fork.is_limit.mk' {C : Type u} {X Y : C} {f g : X Y} (t : g) (create : Π (s : , ) :

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
• = (λ (s : , (create s).val) _ _
def category_theory.limits.cofork.is_colimit.mk {C : Type u} {X Y : C} {f g : X Y} (t : g) (desc : Π (s : , t.X s.X) (fac : (s : , t.π desc s = s.π) (uniq : (s : (m : t.X s.X), t.π m = s.π m = desc s) :

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
def category_theory.limits.cofork.is_colimit.mk' {C : Type u} {X Y : C} {f g : X Y} (t : g) (create : Π (s : , ) :

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
• = (λ (s : , (create s).val) _ _
noncomputable def category_theory.limits.fork.is_limit.of_exists_unique {C : Type u} {X Y : C} {f g : X Y} {t : g} (hs : (s : , ∃! (l : s.X t.X), l t.ι = s.ι) :

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

Equations
noncomputable def category_theory.limits.cofork.is_colimit.of_exists_unique {C : Type u} {X Y : C} {f g : X Y} {t : g} (hs : (s : , ∃! (d : t.X s.X), t.π d = s.π) :

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

Equations
def category_theory.limits.fork.is_limit.hom_iso {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) :
(Z t.X) {h // h f = 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.is_limit.hom_iso_natural. This is a special case of is_limit.hom_iso', often useful to construct adjunctions.

Equations
@[simp]
theorem category_theory.limits.fork.is_limit.hom_iso_apply_coe {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) (k : Z t.X) :
= k t.ι
@[simp]
theorem category_theory.limits.fork.is_limit.hom_iso_symm_apply {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) (h : {h // h f = h g}) :
theorem category_theory.limits.fork.is_limit.hom_iso_natural {C : Type u} {X Y : C} {f g : X Y} {t : g} {Z Z' : C} (q : Z' Z) (k : Z t.X) :
(q k)) = q

The bijection of fork.is_limit.hom_iso is natural in Z.

def category_theory.limits.cofork.is_colimit.hom_iso {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) :
(t.X Z) {h // f h = 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.is_colimit.hom_iso_natural. This is a special case of is_colimit.hom_iso', often useful to construct adjunctions.

Equations
@[simp]
theorem category_theory.limits.cofork.is_colimit.hom_iso_symm_apply {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) (h : {h // f h = g h}) :
@[simp]
theorem category_theory.limits.cofork.is_colimit.hom_iso_apply_coe {C : Type u} {X Y : C} {f g : X Y} {t : g} (Z : C) (k : t.X Z) :
= t.π k
theorem category_theory.limits.cofork.is_colimit.hom_iso_natural {C : Type u} {X Y : C} {f g : X Y} {t : g} {Z Z' : C} (q : Z Z') (k : t.X Z) :
(k q)) =

The bijection of cofork.is_colimit.hom_iso is natural in Z.

This is a helper construction that can be useful when verifying that a category has all equalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (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 has_equalizers_of_has_limit_parallel_pair, which you may find to be an easier way of achieving your goal.

Equations

This is a helper construction that can be useful when verifying that a category has all coequalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (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 has_coequalizers_of_has_colimit_parallel_pair, which you may find to be an easier way of achieving your goal.

Equations
@[simp]
@[simp]

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

Equations

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

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.fork.ι_postcompose {C : Type u} {X Y : C} {f g f' g' : X Y} {c : g} :
@[simp]
theorem category_theory.limits.cofork.π_precompose {C : Type u} {X Y : C} {f g f' g' : X Y} {c : g'} :
def category_theory.limits.fork.mk_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (k : s.X t.X) (w : k t.ι = s.ι) :
s t

Helper function for constructing morphisms between equalizer forks.

Equations
@[simp]
theorem category_theory.limits.fork.mk_hom_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (k : s.X t.X) (w : k t.ι = s.ι) :
@[simp]
theorem category_theory.limits.fork.ext_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
@[simp]
theorem category_theory.limits.fork.ext_inv {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
def category_theory.limits.fork.ext {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
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
def category_theory.limits.fork.iso_fork_of_ι {C : Type u} {X Y : C} {f g : X Y} (c : g) :

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

Equations
def category_theory.limits.cofork.mk_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (k : s.X t.X) (w : s.π k = t.π) :
s t

Helper function for constructing morphisms between coequalizer coforks.

Equations
@[simp]
theorem category_theory.limits.cofork.mk_hom_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (k : s.X t.X) (w : s.π k = t.π) :
@[simp]
theorem category_theory.limits.fork.hom_comp_ι_assoc {C : Type u} {X Y : C} {g f : X Y} {s t : g} (f_1 : s t) {X' : C}  :
f_1.hom t.ι f' = s.ι f'
@[simp]
theorem category_theory.limits.fork.hom_comp_ι {C : Type u} {X Y : C} {g f : X Y} {s t : g} (f_1 : s t) :
f_1.hom t.ι = s.ι
@[simp]
theorem category_theory.limits.fork.π_comp_hom {C : Type u} {X Y : C} {g f : X Y} {s t : g} (f_1 : s t) :
s.π f_1.hom = t.π
@[simp]
theorem category_theory.limits.fork.π_comp_hom_assoc {C : Type u} {X Y : C} {g f : X Y} {s t : g} (f_1 : s t) {X' : C} (f' : t.X X') :
s.π f_1.hom f' = t.π f'
@[simp]
theorem category_theory.limits.cofork.ext_inv {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : s.π i.hom = t.π) :
@[simp]
theorem category_theory.limits.cofork.ext_hom {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : s.π i.hom = t.π) :
def category_theory.limits.cofork.ext {C : Type u} {X Y : C} {f g : X Y} {s t : g} (i : s.X t.X) (w : s.π i.hom = t.π) :
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
def category_theory.limits.cofork.iso_cofork_of_π {C : Type u} {X Y : C} {f g : X Y} (c : g) :

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

Equations
@[reducible]
def category_theory.limits.has_equalizer {C : Type u} {X Y : C} (f g : X Y) :
Prop

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

@[reducible]
noncomputable def category_theory.limits.equalizer {C : Type u} {X Y : C} (f g : X Y)  :
C

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

@[reducible]
noncomputable def category_theory.limits.equalizer.ι {C : Type u} {X Y : C} (f g : X Y)  :

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

@[reducible]
noncomputable def category_theory.limits.equalizer.fork {C : Type u} {X Y : C} (f g : X Y)  :

An equalizer cone for a parallel pair f and g.

@[simp]
theorem category_theory.limits.equalizer.fork_ι {C : Type u} {X Y : C} (f g : X Y)  :
@[simp]
theorem category_theory.limits.equalizer.fork_π_app_zero {C : Type u} {X Y : C} (f g : X Y)  :
theorem category_theory.limits.equalizer.condition_assoc {C : Type u} {X Y : C} (f g : X Y) {X' : C} (f' : Y X') :
f f' = g f'
theorem category_theory.limits.equalizer.condition {C : Type u} {X Y : C} (f g : X Y)  :
noncomputable def category_theory.limits.equalizer_is_equalizer {C : Type u} {X Y : C} (f g : X Y)  :

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

Equations
@[reducible]
noncomputable def category_theory.limits.equalizer.lift {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : W X) (h : k f = k 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.

@[simp]
theorem category_theory.limits.equalizer.lift_ι_assoc {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : W X) (h : k f = k g) {X' : C} (f' : X X') :
= k f'
@[simp]
theorem category_theory.limits.equalizer.lift_ι {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : W X) (h : k f = k g) :
noncomputable def category_theory.limits.equalizer.lift' {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : W X) (h : k f = k g) :
{l // = 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
@[ext]
theorem category_theory.limits.equalizer.hom_ext {C : Type u} {X Y : C} {f g : X Y} {W : C} {k l : W } (h : = ) :
k = l

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

theorem category_theory.limits.equalizer.exists_unique {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : W X) (h : k f = k g) :
∃! (l : ,
@[protected, instance]
def category_theory.limits.equalizer.ι_mono {C : Type u} {X Y : C} {f g : X Y}  :

An equalizer morphism is a monomorphism

theorem category_theory.limits.mono_of_is_limit_fork {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

The equalizer morphism in any limit cone is a monomorphism.

def category_theory.limits.id_fork {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

Equations
def category_theory.limits.is_limit_id_fork {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

Equations
theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_eq {C : Type u} {X Y : C} {f g : X Y} (h₀ : f = g) {c : g}  :

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

theorem category_theory.limits.equalizer.ι_of_eq {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_self {C : Type u} {X Y : C} {f : X Y} {c : f}  :

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

theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_epi {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

An equalizer that is an epimorphism is an isomorphism.

theorem category_theory.limits.eq_of_epi_fork_ι {C : Type u} {X Y : C} {f g : X Y} (t : g)  :
f = g

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

theorem category_theory.limits.eq_of_epi_equalizer {C : Type u} {X Y : C} {f g : X Y}  :
f = g

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

@[protected, instance]
def category_theory.limits.has_equalizer_of_self {C : Type u} {X Y : C} (f : X Y) :
@[protected, instance]
def category_theory.limits.equalizer.ι_of_self {C : Type u} {X Y : C} (f : X Y) :

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

noncomputable def category_theory.limits.equalizer.iso_source_of_self {C : Type u} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.limits.equalizer.iso_source_of_self_hom {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.limits.equalizer.iso_source_of_self_inv {C : Type u} {X Y : C} (f : X Y) :
@[reducible]
def category_theory.limits.has_coequalizer {C : Type u} {X Y : C} (f g : X Y) :
Prop

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

@[reducible]
noncomputable def category_theory.limits.coequalizer {C : Type u} {X Y : C} (f g : X Y)  :
C

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

@[reducible]
noncomputable def category_theory.limits.coequalizer.π {C : Type u} {X Y : C} (f g : X Y)  :

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

@[reducible]
noncomputable def category_theory.limits.coequalizer.cofork {C : Type u} {X Y : C} (f g : X Y)  :

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

@[simp]
theorem category_theory.limits.coequalizer.cofork_π {C : Type u} {X Y : C} (f g : X Y)  :
@[simp]
theorem category_theory.limits.coequalizer.cofork_ι_app_one {C : Type u} {X Y : C} (f g : X Y)  :
theorem category_theory.limits.coequalizer.condition {C : Type u} {X Y : C} (f g : X Y)  :
theorem category_theory.limits.coequalizer.condition_assoc {C : Type u} {X Y : C} (f g : X Y) {X' : C} (f' : X') :
=
noncomputable def category_theory.limits.coequalizer_is_coequalizer {C : Type u} {X Y : C} (f g : X Y)  :

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

Equations
@[reducible]
noncomputable def category_theory.limits.coequalizer.desc {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : Y W) (h : f k = g k) :

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.

@[simp]
theorem category_theory.limits.coequalizer.π_desc {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : Y W) (h : f k = g k) :
@[simp]
theorem category_theory.limits.coequalizer.π_desc_assoc {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : Y W) (h : f k = g k) {X' : C} (f' : W X') :
theorem category_theory.limits.coequalizer.π_colim_map_desc {C : Type u} {X Y : C} {f g : X Y} {X' Y' Z : C} (f' g' : X' Y') (p : X X') (q : Y Y') (wf : f q = p f') (wg : g q = p g') (h : Y' Z) (wh : f' h = g' h) :
= q h
noncomputable def category_theory.limits.coequalizer.desc' {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : Y W) (h : f k = g k) :
{l //

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

Equations
@[ext]
theorem category_theory.limits.coequalizer.hom_ext {C : Type u} {X Y : C} {f g : X Y} {W : C} {k l : W} (h : = ) :
k = l

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

theorem category_theory.limits.coequalizer.exists_unique {C : Type u} {X Y : C} {f g : X Y} {W : C} (k : Y W) (h : f k = g k) :
∃! (d : ,
@[protected, instance]
def category_theory.limits.coequalizer.π_epi {C : Type u} {X Y : C} {f g : X Y}  :

A coequalizer morphism is an epimorphism

theorem category_theory.limits.epi_of_is_colimit_cofork {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

The coequalizer morphism in any colimit cocone is an epimorphism.

def category_theory.limits.id_cofork {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

Equations
def category_theory.limits.is_colimit_id_cofork {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

Equations
• = category_theory.limits.is_colimit_id_cofork._proof_1 _
theorem category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_eq {C : Type u} {X Y : C} {f g : X Y} (h₀ : f = g) {c : g}  :

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

theorem category_theory.limits.coequalizer.π_of_eq {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

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

theorem category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_self {C : Type u} {X Y : C} {f : X Y} {c : f}  :

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

theorem category_theory.limits.is_iso_limit_cocone_parallel_pair_of_epi {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

A coequalizer that is a monomorphism is an isomorphism.

theorem category_theory.limits.eq_of_mono_cofork_π {C : Type u} {X Y : C} {f g : X Y} (t : g)  :
f = g

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

theorem category_theory.limits.eq_of_mono_coequalizer {C : Type u} {X Y : C} {f g : X Y}  :
f = g

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

@[protected, instance]
def category_theory.limits.has_coequalizer_of_self {C : Type u} {X Y : C} (f : X Y) :
@[protected, instance]
def category_theory.limits.coequalizer.π_of_self {C : Type u} {X Y : C} (f : X Y) :

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

noncomputable def category_theory.limits.coequalizer.iso_target_of_self {C : Type u} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.limits.coequalizer.iso_target_of_self_hom {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.limits.coequalizer.iso_target_of_self_inv {C : Type u} {X Y : C} (f : X Y) :
noncomputable def category_theory.limits.equalizer_comparison {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] :
(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 category_theory/limits/preserves/shapes/equalizers.lean

Equations
Instances for category_theory.limits.equalizer_comparison
@[simp]
theorem category_theory.limits.equalizer_comparison_comp_π {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] :
=
@[simp]
theorem category_theory.limits.equalizer_comparison_comp_π_assoc {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {X' : D} (f' : G.obj X X') :
(G.map g) f' = f'
@[simp]
theorem category_theory.limits.map_lift_equalizer_comparison {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {Z : C} {h : Z X} (w : h f = h g) :
@[simp]
theorem category_theory.limits.map_lift_equalizer_comparison_assoc {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {Z : C} {h : Z X} (w : h f = h g) {X' : D} (f' : (G.map g) X') :
= f'
noncomputable def category_theory.limits.coequalizer_comparison {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] :
(G.map g)

The comparison morphism for the coequalizer of f,g.

Equations
Instances for category_theory.limits.coequalizer_comparison
@[simp]
theorem category_theory.limits.ι_comp_coequalizer_comparison_assoc {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {X' : D} (f' : X') :
(G.map g) = f'
@[simp]
theorem category_theory.limits.ι_comp_coequalizer_comparison {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] :
@[simp]
theorem category_theory.limits.coequalizer_comparison_map_desc {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {Z : C} {h : Y Z} (w : f h = g h) :
@[simp]
theorem category_theory.limits.coequalizer_comparison_map_desc_assoc {C : Type u} {X Y : C} (f g : X Y) {D : Type u₂} (G : C D) [ (G.map g)] {Z : C} {h : Y Z} (w : f h = g h) {X' : D} (f' : G.obj Z X') :
= f'
@[reducible]

has_equalizers represents a choice of equalizer for every pair of morphisms

@[reducible]

has_coequalizers represents a choice of coequalizer for every pair of morphisms

theorem category_theory.limits.has_equalizers_of_has_limit_parallel_pair (C : Type u) [ {X Y : C} {f g : X Y}, ] :

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

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

@[simp]
theorem category_theory.limits.cone_of_is_split_mono_π_app {C : Type u} {X Y : C} (f : X Y)  :
= X_1.cases_on f (f 𝟙 Y)
noncomputable def category_theory.limits.cone_of_is_split_mono {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.cone_of_is_split_mono_X {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.cone_of_is_split_mono_ι {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.is_split_mono_equalizes {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
def category_theory.limits.split_mono_of_equalizer (C : Type u) {X Y : C} {f : X Y} {r : Y X} (hr : f r f = f)  :

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

Equations
def category_theory.limits.is_equalizer_comp_mono {C : Type u} {X Y : C} {f g : X Y} {c : g} {Z : C} (h : Y Z) [hm : category_theory.mono h] :

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

Equations
• = (λ (s : (g h)), let s' : := , l : {l // l c.ι = s'.ι} := in l.val, _⟩)
@[instance]
theorem category_theory.limits.has_equalizer_comp_mono (C : Type u) {X Y : C} (f g : X Y) {Z : C} (h : Y Z)  :
(g h)
def category_theory.limits.split_mono_of_idempotent_of_is_limit_fork (C : Type u) {X : C} {f : X X} (hf : f f = f) {c : f}  :

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

Equations
@[simp]
theorem category_theory.limits.split_mono_of_idempotent_of_is_limit_fork_retraction (C : Type u) {X : C} {f : X X} (hf : f f = f) {c : f}  :
noncomputable def category_theory.limits.split_mono_of_idempotent_equalizer (C : Type u) {X : C} {f : X X} (hf : f f = f)  :

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

Equations
@[simp]
theorem category_theory.limits.cocone_of_is_split_epi_ι_app {C : Type u} {X Y : C} (f : X Y)  :
= X_1.cases_on (𝟙 X f) f
noncomputable def category_theory.limits.cocone_of_is_split_epi {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.cocone_of_is_split_epi_X {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.cocone_of_is_split_epi_π {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.is_split_epi_coequalizes {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
def category_theory.limits.split_epi_of_coequalizer (C : Type u) {X Y : C} {f : X Y} {s : Y X} (hs : f s f = f)  :

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

Equations
def category_theory.limits.is_coequalizer_epi_comp {C : Type u} {X Y : C} {f g : X Y} {c : g} {W : C} (h : W X) [hm : category_theory.epi h] :

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

Equations
• = (λ (s : (h g)), let s' : := , l : {l // c.π l = s'.π} := in l.val, _⟩)
theorem category_theory.limits.has_coequalizer_epi_comp {C : Type u} {X Y : C} {f g : X Y} {W : C} (h : W X) [hm : category_theory.epi h] :
(h g)
def category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork (C : Type u) {X : C} {f : X X} (hf : f f = f) {c : f}  :

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

Equations
@[simp]
theorem category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork_section_ (C : Type u) {X : C} {f : X X} (hf : f f = f) {c : f}  :
noncomputable def category_theory.limits.split_epi_of_idempotent_coequalizer (C : Type u) {X : C} {f : X X} (hf : f f = f)  :

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

Equations