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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.Fork.ofι h w)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯)

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.

def CategoryTheory.Limits.isLimitForkMapOfIsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι h w)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯)

The property of preserving equalizers expressed in terms of forks.

Equations

• CategoryTheory.Limits.isLimitForkMapOfIsLimit G w l = (CategoryTheory.Limits.isLimitMapConeForkEquiv G w) (CategoryTheory.Limits.PreservesLimit.preserves l)

def CategoryTheory.Limits.isLimitOfIsLimitForkMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) G] (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι h w)

The property of reflecting equalizers expressed in terms of forks.

Equations

• CategoryTheory.Limits.isLimitOfIsLimitForkMap G w l = CategoryTheory.Limits.ReflectsLimit.reflects ((CategoryTheory.Limits.isLimitMapConeForkEquiv G w).symm l)

def CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map (CategoryTheory.Limits.equalizer.ι f g)) ⋯)

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

Equations

• CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit G f g = CategoryTheory.Limits.isLimitForkMapOfIsLimit G ⋯ (CategoryTheory.Limits.equalizerIsEqualizer f g)

def CategoryTheory.Limits.PreservesEqualizer.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) 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.

def CategoryTheory.Limits.PreservesEqualizer.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : G.obj (CategoryTheory.Limits.equalizer f g) ≅ 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.

@[simp]

theorem CategoryTheory.Limits.PreservesEqualizer.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : (CategoryTheory.Limits.PreservesEqualizer.iso G f g).hom = CategoryTheory.Limits.equalizerComparison f g G

@[simp]

theorem CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesEqualizer.iso G f g).inv (G.map (CategoryTheory.Limits.equalizer.ι f g)) = CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)

instance CategoryTheory.Limits.instIsIsoEqualizerComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofork.ofπ h w)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map 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.mapCocone.

Equations

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

def CategoryTheory.Limits.isColimitCoforkMapOfIsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ h w)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯)

The property of preserving coequalizers expressed in terms of coforks.

Equations

• CategoryTheory.Limits.isColimitCoforkMapOfIsColimit G w l = (CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv G w) (CategoryTheory.Limits.PreservesColimit.preserves l)

def CategoryTheory.Limits.isColimitOfIsColimitCoforkMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G] (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ h w)

The property of reflecting coequalizers expressed in terms of coforks.

Equations

• CategoryTheory.Limits.isColimitOfIsColimitCoforkMap G w l = CategoryTheory.Limits.ReflectsColimit.reflects ((CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv G w).symm l)

def CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.coequalizer.π f g)) ⋯)

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

Equations

• CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit G f g = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit G ⋯ (CategoryTheory.Limits.coequalizerIsCoequalizer f g)

def CategoryTheory.Limits.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.coequalizerComparison f g G)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) 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.

def CategoryTheory.Limits.PreservesCoequalizer.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ≅ G.obj (CategoryTheory.Limits.coequalizer f g)

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.

@[simp]

theorem CategoryTheory.Limits.PreservesCoequalizer.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).hom = CategoryTheory.Limits.coequalizerComparison f g G

instance CategoryTheory.Limits.instIsIsoCoequalizerComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.IsIso (CategoryTheory.Limits.coequalizerComparison f g G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.map_π_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.Epi (G.map (CategoryTheory.Limits.coequalizer.π f g))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {Z : D} (h : CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)) h

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv = CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) 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) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc k wk) h)) = CategoryTheory.CategoryStruct.comp k h

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {W : D} (k : G.obj Y ⟶ W) (wk : CategoryTheory.CategoryStruct.comp (G.map f) k = CategoryTheory.CategoryStruct.comp (G.map g) k) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.Limits.coequalizer.desc k wk)) = k

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' : D} {Y' : D} (f' : X' ⟶ Y') (g' : X' ⟶ Y') [CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z : D} (h : CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair f' g') ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)) h)) = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f' g') h)

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' : D} {Y' : D} (f' : X' ⟶ Y') (g' : X' ⟶ Y') [CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))) = CategoryTheory.CategoryStruct.comp q (CategoryTheory.Limits.coequalizer.π f' g')

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' : D} {Y' : D} (f' : X' ⟶ Y') (g' : X' ⟶ Y') [CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z' : D} (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h✝ = CategoryTheory.CategoryStruct.comp g' h✝) {Z : D} (h : Z' ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc h✝ wh) h))) = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp h✝ h)

theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' : D} {Y' : D} (f' : X' ⟶ Y') (g' : X' ⟶ Y') [CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z' : D} (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh))) = CategoryTheory.CategoryStruct.comp q h

@[instance 1]

instance CategoryTheory.Limits.preservesSplitCoequalizers {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.HasSplitCoequalizer f g] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

Any functor preserves coequalizers of split pairs.

Equations

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

@[instance 1]

instance CategoryTheory.Limits.preservesSplitEqualizers {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.HasSplitEqualizer f g] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G

Equations

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