Documentation

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Left Homology of short complexes #

Given a short complex S : ShortComplex C, which consists of two composable maps f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0, we shall define here the "left homology" S.leftHomology of S. For this, we introduce the notion of "left homology data". Such an h : S.LeftHomologyData consists of the data of morphisms i : K ⟶ X₂ and π : KH such that i identifies K with the kernel of g : X₂ ⟶ X₃, and that π identifies H with the cokernel of the induced map f' : X₁ ⟶ K.

When such a S.LeftHomologyData exists, we shall say that [S.HasLeftHomology] and we define S.leftHomology to be the H field of a chosen left homology data. Similarly, we define S.cycles to be the K field.

The dual notion is defined in RightHomologyData.lean. In Homology.lean, when S has two compatible left and right homology data (i.e. they give the same H up to a canonical isomorphism), we shall define [S.HasHomology] and S.homology.

A left homology data for a short complex S consists of morphisms i : K ⟶ S.X₂ and π : KH such that i identifies K to the kernel of g : S.X₂ ⟶ S.X₃, and that π identifies H to the cokernel of the induced map f' : S.X₁ ⟶ K

Instances For

    The chosen kernels and cokernels of the limits API give a LeftHomologyData

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

      Any morphism k : A ⟶ S.X₂ that is a cycle (i.e. k ≫ S.g = 0) lifts to a morphism A ⟶ K

      Equations
      Instances For

        The (left) homology class A ⟶ H attached to a cycle k : A ⟶ S.X₂

        Equations
        Instances For

          Given h : LeftHomologyData S, this is morphism S.X₁ ⟶ h.K induced by S.f : S.X₁ ⟶ S.X₂ and the fact that h.K is a kernel of S.g : S.X₂ ⟶ S.X₃.

          Equations
          • h.f' = h.liftK S.f
          Instances For

            For h : S.LeftHomologyData, this is a restatement of h., saying that π : h.K ⟶ h.H is a cokernel of h.f' : S.X₁ ⟶ h.K.

            Equations
            • h.hπ' = h.hπ
            Instances For

              The morphism H ⟶ A induced by a morphism k : K ⟶ A such that f' ≫ k = 0

              Equations
              Instances For

                When the second map S.g is zero, this is the left 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 left 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 the first map S.f is zero, this is the left 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 left 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 both S.f and S.g are zero, the middle object S.X₂ gives a left homology data on S

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

                          A short complex S has left homology when there exists a S.LeftHomologyData

                          Instances

                            A chosen S.LeftHomologyData for a short complex S that has left homology

                            Equations
                            • S.leftHomologyData = .some
                            Instances For
                              structure CategoryTheory.ShortComplex.LeftHomologyMapData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                              Type u_2

                              Given left homology data h₁ and h₂ for two short complexes S₁ and S₂, a LeftHomologyMapData for a morphism φ : S₁ ⟶ S₂ consists of a description of the induced morphisms on the K (cycles) and H (left homology) fields of h₁ and h₂.

                              Instances For
                                @[simp]

                                commutation with i

                                @[simp]

                                commutation with f'

                                @[simp]

                                commutation with π

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

                                Equations
                                Instances For

                                  The left homology map data associated to the identity morphism of a short complex.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} {h₃ : S₃.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃) :
                                    (ψ.comp ψ').φK = CategoryTheory.CategoryStruct.comp ψ.φK ψ'.φK
                                    @[simp]
                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} {h₃ : S₃.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃) :
                                    (ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH

                                    The composition of left homology map data.

                                    Equations
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₂} {γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
                                      γ₁.φH = γ₂.φH
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₂} {γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
                                      γ₁.φK = γ₂.φK
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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) :
                                      (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂
                                      @[simp]
                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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) :
                                      (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φK = φ.τ₂

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

                                      Equations
                                      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 left 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
                                        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 left 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
                                          Instances For

                                            When both maps S.f and S.g of a short complex S are zero, this is the left homology map data (for the identity of S) which relates the left 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 left homology map data (for the identity of S) which relates the left homology data LeftHomologyData.ofIsLimitKernelFork and ofZeros .

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

                                                The left homology of a short complex, given by the H field of a chosen left homology data.

                                                Equations
                                                • S.leftHomology = S.leftHomologyData.H
                                                Instances For

                                                  The cycles of a short complex, given by the K field of a chosen left homology data.

                                                  Equations
                                                  • S.cycles = S.leftHomologyData.K
                                                  Instances For

                                                    The "homology class" map S.cycles ⟶ S.leftHomology.

                                                    Equations
                                                    • S.leftHomologyπ = S.leftHomologyData
                                                    Instances For

                                                      The inclusion S.cycles ⟶ S.X₂.

                                                      Equations
                                                      • S.iCycles = S.leftHomologyData.i
                                                      Instances For

                                                        The "boundaries" map S.X₁ ⟶ S.cycles. (Note that in this homology API, we make no use of the "image" of this morphism, which under some categorical assumptions would be a subobject of S.X₂ contained in S.cycles.)

                                                        Equations
                                                        • S.toCycles = S.leftHomologyData.f'
                                                        Instances For
                                                          theorem CategoryTheory.ShortComplex.leftHomology_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] {A : C} (f₁ : S.leftHomology A) (f₂ : S.leftHomology A) :
                                                          f₁ = f₂ CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂
                                                          theorem CategoryTheory.ShortComplex.leftHomology_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] {A : C} (f₁ : S.leftHomology A) (f₂ : S.leftHomology A) (h : CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂) :
                                                          f₁ = f₂
                                                          theorem CategoryTheory.ShortComplex.cycles_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] {A : C} (f₁ : A S.cycles) (f₂ : A S.cycles) :
                                                          theorem CategoryTheory.ShortComplex.cycles_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] {A : C} (f₁ : A S.cycles) (f₂ : A S.cycles) (h : CategoryTheory.CategoryStruct.comp f₁ S.iCycles = CategoryTheory.CategoryStruct.comp f₂ S.iCycles) :
                                                          f₁ = f₂
                                                          @[simp]
                                                          theorem CategoryTheory.ShortComplex.cyclesIsoX₂_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] (hg : S.g = 0) :
                                                          (S.cyclesIsoX₂ hg).hom = S.iCycles
                                                          noncomputable def CategoryTheory.ShortComplex.cyclesIsoX₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] (hg : S.g = 0) :
                                                          S.cycles S.X₂

                                                          When S.g = 0, this is the canonical isomorphism S.cycles ≅ S.X₂ induced by S.iCycles.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] (hf : S.f = 0) :
                                                            (S.cyclesIsoLeftHomology hf).hom = S.leftHomologyπ
                                                            noncomputable def CategoryTheory.ShortComplex.cyclesIsoLeftHomology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] (hf : S.f = 0) :
                                                            S.cycles S.leftHomology

                                                            When S.f = 0, this is the canonical isomorphism S.cycles ≅ S.leftHomology induced by S.leftHomologyπ.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              @[simp]
                                                              theorem CategoryTheory.ShortComplex.cyclesIsoLeftHomology_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] (hf : S.f = 0) {Z : C} (h : S.leftHomology Z) :
                                                              CategoryTheory.CategoryStruct.comp (S.cyclesIsoLeftHomology hf).inv (CategoryTheory.CategoryStruct.comp S.leftHomologyπ h) = h

                                                              The (unique) left homology map data associated to a morphism of short complexes that are both equipped with left homology data.

                                                              Equations
                                                              Instances For
                                                                def CategoryTheory.ShortComplex.leftHomologyMap' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                                                                h₁.H h₂.H

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

                                                                Equations
                                                                Instances For
                                                                  def CategoryTheory.ShortComplex.cyclesMap' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                                                                  h₁.K h₂.K

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

                                                                  Equations
                                                                  Instances For
                                                                    noncomputable def CategoryTheory.ShortComplex.leftHomologyMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [S₁.HasLeftHomology] [S₂.HasLeftHomology] (φ : S₁ S₂) :
                                                                    S₁.leftHomology S₂.leftHomology

                                                                    The (left) homology map S₁.leftHomology ⟶ S₂.leftHomology induced by a morphism S₁ ⟶ S₂ of short complexes.

                                                                    Equations
                                                                    Instances For
                                                                      noncomputable def CategoryTheory.ShortComplex.cyclesMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} [S₁.HasLeftHomology] [S₂.HasLeftHomology] (φ : S₁ S₂) :
                                                                      S₁.cycles S₂.cycles

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

                                                                      Equations
                                                                      Instances For
                                                                        theorem CategoryTheory.ShortComplex.cyclesMap'_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ S₂) (φ₂ : S₂ S₃) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData) :
                                                                        def CategoryTheory.ShortComplex.leftHomologyMapIso' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                                                                        h₁.H h₂.H

                                                                        An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the H fields of left homology data of S₁ and S₂.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          @[simp]
                                                                          def CategoryTheory.ShortComplex.cyclesMapIso' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                                                                          h₁.K h₂.K

                                                                          An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the K fields of left homology data of S₁ and S₂.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            noncomputable def CategoryTheory.ShortComplex.leftHomologyMapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
                                                                            S₁.leftHomology S₂.leftHomology

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

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              noncomputable def CategoryTheory.ShortComplex.cyclesMapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
                                                                              S₁.cycles S₂.cycles

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

                                                                              Equations
                                                                              Instances For
                                                                                noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [S.HasLeftHomology] :
                                                                                S.leftHomology h.H

                                                                                The isomorphism S.leftHomology ≅ h.H induced by a left homology data h for a short complex S.

                                                                                Equations
                                                                                Instances For
                                                                                  noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [S.HasLeftHomology] :
                                                                                  S.cycles h.K

                                                                                  The isomorphism S.cycles ≅ h.K induced by a left homology data h for a short complex S.

                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₁.HasLeftHomology] [S₂.HasLeftHomology] :
                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₁.HasLeftHomology] [S₂.HasLeftHomology] :
                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₁.HasLeftHomology] [S₂.HasLeftHomology] :
                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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₁.HasLeftHomology] [S₂.HasLeftHomology] :

                                                                                    The left homology functor ShortComplex C ⥤ C, where the left homology of a short complex S is understood as a cokernel of the obvious map S.toCycles : S.X₁ ⟶ S.cycles where S.cycles is a kernel of S.g : S.X₂ ⟶ S.X₃.

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

                                                                                      The cycles functor ShortComplex C ⥤ C which sends a short complex S to S.cycles which is a kernel of S.g : S.X₂ ⟶ S.X₃.

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

                                                                                        The natural transformation S.cycles ⟶ S.X₂ for all short complexes S.

                                                                                        Equations
                                                                                        Instances For

                                                                                          The natural transformation S.X₁ ⟶ S.cycles for all short complexes S.

                                                                                          Equations
                                                                                          Instances For

                                                                                            If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a left homology data for S₁ induces a left homology data for S₂ with the same K and H fields. 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 left homology data for S₂ induces a left homology data for S₁ with the same K and H fields. The inverse construction is ofEpiOfIsIsoOfMono.

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

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

                                                                                                Equations
                                                                                                Instances For

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

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

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

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

                                                                                                      If a morphism of short complexes φ : S₁ ⟶ S₂ is such that φ.τ₁ is epi, φ.τ₂ is an iso, and φ.τ₃ is mono, then the induced morphism on left homology is an isomorphism.

                                                                                                      Equations
                                                                                                      • =
                                                                                                      noncomputable def CategoryTheory.ShortComplex.liftCycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] :
                                                                                                      A S.cycles

                                                                                                      A morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0 lifts to a morphism A ⟶ S.cycles.

                                                                                                      Equations
                                                                                                      • S.liftCycles k hk = S.leftHomologyData.liftK k hk
                                                                                                      Instances For

                                                                                                        Via S.iCycles : S.cycles ⟶ S.X₂, the object S.cycles identifies to the kernel of S.g : S.X₂ ⟶ S.X₃.

                                                                                                        Equations
                                                                                                        • S.cyclesIsKernel = S.leftHomologyData.hi
                                                                                                        Instances For

                                                                                                          The canonical isomorphism S.cycles ≅ kernel S.g.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            noncomputable def CategoryTheory.ShortComplex.liftLeftHomology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : A S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] :
                                                                                                            A S.leftHomology

                                                                                                            The morphism A ⟶ S.leftHomology obtained from a morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Via S.leftHomologyπ : S.cycles ⟶ S.leftHomology, the object S.leftHomology identifies to the cokernel of S.toCycles : S.X₁ ⟶ S.cycles.

                                                                                                              Equations
                                                                                                              • S.leftHomologyIsCokernel = S.leftHomologyData.hπ
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                @[simp]
                                                                                                                theorem CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] :
                                                                                                                CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) h.cyclesIso.hom = h.liftK k hk
                                                                                                                @[simp]
                                                                                                                theorem CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] {Z : C} (h : S.cycles Z) :
                                                                                                                @[simp]
                                                                                                                theorem CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [S.HasLeftHomology] :
                                                                                                                CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.cyclesIso.inv = S.liftCycles k hk

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

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  The following lemmas and instance gives a sufficient condition for a morphism of short complexes to induce an isomorphism on cycles.