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_pairis the indexing category used for (co)equalizer_diagramsparallel_pairis a functor fromwalking_parallel_pairto our categoryC.- a
forkis 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.ι.
- 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
- an
equalizeris now just alimit (parallel_pair f g)
Each of these has a dual.
Main statements
equalizer.ι_monostates that every equalizer map is a monomorphismis_iso_limit_cone_parallel_pair_of_selfstates that the identity on the domain offis an equalizer offandf.
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][borceux-vol1]
- zero : category_theory.limits.walking_parallel_pair
- one : category_theory.limits.walking_parallel_pair
The type of objects for the diagram indexing a (co)equalizer.
- left : category_theory.limits.walking_parallel_pair_hom category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one
- right : category_theory.limits.walking_parallel_pair_hom category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one
- id : Π (X : category_theory.limits.walking_parallel_pair), category_theory.limits.walking_parallel_pair_hom X X
The type family of morphisms for the diagram indexing a (co)equalizer.
Composition of morphisms in the indexing diagram for (co)equalizers.
Equations
- category_theory.limits.walking_parallel_pair_hom.comp _x _x _x_1 (category_theory.limits.walking_parallel_pair_hom.id _x) h = h
- category_theory.limits.walking_parallel_pair_hom.comp category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair_hom.right (category_theory.limits.walking_parallel_pair_hom.id category_theory.limits.walking_parallel_pair.one) = category_theory.limits.walking_parallel_pair_hom.right
- category_theory.limits.walking_parallel_pair_hom.comp category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair_hom.left (category_theory.limits.walking_parallel_pair_hom.id category_theory.limits.walking_parallel_pair.one) = category_theory.limits.walking_parallel_pair_hom.left
Equations
- category_theory.limits.walking_parallel_pair_hom_category = {to_category_struct := {to_has_hom := {hom := category_theory.limits.walking_parallel_pair_hom}, id := category_theory.limits.walking_parallel_pair_hom.id, comp := category_theory.limits.walking_parallel_pair_hom.comp}, id_comp' := category_theory.limits.walking_parallel_pair_hom_category._proof_1, comp_id' := category_theory.limits.walking_parallel_pair_hom_category._proof_2, assoc' := category_theory.limits.walking_parallel_pair_hom_category._proof_3}
parallel_pair f g is the diagram in C consisting of the two morphisms f and g with
common domain and codomain.
Equations
- category_theory.limits.parallel_pair f g = {obj := λ (x : category_theory.limits.walking_parallel_pair), category_theory.limits.parallel_pair._match_1 x, map := λ (x y : category_theory.limits.walking_parallel_pair) (h : x ⟶ y), category_theory.limits.parallel_pair._match_2 f g x y h, map_id' := _, map_comp' := _}
- category_theory.limits.parallel_pair._match_1 category_theory.limits.walking_parallel_pair.one = Y
- category_theory.limits.parallel_pair._match_1 category_theory.limits.walking_parallel_pair.zero = X
- category_theory.limits.parallel_pair._match_2 f g _x _x (category_theory.limits.walking_parallel_pair_hom.id _x) = 𝟙 (category_theory.limits.parallel_pair._match_1 _x)
- category_theory.limits.parallel_pair._match_2 f g category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair_hom.right = g
- category_theory.limits.parallel_pair._match_2 f g category_theory.limits.walking_parallel_pair.zero category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair_hom.left = f
Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
parallel_pair
A fork on f and g is just a cone (parallel_pair f g).
A cofork on f and g is just a cocone (parallel_pair f g).
A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.
Equations
- category_theory.limits.fork.of_ι ι w = {X := P, π := {app := λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on ι (ι ≫ f), naturality' := _}}
A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying
f ≫ π = g ≫ π.
Equations
- category_theory.limits.cofork.of_π π w = {X := P, ι := {app := λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on (f ≫ π) π, naturality' := _}}
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.
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.
To check whether two maps are equalized by both maps of a fork, it suffices to check it for the first map
To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for the second map
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
- category_theory.limits.fork.is_limit.lift' hs k h = ⟨hs.lift (category_theory.limits.fork.of_ι k h), _⟩
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
- category_theory.limits.cofork.is_colimit.desc' hs k h = ⟨hs.desc (category_theory.limits.cofork.of_π k h), _⟩
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
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
- category_theory.limits.fork.is_limit.mk' t create = category_theory.limits.fork.is_limit.mk t (λ (s : category_theory.limits.fork f g), (create s).val) _ _
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
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
- category_theory.limits.cofork.is_colimit.mk' t create = category_theory.limits.cofork.is_colimit.mk t (λ (s : category_theory.limits.cofork f g), (create s).val) _ _
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
- category_theory.limits.cone.of_fork t = {X := t.X, π := {app := λ (X : category_theory.limits.walking_parallel_pair), t.π.app X ≫ category_theory.eq_to_hom _, naturality' := _}}
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
- category_theory.limits.cocone.of_cofork t = {X := t.X, ι := {app := λ (X : category_theory.limits.walking_parallel_pair), category_theory.eq_to_hom _ ≫ t.ι.app X, naturality' := _}}
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
- category_theory.limits.fork.of_cone t = {X := t.X, π := {app := λ (X : category_theory.limits.walking_parallel_pair), t.π.app X ≫ category_theory.eq_to_hom _, naturality' := _}}
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
- category_theory.limits.cofork.of_cocone t = {X := t.X, ι := {app := λ (X : category_theory.limits.walking_parallel_pair), category_theory.eq_to_hom _ ≫ t.ι.app X, naturality' := _}}
Helper function for constructing morphisms between equalizer forks.
Equations
- category_theory.limits.fork.mk_hom k w = {hom := k, w' := _}
has_equalizer f g represents a particular choice of limiting cone
for the parallel pair of morphisms f and g.
If we have chosen an equalizer of f and g, we can access the corresponding object by
saying equalizer f g.
If we have chosen an equalizer of f and g, we can access the inclusion
equalizer f g ⟶ X by saying equalizer.ι f g.
The chosen equalizer cone for a parallel pair f and 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.
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
Two maps into an equalizer are equal if they are are equal when composed with the equalizer map.
An equalizer morphism is a monomorphism
Equations
The equalizer morphism in any limit cone is a monomorphism.
The identity determines a cone on the equalizer diagram of f and g if f = g.
Equations
The identity on X is an equalizer of (f, g), if f = g.
Equations
Every equalizer of (f, g), where f = g, is an isomorphism.
The equalizer of (f, g), where f = g, is an isomorphism.
Every equalizer of (f, f) is an isomorphism.
Equations
- category_theory.limits.is_iso_limit_cone_parallel_pair_of_self h = category_theory.limits.is_iso_limit_cone_parallel_pair_of_eq category_theory.limits.is_iso_limit_cone_parallel_pair_of_self._proof_1 h
An equalizer that is an epimorphism is an isomorphism.
Equations
- category_theory.limits.is_iso_limit_cone_parallel_pair_of_epi h = category_theory.limits.is_iso_limit_cone_parallel_pair_of_eq category_theory.limits.is_iso_limit_cone_parallel_pair_of_epi._proof_1 h
The equalizer inclusion for (f, f) is an isomorphism.
The equalizer of a morphism with itself is isomorphic to the source.
Helper function for constructing morphisms between coequalizer coforks.
Equations
- category_theory.limits.cofork.mk_hom f g k w = {hom := k, w' := _}
has_coequalizer f g represents a particular choice of colimiting cocone
for the parallel pair of morphisms f and g.
If we have chosen a coequalizer of f and g, we can access the corresponding object by
saying coequalizer f g.
If we have chosen a coequalizer of f and g, we can access the corresponding projection by
saying coequalizer.π f g.
The chosen coequalizer cocone for a parallel pair f and g.
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.
Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism
l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.
Equations
Two maps from a coequalizer are equal if they are equal when composed with the coequalizer map
A coequalizer morphism is an epimorphism
Equations
The coequalizer morphism in any colimit cocone is an epimorphism.
The identity determines a cocone on the coequalizer diagram of f and g, if f = g.
Equations
The identity on Y is a coequalizer of (f, g), where f = g.
Equations
- category_theory.limits.is_colimit_id_cofork h = category_theory.limits.cofork.is_colimit.mk (category_theory.limits.id_cofork h) (λ (s : category_theory.limits.cofork f g), s.π) category_theory.limits.is_colimit_id_cofork._proof_1 _
Every coequalizer of (f, g), where f = g, is an isomorphism.
The coequalizer of (f, g), where f = g, is an isomorphism.
Every coequalizer of (f, f) is an isomorphism.
Equations
- category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_self h = category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_eq category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_self._proof_1 h
A coequalizer that is a monomorphism is an isomorphism.
Equations
- category_theory.limits.is_iso_limit_cocone_parallel_pair_of_epi h = category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_eq category_theory.limits.is_iso_limit_cocone_parallel_pair_of_epi._proof_1 h
The coequalizer projection for (f, f) is an isomorphism.
The coequalizer of a morphism with itself is isomorphic to the target.
has_equalizers represents a choice of equalizer for every pair of morphisms
has_coequalizers represents a choice of coequalizer for every pair of morphisms
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
A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).
Here we build the cone, and show in split_mono_equalizes that it is a limit cone.
A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).
Equations
A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).
Here we build the cocone, and show in split_epi_coequalizes that it is a colimit cocone.
A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).
Equations
- category_theory.limits.split_epi_coequalizes f = {desc := λ (s : category_theory.limits.cocone (category_theory.limits.parallel_pair (𝟙 X) (f ≫ category_theory.section_ f))), category_theory.section_ f ≫ s.ι.app category_theory.limits.walking_parallel_pair.one, fac' := _, uniq' := _}