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

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

The property of reflecting equalizers expressed in terms of forks.

Equations

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

def CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] [PreservesLimit (parallelPair f g) G] : IsLimit (Fork.ofι (G.map (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)

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

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

@[simp]

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

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

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

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

The property of reflecting coequalizers expressed in terms of coforks.

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[instance 1]

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

Any functor preserves coequalizers of split pairs.

@[instance 1]

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