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

      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.

      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

        Instances For

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

          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

            Instances For

              When the second map S.g is zero, this is the 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 homology data on S

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

                  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.

                    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.

                      Instances For

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

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

                          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.

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

                              Instances For

                                The homology of a short complex is the left.H field of a chosen homology data.

                                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.

                                  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.

                                    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.

                                      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.

                                        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.

                                            Instances For