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_diagramsparallel_pair
is a functor fromwalking_parallel_pair
to our categoryC
.- 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.ι
.
- 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
equalizer
is now just alimit (parallel_pair f g)
Each of these has a dual.
Main statements #
equalizer.ι_mono
states that every equalizer map is a monomorphismis_iso_limit_cone_parallel_pair_of_self
states that the identity on the domain off
is an equalizer off
andf
.
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 #
- 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.
Instances for category_theory.limits.walking_parallel_pair
- category_theory.limits.has_equalizers_of_has_wide_equalizers
- category_theory.limits.has_coequalizers_of_has_wide_coequalizers
- category_theory.normal_mono_category.has_equalizers
- category_theory.normal_epi_category.has_coequalizers
- category_theory.abelian.has_equalizers
- category_theory.abelian.has_coequalizers
- category_theory.limits.walking_parallel_pair.has_sizeof_inst
- category_theory.limits.walking_parallel_pair.inhabited
- category_theory.limits.walking_parallel_pair_hom_category
- category_theory.limits.fintype_walking_parallel_pair
- category_theory.limits.walking_parallel_pair.category_theory.fin_category
- algebraic_geometry.LocallyRingedSpace.category_theory.limits.has_coequalizers
- algebraic_geometry.LocallyRingedSpace.preserves_coequalizer
- SemiNormedGroup.category_theory.limits.has_equalizers
- category_theory.parallel_pair_inhabited
- category_theory.parallel_pair_connected
- category_theory.over.category_theory.limits.has_equalizers
- ωCPO.category_theory.limits.has_equalizers
- 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.
Instances for category_theory.limits.walking_parallel_pair_hom
- category_theory.limits.walking_parallel_pair_hom.has_sizeof_inst
- category_theory.limits.walking_parallel_pair_hom.inhabited
- category_theory.limits.walking_parallel_pair_hom.fintype
Satisfying the inhabited linter
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_quiver := {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}
The functor walking_parallel_pair ⥤ walking_parallel_pairᵒᵖ
sending left to left and right to
right.
Equations
- category_theory.limits.walking_parallel_pair_op = {obj := λ (x : category_theory.limits.walking_parallel_pair), opposite.op (x.cases_on category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair.zero), map := λ (i j : category_theory.limits.walking_parallel_pair) (f : i ⟶ j), category_theory.limits.walking_parallel_pair_hom.cases_on f (λ (H_1 : i = category_theory.limits.walking_parallel_pair.zero), eq.rec (λ (f : category_theory.limits.walking_parallel_pair.zero ⟶ j) (H_2 : j = category_theory.limits.walking_parallel_pair.one), eq.rec (λ (f : category_theory.limits.walking_parallel_pair.zero ⟶ category_theory.limits.walking_parallel_pair.one) (H_3 : f == category_theory.limits.walking_parallel_pair_hom.left), eq.rec (quiver.hom.op category_theory.limits.walking_parallel_pair_hom.left) _) _ f) _ f) (λ (H_1 : i = category_theory.limits.walking_parallel_pair.zero), eq.rec (λ (f : category_theory.limits.walking_parallel_pair.zero ⟶ j) (H_2 : j = category_theory.limits.walking_parallel_pair.one), eq.rec (λ (f : category_theory.limits.walking_parallel_pair.zero ⟶ category_theory.limits.walking_parallel_pair.one) (H_3 : f == category_theory.limits.walking_parallel_pair_hom.right), eq.rec (quiver.hom.op category_theory.limits.walking_parallel_pair_hom.right) _) _ f) _ f) (λ (f_1 : category_theory.limits.walking_parallel_pair) (H_1 : i = f_1), eq.rec (λ (H_2 : j = i), eq.rec (λ (f : i ⟶ i) (H_3 : f == category_theory.limits.walking_parallel_pair_hom.id i), eq.rec (quiver.hom.op (category_theory.limits.walking_parallel_pair_hom.id (i.cases_on category_theory.limits.walking_parallel_pair.one category_theory.limits.walking_parallel_pair.zero))) _) _ f) H_1) _ _ _, map_id' := category_theory.limits.walking_parallel_pair_op._proof_5, map_comp' := category_theory.limits.walking_parallel_pair_op._proof_6}
The equivalence walking_parallel_pair ⥤ walking_parallel_pairᵒᵖ
sending left to left and right to
right.
Equations
- category_theory.limits.walking_parallel_pair_op_equiv = {functor := category_theory.limits.walking_parallel_pair_op, inverse := category_theory.limits.walking_parallel_pair_op.left_op, unit_iso := category_theory.nat_iso.of_components (λ (j : category_theory.limits.walking_parallel_pair), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_pair_op_equiv._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (j : category_theory.limits.walking_parallel_pairᵒᵖ), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_pair_op_equiv._proof_4, functor_unit_iso_comp' := category_theory.limits.walking_parallel_pair_op_equiv._proof_5}
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
Instances for category_theory.limits.parallel_pair
- category_theory.limits.has_coequalizer_of_has_split_coequalizer
- category_theory.limits.preserves_split_coequalizers
- category_theory.limits.has_reflexive_coequalizers.has_coeq
- category_theory.limits.has_coreflexive_equalizers.has_eq
- category_theory.limits.has_kernels.has_limit
- category_theory.limits.has_cokernels.has_colimit
- category_theory.limits.has_equalizer_of_self
- category_theory.limits.has_coequalizer_of_self
- category_theory.limits.has_equalizer_comp_mono
- category_theory.limits.has_kernel_comp_mono
- category_theory.limits.has_kernel_iso_comp
- category_theory.limits.has_cokernel_comp_iso
- category_theory.limits.has_cokernel_epi_comp
- category_theory.limits.multiequalizer.category_theory.limits.multicospan_index.snd_pi_map.category_theory.limits.has_equalizer
- category_theory.limits.multicoequalizer.category_theory.limits.multispan_index.snd_sigma_map.category_theory.limits.has_coequalizer
- category_theory.limits.category_theory.functor.map.has_kernel
- category_theory.limits.category_theory.functor.map.has_cokernel
- algebraic_geometry.LocallyRingedSpace.category_theory.limits.has_coequalizer
- SemiNormedGroup.has_limit_parallel_pair
- ωCPO.category_theory.limits.parallel_pair.category_theory.limits.has_limit
Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
parallel_pair
Construct a morphism between parallel pairs.
Equations
- category_theory.limits.parallel_pair_hom f g f' g' p q wf wg = {app := λ (j : category_theory.limits.walking_parallel_pair), category_theory.limits.parallel_pair_hom._match_1 f g f' g' p q j, naturality' := _}
- category_theory.limits.parallel_pair_hom._match_1 f g f' g' p q category_theory.limits.walking_parallel_pair.one = q
- category_theory.limits.parallel_pair_hom._match_1 f g f' g' p q category_theory.limits.walking_parallel_pair.zero = p
Construct a natural isomorphism between functors out of the walking parallel pair from its components.
Equations
- category_theory.limits.parallel_pair.ext zero one left right = category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_pair), X.cases_on zero one) _
Construct a natural isomorphism between parallel_pair f g
and parallel_pair f' g'
given
equalities f = f'
and g = g'
.
Equations
- category_theory.limits.parallel_pair.eq_of_hom_eq hf hg = category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair f g).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair f g).obj category_theory.limits.walking_parallel_pair.one)) _ _
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 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.ι
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
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' := _}}
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) _ _
Noncomputably make a limit cone from the existence of unique factorizations.
Equations
- category_theory.limits.fork.is_limit.of_exists_unique hs = (λ (_x : ∀ (s : category_theory.limits.fork f g), (λ (l : s.X ⟶ t.X), l ≫ t.ι = s.ι) ((λ (s : category_theory.limits.fork f g), classical.some _) s) ∧ ∀ (y : s.X ⟶ t.X), (λ (l : s.X ⟶ t.X), l ≫ t.ι = s.ι) y → y = (λ (s : category_theory.limits.fork f g), classical.some _) s), category_theory.limits.fork.is_limit.mk t (λ (s : category_theory.limits.fork f g), classical.some _) _ _) _
Noncomputably make a colimit cocone from the existence of unique factorizations.
Equations
- category_theory.limits.cofork.is_colimit.of_exists_unique hs = (λ (_x : ∀ (s : category_theory.limits.cofork f g), (λ (d : t.X ⟶ s.X), t.π ≫ d = s.π) ((λ (s : category_theory.limits.cofork f g), classical.some _) s) ∧ ∀ (y : t.X ⟶ s.X), (λ (d : t.X ⟶ s.X), t.π ≫ d = s.π) y → y = (λ (s : category_theory.limits.cofork f g), classical.some _) s), category_theory.limits.cofork.is_colimit.mk t (λ (s : category_theory.limits.cofork f g), classical.some _) _ _) _
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.
The bijection of fork.is_limit.hom_iso
is natural in Z
.
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.
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
- 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' := _}
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
- category_theory.limits.fork.ext i w = {hom := category_theory.limits.fork.mk_hom i.hom w, inv := category_theory.limits.fork.mk_hom i.inv _, hom_inv_id' := _, inv_hom_id' := _}
Every fork is isomorphic to one of the form fork.of_ι _ _
.
Equations
Helper function for constructing morphisms between coequalizer coforks.
Equations
- category_theory.limits.cofork.mk_hom k w = {hom := k, w' := _}
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
- category_theory.limits.cofork.ext i w = {hom := category_theory.limits.cofork.mk_hom i.hom w, inv := category_theory.limits.cofork.mk_hom i.inv _, hom_inv_id' := _, inv_hom_id' := _}
Every cofork is isomorphic to one of the form cofork.of_π _ _
.
Equations
has_equalizer f g
represents a particular choice of limiting cone
for the parallel pair of morphisms f
and g
.
If an equalizer of f
and g
exists, we can access an arbitrary choice of such by
saying equalizer f g
.
If an equalizer of f
and g
exists, we can access the inclusion
equalizer f g ⟶ X
by saying equalizer.ι f g
.
An equalizer cone for a parallel pair f
and g
.
The equalizer built from equalizer.ι f g
is limiting.
Equations
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
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.
An equalizer that is an epimorphism is an isomorphism.
Two morphisms are equal if there is a fork whose inclusion is epi.
If the equalizer of two morphisms is an epimorphism, then the two morphisms are equal.
The equalizer inclusion for (f, f)
is an isomorphism.
The equalizer of a morphism with itself is isomorphic to the source.
has_coequalizer f g
represents a particular choice of colimiting cocone
for the parallel pair of morphisms f
and g
.
If a coequalizer of f
and g
exists, we can access an arbitrary choice of such by
saying coequalizer f g
.
If a coequalizer of f
and g
exists, we can access the corresponding projection by
saying coequalizer.π f g
.
An arbitrary choice of coequalizer cocone for a parallel pair f
and g
.
The cofork built from coequalizer.π f g
is colimiting.
Equations
- category_theory.limits.coequalizer_is_coequalizer f g = (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair f g)).of_iso_colimit (category_theory.limits.cofork.ext (category_theory.iso.refl (category_theory.limits.colimit.cocone (category_theory.limits.parallel_pair f g)).X) _)
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
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.
A coequalizer that is a monomorphism is an isomorphism.
Two morphisms are equal if there is a cofork whose projection is mono.
If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal.
The coequalizer projection for (f, f)
is an isomorphism.
The coequalizer of a morphism with itself is isomorphic to the target.
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
The comparison morphism for the coequalizer of f,g
.
Equations
Instances for category_theory.limits.coequalizer_comparison
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 is_split_mono_equalizes
that it is a limit cone.
A split mono f
equalizes (retraction f ≫ f)
and (𝟙 Y)
.
Equations
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
- category_theory.limits.split_mono_of_equalizer C hr h = {retraction := r, id' := _}
The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.
Equations
- category_theory.limits.is_equalizer_comp_mono i h = category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι c.ι _) (λ (s : category_theory.limits.fork (f ≫ h) (g ≫ h)), let s' : category_theory.limits.fork f g := category_theory.limits.fork.of_ι s.ι _, l : {l // l ≫ c.ι = s'.ι} := category_theory.limits.fork.is_limit.lift' i s'.ι _ in ⟨l.val, _⟩)
An equalizer of an idempotent morphism and the identity is split mono.
Equations
- category_theory.limits.split_mono_of_idempotent_of_is_limit_fork C hf i = {retraction := i.lift (category_theory.limits.fork.of_ι f _), id' := _}
The equalizer of an idempotent morphism and the identity is split mono.
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.
A split epi f
coequalizes (f ≫ section_ f)
and (𝟙 X)
.
Equations
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
- category_theory.limits.split_epi_of_coequalizer C hs h = {section_ := s, id' := _}
The cofork obtained by precomposing a coequalizer cofork with an epimorphism is a coequalizer.
Equations
- category_theory.limits.is_coequalizer_epi_comp i h = category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cofork.of_π c.π _) (λ (s : category_theory.limits.cofork (h ≫ f) (h ≫ g)), let s' : category_theory.limits.cofork f g := category_theory.limits.cofork.of_π s.π _, l : {l // c.π ≫ l = s'.π} := category_theory.limits.cofork.is_colimit.desc' i s'.π _ in ⟨l.val, _⟩)
A coequalizer of an idempotent morphism and the identity is split epi.
Equations
- category_theory.limits.split_epi_of_idempotent_of_is_colimit_cofork C hf i = {section_ := i.desc (category_theory.limits.cofork.of_π f _), id' := _}
The coequalizer of an idempotent morphism and the identity is split epi.