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 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
    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 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

                        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

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

                          Equations
                          Instances For
                            @[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 = φ.τ₂
                            @[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 = φ.τ₂

                            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 "opcycles" of a short complex, given by the Q field of a chosen right homology data. This is the dual notion to cycles.

                                      Equations
                                      Instances For

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

                                        Equations
                                        Instances For

                                          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

                                            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

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

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

                                                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

                                                  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

                                                    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

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

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

                                                        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

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

                                                            Equations
                                                            Instances For

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

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

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

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

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

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

                                                                              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
                                                                                    • =

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

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

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