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

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

    Instances For

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

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

        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

          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

            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

              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

                Instances For

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

                  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
                      @[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.

                      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₂.ι.

                        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.

                          Instances For

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

                            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.

                              Instances For

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

                                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.

                                  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.

                                    Instances For

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

                                      Instances For

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

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

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

                                            Instances For

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

                                              Instances For

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

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

                                                  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.

                                                    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.

                                                      Instances For