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.

source
class CategoryTheory.Functor.PreservesHomology {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] :
Type (max (max (max u_1 u_2) u_3) u_4)

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

Instances
    source
    def CategoryTheory.Functor.PreservesHomology.preservesKernel {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesHomology F] {X : C} {Y : C} (f : X ⟶ Y) :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F

    A functor which preserves homology preserves kernels.

    Equations
    Instances For
      source
      def CategoryTheory.Functor.PreservesHomology.preservesCokernel {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesHomology F] {X : C} {Y : C} (f : X ⟶ Y) :
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F

      A functor which preserves homology preserves cokernels.

      Equations
      Instances For
        source
        noncomputable instance CategoryTheory.Functor.preservesHomologyOfExact {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] :
        CategoryTheory.Functor.PreservesHomology F
        Equations
        source
        class CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy {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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] :
        Type (max (max (max u_1 u_2) u_3) u_4)

        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
          source
          noncomputable instance CategoryTheory.ShortComplex.LeftHomologyData.isPreservedByOfPreservesHomology {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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesHomology F] :
          CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg {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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F

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

          Equations
          Instances For
            source
            def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf' {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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.ShortComplex.LeftHomologyData.f' h) 0) F

            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
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.LeftHomologyData.map_i {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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
              (CategoryTheory.ShortComplex.LeftHomologyData.map h F).i = F.toPrefunctor.map h.i
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.LeftHomologyData.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} (h : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
              (CategoryTheory.ShortComplex.LeftHomologyData.map h F).K = F.toPrefunctor.obj h.K
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.LeftHomologyData.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} (h : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
              (CategoryTheory.ShortComplex.LeftHomologyData.map h F).H = F.toPrefunctor.obj h.H
              source
              @[simp]
              theorem 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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
              (CategoryTheory.ShortComplex.LeftHomologyData.map h F).π = F.toPrefunctor.map h.π
              source
              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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
              CategoryTheory.ShortComplex.LeftHomologyData (CategoryTheory.ShortComplex.map S F)

              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
                source
                @[simp]
                theorem CategoryTheory.ShortComplex.LeftHomologyData.map_f' {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} (h : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
                CategoryTheory.ShortComplex.LeftHomologyData.f' (CategoryTheory.ShortComplex.LeftHomologyData.map h F) = F.toPrefunctor.map (CategoryTheory.ShortComplex.LeftHomologyData.f' h)
                source
                @[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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ F] :
                (CategoryTheory.ShortComplex.LeftHomologyMapData.map ψ F).φH = F.toPrefunctor.map ψ.φH
                source
                @[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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ F] :
                (CategoryTheory.ShortComplex.LeftHomologyMapData.map ψ F).φK = F.toPrefunctor.map ψ.φK
                source
                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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ F] :
                CategoryTheory.ShortComplex.LeftHomologyMapData ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.LeftHomologyData.map h₁ F) (CategoryTheory.ShortComplex.LeftHomologyData.map h₂ 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
                Instances For
                  source
                  class CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy {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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] :
                  Type (max (max (max u_1 u_2) u_3) u_4)

                  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
                    source
                    noncomputable instance CategoryTheory.ShortComplex.RightHomologyData.isPreservedByOfPreservesHomology {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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesHomology F] :
                    CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf {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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F

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

                    Equations
                    Instances For
                      source
                      def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg' {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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.ShortComplex.RightHomologyData.g' h) 0) F

                      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
                        source
                        @[simp]
                        theorem CategoryTheory.ShortComplex.RightHomologyData.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} (h : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                        (CategoryTheory.ShortComplex.RightHomologyData.map h F).H = F.toPrefunctor.obj h.H
                        source
                        @[simp]
                        theorem CategoryTheory.ShortComplex.RightHomologyData.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} (h : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                        (CategoryTheory.ShortComplex.RightHomologyData.map h F).Q = F.toPrefunctor.obj h.Q
                        source
                        @[simp]
                        theorem CategoryTheory.ShortComplex.RightHomologyData.map_p {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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                        (CategoryTheory.ShortComplex.RightHomologyData.map h F).p = F.toPrefunctor.map h.p
                        source
                        @[simp]
                        theorem 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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                        (CategoryTheory.ShortComplex.RightHomologyData.map h F).ι = F.toPrefunctor.map h.ι
                        source
                        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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                        CategoryTheory.ShortComplex.RightHomologyData (CategoryTheory.ShortComplex.map S F)

                        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
                          source
                          @[simp]
                          theorem CategoryTheory.ShortComplex.RightHomologyData.map_g' {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} (h : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                          CategoryTheory.ShortComplex.RightHomologyData.g' (CategoryTheory.ShortComplex.RightHomologyData.map h F) = F.toPrefunctor.map (CategoryTheory.ShortComplex.RightHomologyData.g' h)
                          source
                          @[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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F] :
                          (CategoryTheory.ShortComplex.RightHomologyMapData.map ψ F).φH = F.toPrefunctor.map ψ.φH
                          source
                          @[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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F] :
                          (CategoryTheory.ShortComplex.RightHomologyMapData.map ψ F).φQ = F.toPrefunctor.map ψ.φQ
                          source
                          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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F] :
                          CategoryTheory.ShortComplex.RightHomologyMapData ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.RightHomologyData.map h₁ F) (CategoryTheory.ShortComplex.RightHomologyData.map h₂ 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
                          Instances For
                            source
                            @[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 : CategoryTheory.ShortComplex.HomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F] :
                            (CategoryTheory.ShortComplex.HomologyData.map h F).right = CategoryTheory.ShortComplex.RightHomologyData.map h.right F
                            source
                            @[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 : CategoryTheory.ShortComplex.HomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F] :
                            (CategoryTheory.ShortComplex.HomologyData.map h F).iso = F.mapIso h.iso
                            source
                            @[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 : CategoryTheory.ShortComplex.HomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F] :
                            (CategoryTheory.ShortComplex.HomologyData.map h F).left = CategoryTheory.ShortComplex.LeftHomologyData.map h.left F
                            source
                            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 : CategoryTheory.ShortComplex.HomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F] :
                            CategoryTheory.ShortComplex.HomologyData (CategoryTheory.ShortComplex.map S F)

                            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
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[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₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right F] :
                              (CategoryTheory.ShortComplex.HomologyMapData.map ψ F).right = CategoryTheory.ShortComplex.RightHomologyMapData.map ψ.right F
                              source
                              @[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₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right F] :
                              (CategoryTheory.ShortComplex.HomologyMapData.map ψ F).left = CategoryTheory.ShortComplex.LeftHomologyMapData.map ψ.left F
                              source
                              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₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right F] :
                              CategoryTheory.ShortComplex.HomologyMapData ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.HomologyData.map h₁ F) (CategoryTheory.ShortComplex.HomologyData.map h₂ 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
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                class CategoryTheory.Functor.PreservesLeftHomologyOf {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) :
                                Type (max (max (max u_1 u_2) u_3) u_4)

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

                                Instances
                                  source
                                  class CategoryTheory.Functor.PreservesRightHomologyOf {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) :
                                  Type (max (max (max u_1 u_2) u_3) u_4)

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

                                  Instances
                                    source
                                    noncomputable instance CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Functor.PreservesHomology F] :
                                    CategoryTheory.Functor.PreservesLeftHomologyOf F S
                                    Equations
                                    source
                                    noncomputable instance CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Functor.PreservesHomology F] :
                                    CategoryTheory.Functor.PreservesRightHomologyOf F S
                                    Equations
                                    source
                                    def 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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.LeftHomologyData S) [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F] :
                                    CategoryTheory.Functor.PreservesLeftHomologyOf F S

                                    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
                                      source
                                      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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.RightHomologyData S) [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F] :
                                      CategoryTheory.Functor.PreservesRightHomologyOf F 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
                                        source
                                        instance CategoryTheory.ShortComplex.LeftHomologyData.isPreservedByOfPreserves {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₁ : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                        CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F
                                        Equations
                                        source
                                        instance CategoryTheory.ShortComplex.RightHomologyData.isPreservedByOfPreserves {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₂ : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                        CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F
                                        Equations
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasLeftHomology (CategoryTheory.ShortComplex.map S F)
                                        Equations
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasLeftHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S)
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasRightHomology (CategoryTheory.ShortComplex.map S F)
                                        Equations
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasRightHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S)
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)
                                        Equations
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                        CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S)
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        source
                                        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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ F] :
                                        F.toPrefunctor.map (CategoryTheory.ShortComplex.cyclesMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.cyclesMap' ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.LeftHomologyData.map hl₁ F) (CategoryTheory.ShortComplex.LeftHomologyData.map hl₂ F)
                                        source
                                        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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ F] :
                                        F.toPrefunctor.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.leftHomologyMap' ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.LeftHomologyData.map hl₁ F) (CategoryTheory.ShortComplex.LeftHomologyData.map hl₂ F)
                                        source
                                        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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ F] :
                                        F.toPrefunctor.map (CategoryTheory.ShortComplex.opcyclesMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.opcyclesMap' ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.RightHomologyData.map hr₁ F) (CategoryTheory.ShortComplex.RightHomologyData.map hr₂ F)
                                        source
                                        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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ F] :
                                        F.toPrefunctor.map (CategoryTheory.ShortComplex.rightHomologyMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.rightHomologyMap' ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.RightHomologyData.map hr₁ F) (CategoryTheory.ShortComplex.RightHomologyData.map hr₂ F)
                                        source
                                        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₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right F] :
                                        F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂) = CategoryTheory.ShortComplex.homologyMap' ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) (CategoryTheory.ShortComplex.HomologyData.map h₁ F) (CategoryTheory.ShortComplex.HomologyData.map h₂ F)
                                        source
                                        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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                        CategoryTheory.ShortComplex.cycles (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.cycles S)

                                        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
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          @[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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] {Z : D} (h : F.toPrefunctor.obj S.X₂ ⟶ Z) :
                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.iCycles S)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles (CategoryTheory.ShortComplex.map S F)) h
                                          source
                                          @[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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.iCycles S)) = CategoryTheory.ShortComplex.iCycles (CategoryTheory.ShortComplex.map S F)
                                          source
                                          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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                          CategoryTheory.ShortComplex.leftHomology (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.leftHomology S)

                                          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
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                            CategoryTheory.ShortComplex.opcycles (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.opcycles S)

                                            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
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                              CategoryTheory.ShortComplex.rightHomology (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.rightHomology S)

                                              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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                                CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.homology S)

                                                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
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                                  CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S F) ≅ F.toPrefunctor.obj (CategoryTheory.ShortComplex.homology S)

                                                  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
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapCyclesIso S F = CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso (CategoryTheory.ShortComplex.LeftHomologyData.map hl F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso hl).symm
                                                    source
                                                    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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapLeftHomologyIso S F = CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso (CategoryTheory.ShortComplex.LeftHomologyData.map hl F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso hl).symm
                                                    source
                                                    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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapOpcyclesIso S F = CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso (CategoryTheory.ShortComplex.RightHomologyData.map hr F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso hr).symm
                                                    source
                                                    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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapRightHomologyIso S F = CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso (CategoryTheory.ShortComplex.RightHomologyData.map hr F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso hr).symm
                                                    source
                                                    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 : CategoryTheory.ShortComplex.LeftHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapHomologyIso S F = CategoryTheory.ShortComplex.LeftHomologyData.homologyIso (CategoryTheory.ShortComplex.LeftHomologyData.map hl F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.LeftHomologyData.homologyIso hl).symm
                                                    source
                                                    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 : CategoryTheory.ShortComplex.RightHomologyData S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapHomologyIso' S F = CategoryTheory.ShortComplex.RightHomologyData.homologyIso (CategoryTheory.ShortComplex.RightHomologyData.map hr F) ≪≫ F.mapIso (CategoryTheory.ShortComplex.RightHomologyData.homologyIso hr).symm
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.cycles S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.cyclesMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.cyclesMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.cycles (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.cyclesMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.cyclesMap φ)) (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).inv (CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.leftHomology S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.leftHomology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).inv (CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.opcycles S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.opcyclesMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.opcyclesMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.opcycles (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).inv (CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.rightHomology S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.rightHomology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).inv (CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.homology S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).inv (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.ShortComplex.homology S₂) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).hom (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).hom (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] {Z : D} (h : CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z) :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)) h)
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)] [CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] :
                                                    CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.ShortComplex.homologyMap φ)) (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).inv (CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ))
                                                    source
                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] :
                                                    CategoryTheory.ShortComplex.mapHomologyIso' S F = CategoryTheory.ShortComplex.mapHomologyIso S F
                                                    source
                                                    @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] (h : CategoryTheory.ShortComplex.LeftHomologyData S) (τ : F ⟶ G) :
                                                    (CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φH = τ.app h.H
                                                    source
                                                    @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] (h : CategoryTheory.ShortComplex.LeftHomologyData S) (τ : F ⟶ G) :
                                                    (CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φK = τ.app h.K
                                                    source
                                                    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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] (h : CategoryTheory.ShortComplex.LeftHomologyData S) (τ : F ⟶ G) :
                                                    CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.ShortComplex.mapNatTrans S τ) (CategoryTheory.ShortComplex.LeftHomologyData.map h F) (CategoryTheory.ShortComplex.LeftHomologyData.map h 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
                                                      source
                                                      @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.RightHomologyData S) (τ : F ⟶ G) :
                                                      (CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φQ = τ.app h.Q
                                                      source
                                                      @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.RightHomologyData S) (τ : F ⟶ G) :
                                                      (CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φH = τ.app h.H
                                                      source
                                                      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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.RightHomologyData S) (τ : F ⟶ G) :
                                                      CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.ShortComplex.mapNatTrans S τ) (CategoryTheory.ShortComplex.RightHomologyData.map h F) (CategoryTheory.ShortComplex.RightHomologyData.map h 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
                                                        source
                                                        @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.HomologyData S) (τ : F ⟶ G) :
                                                        (CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).left = CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h.left τ
                                                        source
                                                        @[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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.HomologyData S) (τ : F ⟶ G) :
                                                        (CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).right = CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h.right τ
                                                        source
                                                        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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] (h : CategoryTheory.ShortComplex.HomologyData S) (τ : F ⟶ G) :
                                                        CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.ShortComplex.mapNatTrans S τ) (CategoryTheory.ShortComplex.HomologyData.map h F) (CategoryTheory.ShortComplex.HomologyData.map h 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
                                                          source
                                                          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} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] [CategoryTheory.ShortComplex.HasHomology S] (τ : F ⟶ G) :
                                                          CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.mapNatTrans S τ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S F).hom (CategoryTheory.CategoryStruct.comp (τ.app (CategoryTheory.ShortComplex.homology S)) (CategoryTheory.ShortComplex.mapHomologyIso S G).inv)
                                                          source
                                                          noncomputable def CategoryTheory.ShortComplex.cyclesFunctorIso {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [CategoryTheory.Functor.PreservesHomology F] :
                                                          CategoryTheory.Functor.comp (CategoryTheory.Functor.mapShortComplex F) (CategoryTheory.ShortComplex.cyclesFunctor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.cyclesFunctor C) F

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

                                                          Equations
                                                          Instances For
                                                            source
                                                            noncomputable def CategoryTheory.ShortComplex.leftHomologyFunctorIso {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [CategoryTheory.Functor.PreservesHomology F] :
                                                            CategoryTheory.Functor.comp (CategoryTheory.Functor.mapShortComplex F) (CategoryTheory.ShortComplex.leftHomologyFunctor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.leftHomologyFunctor C) F

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

                                                            Equations
                                                            Instances For
                                                              source
                                                              noncomputable def CategoryTheory.ShortComplex.opcyclesFunctorIso {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [CategoryTheory.Functor.PreservesHomology F] :
                                                              CategoryTheory.Functor.comp (CategoryTheory.Functor.mapShortComplex F) (CategoryTheory.ShortComplex.opcyclesFunctor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.opcyclesFunctor C) F

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

                                                              Equations
                                                              Instances For
                                                                source
                                                                noncomputable def CategoryTheory.ShortComplex.rightHomologyFunctorIso {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [CategoryTheory.Functor.PreservesHomology F] :
                                                                CategoryTheory.Functor.comp (CategoryTheory.Functor.mapShortComplex F) (CategoryTheory.ShortComplex.rightHomologyFunctor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.rightHomologyFunctor C) F

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

                                                                Equations
                                                                Instances For
                                                                  source
                                                                  noncomputable def CategoryTheory.ShortComplex.homologyFunctorIso {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [CategoryTheory.Functor.PreservesHomology F] :
                                                                  CategoryTheory.Functor.comp (CategoryTheory.Functor.mapShortComplex F) (CategoryTheory.ShortComplex.homologyFunctor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.homologyFunctor C) F

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

                                                                  Equations
                                                                  Instances For
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {hl₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂) [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F] [CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ F] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) ↔ CategoryTheory.IsIso (F.toPrefunctor.map ψl.φH)
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {hr₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂) [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F] [CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ F] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) ↔ CategoryTheory.IsIso (F.toPrefunctor.map ψr.φH)
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] [CategoryTheory.ShortComplex.QuasiIso φ] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₁] [CategoryTheory.Functor.PreservesLeftHomologyOf F S₂] [CategoryTheory.ReflectsIsomorphisms F] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] [CategoryTheory.ShortComplex.QuasiIso φ] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ)
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    source
                                                                    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) [CategoryTheory.Functor.PreservesZeroMorphisms F] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₁)] [CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S₂)] [CategoryTheory.Functor.PreservesRightHomologyOf F S₁] [CategoryTheory.Functor.PreservesRightHomologyOf F S₂] [CategoryTheory.ReflectsIsomorphisms F] :
                                                                    CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
                                                                    source
                                                                    noncomputable def CategoryTheory.Functor.preservesLeftHomologyOfZerof {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F] :
                                                                    CategoryTheory.Functor.PreservesLeftHomologyOf F 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 left homology of S.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      source
                                                                      noncomputable def CategoryTheory.Functor.preservesRightHomologyOfZerog {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F] :
                                                                      CategoryTheory.Functor.PreservesRightHomologyOf F 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.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        source
                                                                        noncomputable def CategoryTheory.Functor.preservesLeftHomologyOfZerog {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F] :
                                                                        CategoryTheory.Functor.PreservesLeftHomologyOf F 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.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          source
                                                                          noncomputable def CategoryTheory.Functor.preservesRightHomologyOfZerof {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F] :
                                                                          CategoryTheory.Functor.PreservesRightHomologyOf F 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.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            source
                                                                            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) [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesLeftHomologyOf G S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf G S] :
                                                                            τ.app (CategoryTheory.ShortComplex.homology S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.mapNatTrans S τ)) (CategoryTheory.ShortComplex.mapHomologyIso S G).hom)