Documentation

Mathlib.Algebra.Homology.ShortComplex.Homology

Homology of short complexes #

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

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

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

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

Instances For

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

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

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

      Equations
      Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                      Equations
                      Instances For

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

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

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

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

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

                            Instances

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

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

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                    Equations
                                                    Instances For

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

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

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

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

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

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

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

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

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

                                                              Instances

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

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

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

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

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

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

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

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

                                                                        The natural isomorphism (homologyFunctor C).op ≅ opFunctor C ⋙ homologyFunctor Cᵒᵖ which relates the homology in C and in Cᵒᵖ.

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