# Preserving (co)equalizers #

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

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

def CategoryTheory.Limits.isLimitMapConeForkEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Z X} :

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.mapCone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.isLimitForkMapOfIsLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Z X} :

The property of preserving equalizers expressed in terms of forks.

Equations
Instances For
def CategoryTheory.Limits.isLimitOfIsLimitForkMap {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Z X} (l : ) :

The property of reflecting equalizers expressed in terms of forks.

Equations
Instances For
def CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (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
Instances For
def CategoryTheory.Limits.PreservesEqualizer.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer (G.map f) (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
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.PreservesEqualizer.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] :
G.obj CategoryTheory.Limits.equalizer (G.map f) (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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesEqualizer.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] :
@[simp]
theorem CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] :
instance CategoryTheory.Limits.instIsIsoEqualizerComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] :
Equations
• =
def CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Y Z} :

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.mapCocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.isColimitCoforkMapOfIsColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Y Z} :

The property of preserving coequalizers expressed in terms of coforks.

Equations
Instances For
def CategoryTheory.Limits.isColimitOfIsColimitCoforkMap {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} {h : Y Z} (l : ) :

The property of reflecting coequalizers expressed in terms of coforks.

Equations
Instances For
def CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (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
Instances For
def CategoryTheory.Limits.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (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
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.PreservesCoequalizer.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] :
CategoryTheory.Limits.coequalizer (G.map f) (G.map g) G.obj

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesCoequalizer.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] :
instance CategoryTheory.Limits.instIsIsoCoequalizerComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] :
Equations
• =
instance CategoryTheory.Limits.map_π_epi {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] :
Equations
• =
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {Z : D} (h : CategoryTheory.Limits.coequalizer (G.map f) (G.map g) Z) :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {W : D} (k : G.obj Y W) (wk : CategoryTheory.CategoryStruct.comp (G.map f) k = CategoryTheory.CategoryStruct.comp (G.map g) k) {Z : D} (h : W Z) :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {W : D} (k : G.obj Y W) (wk : CategoryTheory.CategoryStruct.comp (G.map f) k = CategoryTheory.CategoryStruct.comp (G.map g) k) :
= k
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {X' : D} {Y' : D} (f' : X' Y') (g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : ) (wg : ) {Z : D} (h : ) :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {X' : D} {Y' : D} (f' : X' Y') (g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : ) (wg : ) :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {X' : D} {Y' : D} (f' : X' Y') (g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : ) (wg : ) {Z' : D} (h : Y' Z') (wh : ) {Z : D} (h : Z' Z) :
theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {X' : D} {Y' : D} (f' : X' Y') (g' : X' Y') (p : G.obj X X') (q : G.obj Y Y') (wf : ) (wg : ) {Z' : D} (h : Y' Z') (wh : ) :
@[instance 1]
instance CategoryTheory.Limits.preservesSplitCoequalizers {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) (g : X Y) :

Any functor preserves coequalizers of split pairs.

Equations
• One or more equations did not get rendered due to their size.