Documentation

Mathlib.Algebra.Homology.ShortComplex.Homology

Homology of short complexes #

In this file, we shall define the homology of short complexes S, i.e. diagrams f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0. We shall say that [S.HasHomology] when there exists h : S.HomologyData. A homology data for S consists of compatible left/right homology data left and right. The left homology data left involves an object left.H that is a cokernel of the canonical map S.X₁ ⟶ K where K is a kernel of g. On the other hand, the dual notion right.H is a kernel of the canonical morphism Q ⟶ S.X₃ when Q is a cokernel of f. The compatibility that is required involves an isomorphism left.H ≅ right.H which makes a certain pentagon commute. When such a homology data exists, S.homology shall be defined as h.left.H for a chosen h : S.HomologyData.

This definition requires very little assumption on the category (only the existence of zero morphisms). We shall prove that in abelian categories, all short complexes have homology data.

Note: This definition arose by the end of the Liquid Tensor Experiment which contained a structure has_homology which is quite similar to S.HomologyData. After the category ShortComplex C was introduced by J. Riou, A. Topaz suggested such a structure could be used as a basis for the definition of homology.

A homology data for a short complex consists of two compatible left and right homology data

Instances For
    @[simp]

    the pentagon relation expressing the compatibility of the left and right homology data

    structure CategoryTheory.ShortComplex.HomologyMapData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :

    A homology map data for a morphism φ : S₁ ⟶ S₂ where both S₁ and S₂ are equipped with homology data consists of left and right homology map data.

    Instances For
      Equations
      • CategoryTheory.ShortComplex.HomologyMapData.instInhabited = { default := { left := default, right := default } }
      Equations

      A choice of the (unique) homology map data associated with a morphism φ : S₁ ⟶ S₂ where both short complexes S₁ and S₂ are equipped with homology data.

      Equations
      Instances For
        theorem CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} {γ₁ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂} {γ₂ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
        γ₁.left.φH = γ₂.left.φH

        When the first map S.f is zero, this is the homology data on S given by any limit kernel fork of S.g

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

          When the first map S.f is zero, this is the homology data on S given by the chosen kernel S.g

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

            When the second map S.g is zero, this is the homology data on S given by any colimit cokernel cofork of S.f

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

              When the second map S.g is zero, this is the homology data on S given by the chosen cokernel S.f

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

                When both S.f and S.g are zero, the middle object S.X₂ gives a homology data on S

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

                  If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a homology data for S₁ induces a homology data for S₂. The inverse construction is ofEpiOfIsIsoOfMono'.

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

                    If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a homology data for S₂ induces a homology data for S₁. The inverse construction is ofEpiOfIsIsoOfMono.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      noncomputable def CategoryTheory.ShortComplex.HomologyData.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) (h : S₁.HomologyData) :
                      S₂.HomologyData

                      If e : S₁ ≅ S₂ is an isomorphism of short complexes and h₁ : HomologyData S₁, this is the homology data for S₂ deduced from the isomorphism.

                      Equations
                      Instances For

                        A homology data for a short complex S induces a homology data for S.op.

                        Equations
                        • h.op = { left := h.right.op, right := h.left.op, iso := h.iso.op, comm := }
                        Instances For

                          A homology data for a short complex S in the opposite category induces a homology data for S.unop.

                          Equations
                          • h.unop = { left := h.right.unop, right := h.left.unop, iso := h.iso.unop, comm := }
                          Instances For

                            A short complex S has homology when there exists a S.HomologyData

                            • condition : Nonempty S.HomologyData

                              the condition that there exists a homology data

                            Instances

                              the condition that there exists a homology data

                              A chosen S.HomologyData for a short complex S that has homology

                              Equations
                              • S.homologyData = .some
                              Instances For

                                The homology map data associated to the zero morphism between two short complexes.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.HomologyMapData.comp_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} {h₃ : S₃.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃) :
                                  (ψ.comp ψ').right = ψ.right.comp ψ'.right
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.HomologyMapData.comp_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} {h₃ : S₃.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃) :
                                  (ψ.comp ψ').left = ψ.left.comp ψ'.left

                                  The composition of homology map data.

                                  Equations
                                  • ψ.comp ψ' = { left := ψ.left.comp ψ'.left, right := ψ.right.comp ψ'.right }
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.ShortComplex.HomologyMapData.op_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
                                    ψ.op.right = ψ.left.op
                                    @[simp]
                                    theorem CategoryTheory.ShortComplex.HomologyMapData.op_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
                                    ψ.op.left = ψ.right.op

                                    A homology map data for a morphism of short complexes induces a homology map data in the opposite category.

                                    Equations
                                    • ψ.op = { left := ψ.right.op, right := ψ.left.op }
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.HomologyMapData.unop_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
                                      ψ.unop.right = ψ.left.unop
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.HomologyMapData.unop_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
                                      ψ.unop.left = ψ.right.unop

                                      A homology map data for a morphism of short complexes in the opposite category induces a homology map data in the original category.

                                      Equations
                                      • ψ.unop = { left := ψ.right.unop, right := ψ.left.unop }
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
                                        @[simp]
                                        theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :

                                        When S₁.f, S₁.g, S₂.f and S₂.g are all zero, the action on homology of a morphism φ : S₁ ⟶ S₂ is given by the action φ.τ₂ on the middle objects.

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

                                          When S₁.g and S₂.g are zero and we have chosen colimit cokernel coforks c₁ and c₂ for S₁.f and S₂.f respectively, the action on homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that φ.τ₂ ≫ c₂.π = c₁.π ≫ f.

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

                                            When S₁.f and S₂.f are zero and we have chosen limit kernel forks c₁ and c₂ for S₁.g and S₂.g respectively, the action on homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι.

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

                                              When both maps S.f and S.g of a short complex S are zero, this is the homology map data (for the identity of S) which relates the homology data ofZeros and ofIsColimitCokernelCofork.

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

                                                When both maps S.f and S.g of a short complex S are zero, this is the homology map data (for the identity of S) which relates the homology data HomologyData.ofIsLimitKernelFork and ofZeros .

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

                                                  This homology map data expresses compatibilities of the homology data constructed by HomologyData.ofEpiOfIsIsoOfMono

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

                                                    This homology map data expresses compatibilities of the homology data constructed by HomologyData.ofEpiOfIsIsoOfMono'

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

                                                      The homology of a short complex is the left.H field of a chosen homology data.

                                                      Equations
                                                      • S.homology = S.homologyData.left.H
                                                      Instances For

                                                        When a short complex has homology, this is the canonical isomorphism S.leftHomology ≅ S.homology.

                                                        Equations
                                                        Instances For

                                                          When a short complex has homology, this is the canonical isomorphism S.rightHomology ≅ S.homology.

                                                          Equations
                                                          Instances For

                                                            When a short complex has homology, its homology can be computed using any left homology data.

                                                            Equations
                                                            • h.homologyIso = S.leftHomologyIso.symm.trans h.leftHomologyIso
                                                            Instances For

                                                              When a short complex has homology, its homology can be computed using any right homology data.

                                                              Equations
                                                              • h.homologyIso = S.rightHomologyIso.symm.trans h.rightHomologyIso
                                                              Instances For
                                                                def CategoryTheory.ShortComplex.homologyMap' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
                                                                h₁.left.H h₂.left.H

                                                                Given a morphism φ : S₁ ⟶ S₂ of short complexes and homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced homology map h₁.left.H ⟶ h₁.left.H.

                                                                Equations
                                                                Instances For
                                                                  noncomputable def CategoryTheory.ShortComplex.homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                  S₁.homology S₂.homology

                                                                  The homology map S₁.homology ⟶ S₂.homology induced by a morphism S₁ ⟶ S₂ of short complexes.

                                                                  Equations
                                                                  Instances For
                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                    theorem CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                    theorem CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                    def CategoryTheory.ShortComplex.homologyMapIso' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
                                                                    h₁.left.H h₂.left.H

                                                                    Given an isomorphism S₁ ≅ S₂ of short complexes and homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced homology isomorphism h₁.left.H ≅ h₁.left.H.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      noncomputable def CategoryTheory.ShortComplex.homologyMapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] :
                                                                      S₁.homology S₂.homology

                                                                      The homology isomorphism S₁.homology ⟶ S₂.homology induced by an isomorphism S₁ ≅ S₂ of short complexes.

                                                                      Equations
                                                                      Instances For

                                                                        If a short complex S has both a left homology data h₁ and a right homology data h₂, this is the canonical morphism h₁.H ⟶ h₂.H.

                                                                        Equations
                                                                        Instances For
                                                                          noncomputable def CategoryTheory.ShortComplex.leftRightHomologyComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] [S.HasRightHomology] :
                                                                          S.leftHomology S.rightHomology

                                                                          If a short complex S has both a left and right homology, this is the canonical morphism S.leftHomology ⟶ S.rightHomology.

                                                                          Equations
                                                                          Instances For
                                                                            theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [S.HasLeftHomology] [S.HasRightHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
                                                                            S.leftRightHomologyComparison = CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.rightHomologyIso.inv)

                                                                            This is the homology data for a short complex S that is obtained from a left homology data h₁ and a right homology data h₂ when the comparison morphism leftRightHomologyComparison' h₁ h₂ : h₁.H ⟶ h₂.H is an isomorphism.

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

                                                                              We shall say that a category C is a category with homology when all short complexes have homology.

                                                                              Instances

                                                                                The homology functor ShortComplex C ⥤ C for a category C with homology.

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

                                                                                  The canonical morphism S.cycles ⟶ S.homology for a short complex S that has homology.

                                                                                  Equations
                                                                                  Instances For

                                                                                    The canonical morphism S.homology ⟶ S.opcycles for a short complex S that has homology.

                                                                                    Equations
                                                                                    Instances For

                                                                                      The homology S.homology of a short complex is the cokernel of the morphism S.toCycles : S.X₁ ⟶ S.cycles.

                                                                                      Equations
                                                                                      Instances For

                                                                                        The homology S.homology of a short complex is the kernel of the morphism S.fromOpcycles : S.opcycles ⟶ S.X₃.

                                                                                        Equations
                                                                                        Instances For
                                                                                          noncomputable def CategoryTheory.ShortComplex.descHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [S.HasHomology] (k : S.cycles A) (hk : CategoryTheory.CategoryStruct.comp S.toCycles k = 0) :
                                                                                          S.homology A

                                                                                          Given a morphism k : S.cycles ⟶ A such that S.toCycles ≫ k = 0, this is the induced morphism S.homology ⟶ A.

                                                                                          Equations
                                                                                          Instances For
                                                                                            noncomputable def CategoryTheory.ShortComplex.liftHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [S.HasHomology] (k : A S.opcycles) (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0) :
                                                                                            A S.homology

                                                                                            Given a morphism k : A ⟶ S.opcycles such that k ≫ S.fromOpcycles = 0, this is the induced morphism A ⟶ S.homology.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.ShortComplex.liftHomology_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} [S.HasHomology] (k : A S.opcycles) (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0) :
                                                                                              CategoryTheory.CategoryStruct.comp (S.liftHomology k hk) S.homologyι = k

                                                                                              The homology of a short complex S identifies to the kernel of the induced morphism cokernel S.f ⟶ S.X₃.

                                                                                              Equations
                                                                                              • S.homologyIsoKernelDesc = S.rightHomologyIso.symm.trans S.rightHomologyIsoKernelDesc
                                                                                              Instances For

                                                                                                The homology of a short complex S identifies to the cokernel of the induced morphism S.X₁ ⟶ kernel S.g.

                                                                                                Equations
                                                                                                • S.homologyIsoCokernelLift = S.leftHomologyIso.symm.trans CategoryTheory.ShortComplex.leftHomologyIsoCokernelLift
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  @[simp]
                                                                                                  @[simp]
                                                                                                  @[simp]
                                                                                                  noncomputable def CategoryTheory.ShortComplex.homologyOpIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] :
                                                                                                  S.op.homology { unop := S.homology }

                                                                                                  The canonical isomorphism S.op.homologyOpposite.op S.homology when a short complex S has homology.

                                                                                                  Equations
                                                                                                  • S.homologyOpIso = S.op.leftHomologyIso.symm.trans (S.leftHomologyOpIso.trans S.rightHomologyIso.symm.op)
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.ShortComplex.asIsoHomologyπ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [S.HasHomology] :
                                                                                                    (S.asIsoHomologyπ hf).hom = S.homologyπ
                                                                                                    noncomputable def CategoryTheory.ShortComplex.asIsoHomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [S.HasHomology] :
                                                                                                    S.cycles S.homology

                                                                                                    The canonical isomorphism S.cycles ≅ S.homology when S.f = 0.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.ShortComplex.asIsoHomologyι_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [S.HasHomology] :
                                                                                                      (S.asIsoHomologyι hg).hom = S.homologyι
                                                                                                      noncomputable def CategoryTheory.ShortComplex.asIsoHomologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [S.HasHomology] :
                                                                                                      S.homology S.opcycles

                                                                                                      The canonical isomorphism S.homology ≅ S.opcycles when S.g = 0.

                                                                                                      Equations
                                                                                                      Instances For