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
    Equations
    • F.preservesHomologyOfExact = { preservesKernels := inferInstance, preservesCokernels := inferInstance }

    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 h is preserved by a functor F, this functor preserves the cokernel of h.f' : S.X₁ ⟶ h.K.

      Equations
      Instances For
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        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]
          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₁ : CategoryTheory.ShortComplex C} {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
          @[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₁ : CategoryTheory.ShortComplex C} {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
          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₁ : CategoryTheory.ShortComplex C} {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

            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 h is preserved by a functor F, this functor preserves the kernel of h.g' : h.Q ⟶ S.X₃.

              Equations
              Instances For
                @[simp]
                @[simp]
                @[simp]
                @[simp]
                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]
                  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₁ : CategoryTheory.ShortComplex C} {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
                  @[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₁ : CategoryTheory.ShortComplex C} {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
                  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₁ : CategoryTheory.ShortComplex C} {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.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
                    @[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
                    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.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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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
                      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₁ : CategoryTheory.ShortComplex C} {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

                        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

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def 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.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                Equations
                                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] :
                                (S.map F).HasLeftHomology
                                Equations
                                • =
                                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
                                Equations
                                • =
                                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
                                Equations
                                • =
                                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
                                Equations
                                • =
                                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
                                Equations
                                • =
                                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
                                Equations
                                • =
                                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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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_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) :
                                  @[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
                                  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_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} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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.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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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_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₁ : CategoryTheory.ShortComplex C} {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'_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₁ : CategoryTheory.ShortComplex C} {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'_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₁ : CategoryTheory.ShortComplex C} {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'_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₁ : CategoryTheory.ShortComplex C} {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'_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₁ : CategoryTheory.ShortComplex C} {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'_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
                                            @[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 : CategoryTheory.Functor C D} {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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F G) :
                                            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 : CategoryTheory.Functor C D} {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.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 : CategoryTheory.Functor C D} {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_φ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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : 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 : CategoryTheory.Functor C D} {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.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 : CategoryTheory.Functor C D} {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_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 : CategoryTheory.Functor C D} {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) :
                                                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 : CategoryTheory.Functor C D} {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
                                                  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 : CategoryTheory.Functor C D} {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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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 φ)
                                                            Equations
                                                            • =
                                                            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₁ : CategoryTheory.ShortComplex C} {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₁ : CategoryTheory.ShortComplex C} {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 φ)
                                                            Equations
                                                            • =
                                                            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₁ : CategoryTheory.ShortComplex C} {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.

                                                            Equations
                                                            Instances For

                                                              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.

                                                              Equations
                                                              Instances For

                                                                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.

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

                                                                  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.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    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 : CategoryTheory.Functor C D} {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)