Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

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.

source
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
    Instances For
      source
      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
        Instances For
          source
          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
            Instances For
              source
              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
                Instances For
                  source
                  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).

                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      @[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)
                      source
                      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)
                      source
                      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
                        Instances For
                          source
                          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
                            Instances For
                              source
                              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
                                Instances For
                                  source
                                  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
                                    Instances For
                                      source
                                      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).

                                      source
                                      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
                                        Instances For
                                          source
                                          @[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
                                          source
                                          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)
                                          source
                                          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))
                                          source
                                          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)
                                          source
                                          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
                                          source
                                          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
                                          source
                                          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
                                          source
                                          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')
                                          source
                                          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)
                                          source
                                          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
                                          source
                                          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✝)
                                          source
                                          @[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.

                                          source
                                          @[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