# mathlibdocumentation

category_theory.limits.shapes.equalizers

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

• `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 `abbreviation`s 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 : , {l // ) :

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
• = (λ (_x : ∀ (s : , (λ (l : s.X t.X), l t.ι = s.ι) ((λ (s : , s) ∀ (y : s.X t.X), (λ (l : s.X t.X), l t.ι = s.ι) yy = (λ (s : , s), (λ (s : , _ _) _
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
• = (λ (_x : ∀ (s : , (λ (d : t.X s.X), t.π d = s.π) ((λ (s : , s) ∀ (y : t.X s.X), (λ (d : t.X s.X), t.π d = s.π) yy = (λ (s : , s), _ _) _
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]
theorem category_theory.limits.fork.of_cone_π {C : Type u}  :
@[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') :
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]
def category_theory.limits.has_equalizers (C : Type u)  :
Prop

`has_equalizers` represents a choice of equalizer for every pair of morphisms

@[reducible]
def category_theory.limits.has_coequalizers (C : Type u)  :
Prop

`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

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

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