# mathlib3documentation

category_theory.limits.preserves.shapes.equalizers

# Preserving (co)equalizers #

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

Constructions to relate the notions of preserving (co)equalizers and reflecting (co)equalizers to concrete (co)forks.

In particular, we show that equalizer_comparison f g G is an isomorphism iff G preserves the limit of the parallel pair f,g, as well as the dual result.

def category_theory.limits.is_limit_map_cone_fork_equiv {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Z X} (w : h f = h g) :

The map of a fork is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute fork.of_ι with functor.map_cone.

Equations
def category_theory.limits.is_limit_fork_map_of_is_limit {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Z X} (w : h f = h g)  :

The property of preserving equalizers expressed in terms of forks.

Equations
def category_theory.limits.is_limit_of_is_limit_fork_map {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Z X} (w : h f = h g)  :

The property of reflecting equalizers expressed in terms of forks.

Equations
noncomputable def category_theory.limits.is_limit_of_has_equalizer_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y)  :

If G preserves equalizers and C has them, then the fork constructed of the mapped morphisms of a fork is a limit.

Equations
noncomputable def category_theory.limits.preserves_equalizer.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :

If the equalizer comparison map for G at (f,g) is an isomorphism, then G preserves the equalizer of (f,g).

Equations
noncomputable def category_theory.limits.preserves_equalizer.iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
(G.map g)

If G preserves the equalizer of (f,g), then the equalizer comparison map for G at (f,g) is an isomorphism.

Equations
@[simp]
theorem category_theory.limits.preserves_equalizer.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
@[protected, instance]
def category_theory.limits.equalizer_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
def category_theory.limits.is_colimit_map_cocone_cofork_equiv {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Y Z} (w : f h = g h) :

The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute cofork.of_π with functor.map_cocone.

Equations
def category_theory.limits.is_colimit_cofork_map_of_is_colimit {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Y Z} (w : f h = g h)  :

The property of preserving coequalizers expressed in terms of coforks.

Equations
def category_theory.limits.is_colimit_of_is_colimit_cofork_map {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f g : X Y} {h : Y Z} (w : f h = g h)  :

The property of reflecting coequalizers expressed in terms of coforks.

Equations
noncomputable def category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y)  :

If G preserves coequalizers and C has them, then the cofork constructed of the mapped morphisms of a cofork is a colimit.

Equations
noncomputable def category_theory.limits.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :

If the coequalizer comparison map for G at (f,g) is an isomorphism, then G preserves the coequalizer of (f,g).

Equations
noncomputable def category_theory.limits.preserves_coequalizer.iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
(G.map g)

If G preserves the coequalizer of (f,g), then the coequalizer comparison map for G at (f,g) is an isomorphism.

Equations
@[simp]
theorem category_theory.limits.preserves_coequalizer.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
@[protected, instance]
def category_theory.limits.coequalizer_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
@[protected, instance]
def category_theory.limits.map_π_epi {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
theorem category_theory.limits.map_π_preserves_coequalizer_inv_assoc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {X' : D} (f' : (G.map g) X') :
= (G.map g) f'
theorem category_theory.limits.map_π_preserves_coequalizer_inv {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)]  :
= (G.map g)
theorem category_theory.limits.map_π_preserves_coequalizer_inv_desc_assoc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {W : D} (k : G.obj Y W) (wk : G.map f k = G.map g k) {X' : D} (f' : W X') :
= k f'
theorem category_theory.limits.map_π_preserves_coequalizer_inv_desc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {W : D} (k : G.obj Y W) (wk : G.map f k = G.map g k) :
theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {X' Y' : D} (f' g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : G.map f q = p f') (wg : G.map g q = p g') :
category_theory.limits.colim_map (G.map g) f' g' p q wf wg) =
theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_assoc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {X' Y' : D} (f' g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : G.map f q = p f') (wg : G.map g q = p g') {X'_1 : D} (f'_1 : X'_1) :
category_theory.limits.colim_map (G.map g) f' g' p q wf wg) f'_1 = q f'_1
theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_desc_assoc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {X' Y' : D} (f' g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : G.map f q = p f') (wg : G.map g q = p g') {Z' : D} (h : Y' Z') (wh : f' h = g' h) {X'_1 : D} (f'_1 : Z' X'_1) :
category_theory.limits.colim_map (G.map g) f' g' p q wf wg) = q h f'_1
theorem category_theory.limits.map_π_preserves_coequalizer_inv_colim_map_desc {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y) [ (G.map g)] {X' Y' : D} (f' g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : G.map f q = p f') (wg : G.map g q = p g') {Z' : D} (h : Y' Z') (wh : f' h = g' h) :
category_theory.limits.colim_map (G.map g) f' g' p q wf wg) = q h
@[protected, instance]
noncomputable def category_theory.limits.preserves_split_coequalizers {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f g : X Y)  :

Any functor preserves coequalizers of split pairs.

Equations