Documentation

Mathlib.Algebra.Homology.ShortComplex.RightHomology

Right Homology of short complexes #

In this file, we define the dual notions to those defined in Algebra.Homology.ShortComplex.LeftHomology. In particular, if S : ShortComplex C is a short complex consisting of two composable maps f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0, we define h : S.RightHomologyData to be the datum of morphisms p : X₂ ⟶ Q and ι : HQ such that Q identifies to the cokernel of f and H to the kernel of the induced map g' : Q ⟶ X₃.

When such a S.RightHomologyData exists, we shall say that [S.HasRightHomology] and we define S.rightHomology to be the H field of a chosen right homology data. Similarly, we define S.opcycles to be the Q field.

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 right homology data for a short complex S consists of morphisms p : S.X₂ ⟶ Q and ι : HQ such that p identifies Q to the kernel of f : S.X₁ ⟶ S.X₂, and that ι identifies H to the kernel of the induced map g' : Q ⟶ S.X₃

Instances For

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

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

      Any morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism Q ⟶ A

      Equations
      Instances For

        The morphism from the (right) homology attached to a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0.

        Equations
        Instances For

          The morphism h.Q ⟶ S.X₃ induced by S.g : S.X₂ ⟶ S.X₃ and the fact that h.Q is a cokernel of S.f : S.X₁ ⟶ S.X₂.

          Equations
          • h.g' = h.descQ S.g
          Instances For

            For h : S.RightHomologyData, this is a restatement of h., saying that ι : h.H ⟶ h.Q is a kernel of h.g' : h.Q ⟶ S.X₃.

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

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

              Equations
              Instances For

                When the first map S.f is zero, this is the right 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 right 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 right homology data on S given by any colimit cokernel cofork of 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 right 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 right homology data on S

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

                          A short complex S has right homology when there exists a S.RightHomologyData

                          • condition : Nonempty S.RightHomologyData
                          Instances

                            A chosen S.RightHomologyData for a short complex S that has right homology

                            Equations
                            • S.rightHomologyData = .some
                            Instances For

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

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

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

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

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

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

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      structure CategoryTheory.ShortComplex.RightHomologyMapData {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                      Type u_2

                                      Given right homology data h₁ and h₂ for two short complexes S₁ and S₂, a RightHomologyMapData for a morphism φ : S₁ ⟶ S₂ consists of a description of the induced morphisms on the Q (opcycles) and H (right homology) fields of h₁ and h₂.

                                      Instances For
                                        @[simp]

                                        commutation with p

                                        @[simp]

                                        commutation with g'

                                        @[simp]

                                        commutation with ι

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

                                        Equations
                                        Instances For

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

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃) :
                                            (ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH
                                            @[simp]
                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ {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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃) :
                                            (ψ.comp ψ').φQ = CategoryTheory.CategoryStruct.comp ψ.φQ ψ'.φQ

                                            The composition of right homology map data.

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

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

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

                                                    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 right homology map data (for the identity of S) which relates the right homology data ofZeros and ofIsColimitCokernelCofork.

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

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

                                                        Equations
                                                        • S.rightHomology = S.rightHomologyData.H
                                                        Instances For

                                                          The "opcycles" of a short complex, given by the Q field of a chosen right homology data. This is the dual notion to cycles.

                                                          Equations
                                                          • S.opcycles = S.rightHomologyData.Q
                                                          Instances For

                                                            The canonical map S.rightHomology ⟶ S.opcycles.

                                                            Equations
                                                            • S.rightHomologyι = S.rightHomologyData
                                                            Instances For

                                                              The projection S.X₂ ⟶ S.opcycles.

                                                              Equations
                                                              • S.pOpcycles = S.rightHomologyData.p
                                                              Instances For

                                                                The canonical map S.opcycles ⟶ X₃.

                                                                Equations
                                                                • S.fromOpcycles = S.rightHomologyData.g'
                                                                Instances For
                                                                  theorem CategoryTheory.ShortComplex.rightHomology_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {A : C} (f₁ : A S.rightHomology) (f₂ : A S.rightHomology) :
                                                                  f₁ = f₂ CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι
                                                                  theorem CategoryTheory.ShortComplex.rightHomology_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {A : C} (f₁ : A S.rightHomology) (f₂ : A S.rightHomology) (h : CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι) :
                                                                  f₁ = f₂
                                                                  theorem CategoryTheory.ShortComplex.opcycles_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {A : C} (f₁ : S.opcycles A) (f₂ : S.opcycles A) :
                                                                  theorem CategoryTheory.ShortComplex.opcycles_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {A : C} (f₁ : S.opcycles A) (f₂ : S.opcycles A) (h : CategoryTheory.CategoryStruct.comp S.pOpcycles f₁ = CategoryTheory.CategoryStruct.comp S.pOpcycles f₂) :
                                                                  f₁ = f₂
                                                                  @[simp]
                                                                  theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) :
                                                                  (S.opcyclesIsoX₂ hf).inv = S.pOpcycles
                                                                  noncomputable def CategoryTheory.ShortComplex.opcyclesIsoX₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hf : S.f = 0) :
                                                                  S.opcycles S.X₂

                                                                  When S.f = 0, this is the canonical isomorphism S.opcycles ≅ S.X₂ induced by S.pOpcycles.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) :
                                                                    (S.opcyclesIsoRightHomology hg).inv = S.rightHomologyι
                                                                    noncomputable def CategoryTheory.ShortComplex.opcyclesIsoRightHomology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) :
                                                                    S.opcycles S.rightHomology

                                                                    When S.g = 0, this is the canonical isomorphism S.opcycles ≅ S.rightHomology induced by S.rightHomologyι.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.rightHomology Z) :
                                                                      CategoryTheory.CategoryStruct.comp S.rightHomologyι (CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom h) = h
                                                                      @[simp]
                                                                      theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.opcycles Z) :
                                                                      CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom (CategoryTheory.CategoryStruct.comp S.rightHomologyι h) = h

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

                                                                      Equations
                                                                      Instances For
                                                                        def CategoryTheory.ShortComplex.rightHomologyMap' {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                                                        h₁.H h₂.H

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

                                                                        Equations
                                                                        Instances For
                                                                          def CategoryTheory.ShortComplex.opcyclesMap' {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                                                          h₁.Q h₂.Q

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

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

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

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

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

                                                                              Equations
                                                                              Instances For
                                                                                theorem CategoryTheory.ShortComplex.opcyclesMap'_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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
                                                                                def CategoryTheory.ShortComplex.rightHomologyMapIso' {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                                                                h₁.H h₂.H

                                                                                An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the H fields of right 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.opcyclesMapIso' {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                                                                  h₁.Q h₂.Q

                                                                                  An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the Q fields of right 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.rightHomologyMapIso {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₁.HasRightHomology] [S₂.HasRightHomology] :
                                                                                    S₁.rightHomology S₂.rightHomology

                                                                                    The isomorphism S₁.rightHomology ≅ S₂.rightHomology 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.opcyclesMapIso {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₁.HasRightHomology] [S₂.HasRightHomology] :
                                                                                      S₁.opcycles S₂.opcycles

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

                                                                                      Equations
                                                                                      Instances For
                                                                                        noncomputable def CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] :
                                                                                        S.rightHomology h.H

                                                                                        The isomorphism S.rightHomology ≅ h.H induced by a right homology data h for a short complex S.

                                                                                        Equations
                                                                                        Instances For
                                                                                          noncomputable def CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [S.HasRightHomology] :
                                                                                          S.opcycles h.Q

                                                                                          The isomorphism S.opcycles ≅ h.Q induced by a right homology data h for a short complex S.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
                                                                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
                                                                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
                                                                                            theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :

                                                                                            The right homology functor ShortComplex C ⥤ C, where the right homology of a short complex S is understood as a kernel of the obvious map S.fromOpcycles : S.opcycles ⟶ S.X₃ where S.opcycles is a cokernel of S.f : S.X₁ ⟶ S.X₂.

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

                                                                                              The opcycles functor ShortComplex C ⥤ C which sends a short complex S to S.opcycles which is a cokernel of S.f : S.X₁ ⟶ S.X₂.

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

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

                                                                                                Equations
                                                                                                Instances For

                                                                                                  The natural transformation S.opcycles ⟶ S.X₃ for all short complexes S.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φ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₂) :
                                                                                                    ψ.op.φH = ψ.φH.op
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ {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₂) :
                                                                                                    ψ.op.φQ = ψ.φK.op

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

                                                                                                    Equations
                                                                                                    • ψ.op = { φQ := ψ.φK.op, φH := ψ.φH.op, commp := , commg' := , commι := }
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φ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₂) :
                                                                                                      ψ.unop.φH = ψ.φH.unop
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ {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₂) :
                                                                                                      ψ.unop.φQ = ψ.φK.unop

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

                                                                                                      Equations
                                                                                                      • ψ.unop = { φQ := ψ.φK.unop, φH := ψ.φH.unop, commp := , commg' := , commι := }
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φ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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
                                                                                                        ψ.op.φH = ψ.φH.op
                                                                                                        @[simp]
                                                                                                        theorem CategoryTheory.ShortComplex.RightHomologyMapData.op_φ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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
                                                                                                        ψ.op.φK = ψ.φQ.op

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

                                                                                                        Equations
                                                                                                        • ψ.op = { φK := ψ.φQ.op, φH := ψ.φH.op, commi := , commf' := , commπ := }
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φ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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
                                                                                                          ψ.unop.φH = ψ.φH.unop
                                                                                                          @[simp]
                                                                                                          theorem CategoryTheory.ShortComplex.RightHomologyMapData.unop_φ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₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
                                                                                                          ψ.unop.φK = ψ.φQ.unop

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

                                                                                                          Equations
                                                                                                          • ψ.unop = { φK := ψ.φQ.unop, φH := ψ.φH.unop, commi := , commf' := , commπ := }
                                                                                                          Instances For

                                                                                                            The right homology in the opposite category of the opposite of a short complex identifies to the left homology of this short complex.

                                                                                                            Equations
                                                                                                            • S.rightHomologyOpIso = S.leftHomologyData.op.rightHomologyIso
                                                                                                            Instances For

                                                                                                              The left homology in the opposite category of the opposite of a short complex identifies to the right homology of this short complex.

                                                                                                              Equations
                                                                                                              • S.leftHomologyOpIso = S.rightHomologyData.op.leftHomologyIso
                                                                                                              Instances For

                                                                                                                The opcycles in the opposite category of the opposite of a short complex identifies to the cycles of this short complex.

                                                                                                                Equations
                                                                                                                • S.opcyclesOpIso = S.leftHomologyData.op.opcyclesIso
                                                                                                                Instances For

                                                                                                                  The cycles in the opposite category of the opposite of a short complex identifies to the opcycles of this short complex.

                                                                                                                  Equations
                                                                                                                  • S.cyclesOpIso = S.rightHomologyData.op.cyclesIso
                                                                                                                  Instances For
                                                                                                                    noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono {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₁.RightHomologyData) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] :
                                                                                                                    S₂.RightHomologyData

                                                                                                                    If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₁ induces a right homology data for S₂ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono'. The inverse construction is ofEpiOfIsIsoOfMono'.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' {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₂.RightHomologyData) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃] :
                                                                                                                      S₁.RightHomologyData

                                                                                                                      If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₂ induces a right homology data for S₁ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono. The inverse construction is ofEpiOfIsIsoOfMono.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        noncomputable def CategoryTheory.ShortComplex.RightHomologyData.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₁.RightHomologyData) :
                                                                                                                        S₂.RightHomologyData

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

                                                                                                                        Equations
                                                                                                                        Instances For

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

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

                                                                                                                            This right homology map data expresses compatibilities of the right homology data constructed by RightHomologyData.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 right homology is an isomorphism.

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

                                                                                                                              A morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.opcycles ⟶ A.

                                                                                                                              Equations
                                                                                                                              • S.descOpcycles k hk = S.rightHomologyData.descQ k hk
                                                                                                                              Instances For
                                                                                                                                theorem CategoryTheory.ShortComplex.descOpcycles_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [S.HasRightHomology] {A' : C} (α : A A') :
                                                                                                                                CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) α = S.descOpcycles (CategoryTheory.CategoryStruct.comp k α)

                                                                                                                                Via S.pOpcycles : S.X₂ ⟶ S.opcycles, the object S.opcycles identifies to the cokernel of S.f : S.X₁ ⟶ S.X₂.

                                                                                                                                Equations
                                                                                                                                • S.opcyclesIsCokernel = S.rightHomologyData.hp
                                                                                                                                Instances For

                                                                                                                                  The canonical isomorphism S.opcycles ≅ cokernel S.f.

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

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

                                                                                                                                    Equations
                                                                                                                                    Instances For

                                                                                                                                      Via S.rightHomologyι : S.rightHomology ⟶ S.opcycles, the object S.rightHomology identifies to the kernel of S.fromOpcycles : S.opcycles ⟶ S.X₃.

                                                                                                                                      Equations
                                                                                                                                      • S.rightHomologyIsKernel = S.rightHomologyData.hι
                                                                                                                                      Instances For
                                                                                                                                        @[simp]
                                                                                                                                        theorem CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [S.HasRightHomology] :
                                                                                                                                        CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv (S.descOpcycles k hk) = h.descQ k hk
                                                                                                                                        @[simp]
                                                                                                                                        theorem CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_hom_comp_descQ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [S.HasRightHomology] :
                                                                                                                                        CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom (h.descQ k hk) = S.descOpcycles k hk

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

                                                                                                                                        Equations
                                                                                                                                        Instances For

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