Documentation

Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Functors which preserves homology #

If F : C ⥤ D is a functor between categories with zero morphisms, we shall say that F preserves homology when F preserves both kernels and cokernels. This typeclass is named [F.PreservesHomology], and is automatically satisfied when F preserves both finite limits and finite colimits.

If S : ShortComplex C and [F.PreservesHomology], then there is an isomorphism S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology, which is part of the natural isomorphism homologyFunctorIso F between the functors F.mapShortComplex ⋙ homologyFunctor D and homologyFunctor C ⋙ F.

A functor preserves homology when it preserves both kernels and cokernels.

Instances

    A left homology data h of a short complex S is preserved by a functor F is F preserves the kernel of S.g : S.X₂ ⟶ S.X₃ and the cokernel of h.f' : S.X₁ ⟶ h.K.

    Instances

      When a left homology data is preserved by a functor F, this functor preserves the kernel of S.g : S.X₂ ⟶ S.X₃.

      When a left homology data h is preserved by a functor F, this functor preserves the cokernel of h.f' : S.X₁ ⟶ h.K.

      noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] :
      (S.map F).LeftHomologyData

      When a left homology data h of a short complex S is preserved by a functor F, this is the induced left homology data h.map F for the short complex S.map F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        def CategoryTheory.ShortComplex.LeftHomologyMapData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
        CategoryTheory.ShortComplex.LeftHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

        Given a left homology map data ψ : LeftHomologyMapData φ h₁ h₂ such that both left homology data h₁ and h₂ are preserved by a functor F, this is the induced left homology map data for the morphism F.mapShortComplex.map φ.

        Equations
        • ψ.map F = { φK := F.map ψ.φK, φH := F.map ψ.φH, commi := , commf' := , commπ := }
        Instances For
          @[simp]
          theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
          (ψ.map F).φH = F.map ψ.φH
          @[simp]
          theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
          (ψ.map F).φK = F.map ψ.φK

          A right homology data h of a short complex S is preserved by a functor F is F preserves the cokernel of S.f : S.X₁ ⟶ S.X₂ and the kernel of h.g' : h.Q ⟶ S.X₃.

          Instances

            When a right homology data is preserved by a functor F, this functor preserves the cokernel of S.f : S.X₁ ⟶ S.X₂.

            When a right homology data h is preserved by a functor F, this functor preserves the kernel of h.g' : h.Q ⟶ S.X₃.

            noncomputable def CategoryTheory.ShortComplex.RightHomologyData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] :
            (S.map F).RightHomologyData

            When a right homology data h of a short complex S is preserved by a functor F, this is the induced right homology data h.map F for the short complex S.map F.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              def CategoryTheory.ShortComplex.RightHomologyMapData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
              CategoryTheory.ShortComplex.RightHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

              Given a right homology map data ψ : RightHomologyMapData φ h₁ h₂ such that both right homology data h₁ and h₂ are preserved by a functor F, this is the induced right homology map data for the morphism F.mapShortComplex.map φ.

              Equations
              • ψ.map F = { φQ := F.map ψ.φQ, φH := F.map ψ.φH, commp := , commg' := , commι := }
              Instances For
                @[simp]
                theorem CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
                (ψ.map F).φQ = F.map ψ.φQ
                @[simp]
                theorem CategoryTheory.ShortComplex.RightHomologyMapData.map_φH {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
                (ψ.map F).φH = F.map ψ.φH
                noncomputable def CategoryTheory.ShortComplex.HomologyData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] :
                (S.map F).HomologyData

                When a homology data h of a short complex S is such that both h.left and h.right are preserved by a functor F, this is the induced homology data h.map F for the short complex S.map F.

                Equations
                • h.map F = { left := h.left.map F, right := h.right.map F, iso := F.mapIso h.iso, comm := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.ShortComplex.HomologyData.map_right {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] :
                  (h.map F).right = h.right.map F
                  @[simp]
                  theorem CategoryTheory.ShortComplex.HomologyData.map_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] :
                  (h.map F).iso = F.mapIso h.iso
                  @[simp]
                  theorem CategoryTheory.ShortComplex.HomologyData.map_left {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.left.IsPreservedBy F] [h.right.IsPreservedBy F] :
                  (h.map F).left = h.left.map F
                  def CategoryTheory.ShortComplex.HomologyMapData.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] :
                  CategoryTheory.ShortComplex.HomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)

                  Given a homology map data ψ : HomologyMapData φ h₁ h₂ such that h₁.left, h₁.right, h₂.left and h₂.right are all preserved by a functor F, this is the induced homology map data for the morphism F.mapShortComplex.map φ.

                  Equations
                  • ψ.map F = { left := ψ.left.map F, right := ψ.right.map F }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.ShortComplex.HomologyMapData.map_left {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] :
                    (ψ.map F).left = ψ.left.map F
                    @[simp]
                    theorem CategoryTheory.ShortComplex.HomologyMapData.map_right {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] :
                    (ψ.map F).right = ψ.right.map F

                    A functor preserves the left homology of a short complex S if it preserves all the left homology data of S.

                    • isPreservedBy (h : S.LeftHomologyData) : h.IsPreservedBy F

                      the functor preserves all the left homology data of the short complex

                    Instances

                      A functor preserves the right homology of a short complex S if it preserves all the right homology data of S.

                      • isPreservedBy (h : S.RightHomologyData) : h.IsPreservedBy F

                        the functor preserves all the right homology data of the short complex

                      Instances
                        theorem CategoryTheory.Functor.PreservesLeftHomologyOf.mk' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [h.IsPreservedBy F] :
                        F.PreservesLeftHomologyOf S

                        If a functor preserves a certain left homology data of a short complex S, then it preserves the left homology of S.

                        theorem CategoryTheory.Functor.PreservesRightHomologyOf.mk' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [h.IsPreservedBy F] :
                        F.PreservesRightHomologyOf S

                        If a functor preserves a certain right homology data of a short complex S, then it preserves the right homology of S.

                        instance CategoryTheory.ShortComplex.hasLeftHomology_of_preserves' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                        (F.mapShortComplex.obj S).HasLeftHomology
                        instance CategoryTheory.ShortComplex.hasRightHomology_of_preserves {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                        (S.map F).HasRightHomology
                        instance CategoryTheory.ShortComplex.hasRightHomology_of_preserves' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                        (F.mapShortComplex.obj S).HasRightHomology
                        instance CategoryTheory.ShortComplex.hasHomology_of_preserves {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
                        (S.map F).HasHomology
                        instance CategoryTheory.ShortComplex.hasHomology_of_preserves' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
                        (F.mapShortComplex.obj S).HasHomology
                        theorem CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] :
                        F.map (CategoryTheory.ShortComplex.cyclesMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
                        theorem CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] :
                        F.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
                        theorem CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] :
                        F.map (CategoryTheory.ShortComplex.opcyclesMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
                        theorem CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] :
                        F.map (CategoryTheory.ShortComplex.rightHomologyMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
                        theorem CategoryTheory.ShortComplex.HomologyData.map_homologyMap' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F] [h₂.right.IsPreservedBy F] :
                        F.map (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂) = CategoryTheory.ShortComplex.homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
                        noncomputable def CategoryTheory.ShortComplex.mapCyclesIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                        (S.map F).cycles F.obj S.cycles

                        When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).cycles ≅ F.obj S.cycles.

                        Equations
                        • S.mapCyclesIso F = (S.leftHomologyData.map F).cyclesIso
                        Instances For
                          @[simp]
                          theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                          CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (F.map S.iCycles) = (S.map F).iCycles
                          @[simp]
                          theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] {Z : D} (h : F.obj S.X₂ Z) :
                          noncomputable def CategoryTheory.ShortComplex.mapLeftHomologyIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                          (S.map F).leftHomology F.obj S.leftHomology

                          When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).leftHomology ≅ F.obj S.leftHomology.

                          Equations
                          • S.mapLeftHomologyIso F = (S.leftHomologyData.map F).leftHomologyIso
                          Instances For
                            noncomputable def CategoryTheory.ShortComplex.mapOpcyclesIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                            (S.map F).opcycles F.obj S.opcycles

                            When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).opcycles ≅ F.obj S.opcycles.

                            Equations
                            • S.mapOpcyclesIso F = (S.rightHomologyData.map F).opcyclesIso
                            Instances For
                              noncomputable def CategoryTheory.ShortComplex.mapRightHomologyIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                              (S.map F).rightHomology F.obj S.rightHomology

                              When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).rightHomology ≅ F.obj S.rightHomology.

                              Equations
                              • S.mapRightHomologyIso F = (S.rightHomologyData.map F).rightHomologyIso
                              Instances For
                                noncomputable def CategoryTheory.ShortComplex.mapHomologyIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] :
                                (S.map F).homology F.obj S.homology

                                When a functor F preserves the left homology of a short complex S, this is the canonical isomorphism (S.map F).homology ≅ F.obj S.homology.

                                Equations
                                • S.mapHomologyIso F = (S.homologyData.left.map F).homologyIso
                                Instances For
                                  noncomputable def CategoryTheory.ShortComplex.mapHomologyIso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesRightHomologyOf S] :
                                  (S.map F).homology F.obj S.homology

                                  When a functor F preserves the right homology of a short complex S, this is the canonical isomorphism (S.map F).homology ≅ F.obj S.homology.

                                  Equations
                                  • S.mapHomologyIso' F = (S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm
                                  Instances For
                                    theorem CategoryTheory.ShortComplex.LeftHomologyData.mapCyclesIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                                    S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm
                                    theorem CategoryTheory.ShortComplex.LeftHomologyData.mapLeftHomologyIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
                                    S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm
                                    theorem CategoryTheory.ShortComplex.RightHomologyData.mapOpcyclesIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                                    S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm
                                    theorem CategoryTheory.ShortComplex.RightHomologyData.mapRightHomologyIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
                                    S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm
                                    theorem CategoryTheory.ShortComplex.LeftHomologyData.mapHomologyIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] :
                                    S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm
                                    theorem CategoryTheory.ShortComplex.RightHomologyData.mapHomologyIso'_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [(S.map F).HasHomology] [F.PreservesRightHomologyOf S] :
                                    S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm
                                    theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ)) (S₂.mapCyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
                                    theorem CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.cycles Z) :
                                    theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) (S₂.mapCyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).cycles Z) :
                                    theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ)) (S₂.mapLeftHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
                                    theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.leftHomology Z) :
                                    theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) (S₂.mapLeftHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).leftHomology Z) :
                                    theorem CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ)) (S₂.mapOpcyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
                                    theorem CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.opcycles Z) :
                                    theorem CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (S₂.mapOpcyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).opcycles Z) :
                                    theorem CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ)) (S₂.mapRightHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
                                    theorem CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.rightHomology Z) :
                                    theorem CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) (S₂.mapRightHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).rightHomology Z) :
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.homology Z) :
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] {Z : D} (h : (S₂.map F).homology Z) :
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso' F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : F.obj S₂.homology Z) :
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
                                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso' F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology] [(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] {Z : D} (h : (S₂.map F).homology Z) :
                                    theorem CategoryTheory.ShortComplex.mapHomologyIso'_eq_mapHomologyIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [S.HasHomology] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
                                    S.mapHomologyIso' F = S.mapHomologyIso F
                                    def CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F G) :
                                    CategoryTheory.ShortComplex.LeftHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

                                    Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the left homology of a short complex S, and a left homology data for S, this is the left homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F G) :
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F G) :
                                      def CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F G) :
                                      CategoryTheory.ShortComplex.RightHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

                                      Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the right homology of a short complex S, and a right homology data for S, this is the right homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F G) :
                                        @[simp]
                                        theorem CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F G) :
                                        def CategoryTheory.ShortComplex.HomologyMapData.natTransApp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F G) :
                                        CategoryTheory.ShortComplex.HomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)

                                        Given a natural transformation τ : F ⟶ G between functors C ⥤ D which preserve the homology of a short complex S, and a homology data for S, this is the homology map data for the morphism S.mapNatTrans τ obtained by evaluating τ.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F G) :
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F G) :
                                          theorem CategoryTheory.ShortComplex.homologyMap_mapNatTrans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) {F G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] [S.HasHomology] (τ : F G) :
                                          CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ) = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).hom (CategoryTheory.CategoryStruct.comp (τ.app S.homology) (S.mapHomologyIso G).inv)

                                          The natural isomorphism F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology. -

                                          Equations
                                          Instances For

                                            The natural isomorphism F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology. -

                                            Equations
                                            Instances For

                                              The natural isomorphism F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology. -

                                              Equations
                                              Instances For

                                                The natural isomorphism F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology. -

                                                Equations
                                                Instances For

                                                  The natural isomorphism F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F for a functor F : C ⥤ D which preserves homology. -

                                                  Equations
                                                  Instances For
                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_map_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {hl₁ : S₁.LeftHomologyData} {hl₂ : S₂.LeftHomologyData} (ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂) [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F] :
                                                    CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) CategoryTheory.IsIso (F.map ψl.φH)
                                                    theorem CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_map_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {hr₁ : S₁.RightHomologyData} {hr₂ : S₂.RightHomologyData} (ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂) [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] :
                                                    CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) CategoryTheory.IsIso (F.map ψr.φH)
                                                    instance CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] [CategoryTheory.ShortComplex.QuasiIso φ] :
                                                    CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
                                                    theorem CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] [F.ReflectsIsomorphisms] :
                                                    instance CategoryTheory.ShortComplex.quasiIso_map_of_preservesRightHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] [CategoryTheory.ShortComplex.QuasiIso φ] :
                                                    CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
                                                    theorem CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesRightHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] [F.ReflectsIsomorphisms] :

                                                    If a short complex S is such that S.f = 0 and that the kernel of S.g is preserved by a functor F, then F preserves the left homology of S.

                                                    If a short complex S is such that S.g = 0 and that the cokernel of S.f is preserved by a functor F, then F preserves the right homology of S.

                                                    If a short complex S is such that S.g = 0 and that the cokernel of S.f is preserved by a functor F, then F preserves the left homology of S.

                                                    If a short complex S is such that S.f = 0 and that the kernel of S.g is preserved by a functor F, then F preserves the right homology of S.

                                                    theorem CategoryTheory.NatTrans.app_homology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F G : CategoryTheory.Functor C D} (τ : F G) (S : CategoryTheory.ShortComplex C) [S.HasHomology] [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] :
                                                    τ.app S.homology = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ)) (S.mapHomologyIso G).hom)