Documentation

Mathlib.Algebra.Homology.ShortComplex.Abelian

Abelian categories have homology #

In this file, it is shown that all short complexes S in abelian categories have terms of type S.HomologyData.

The strategy of the proof is to study the morphism kernel.ι S.g ≫ cokernel.π S.f. We show that there is a LeftHomologyData for S for which the H field consists of the coimage of kernel.ι S.g ≫ cokernel.π S.f, while there is a RightHomologyData for which the H is the image of kernel.ι S.g ≫ cokernel.π S.f. The fact that these left and right homology data are compatible (i.e. provide a HomologyData) is obtained by using the coimage-image isomorphism in abelian categories.

source
noncomputable def CategoryTheory.ShortComplex.abelianImageToKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
CategoryTheory.Abelian.image S.f ⟶ CategoryTheory.Limits.kernel S.g

The canonical morphism Abelian.image S.f ⟶ kernel S.g for a short complex S in an abelian category.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.X₂ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι S.f) h
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.Limits.kernel.ι S.g) = CategoryTheory.Abelian.image.ι S.f
    source
    instance CategoryTheory.ShortComplex.instMonoImagePreadditiveHasZeroMorphismsToPreadditiveHasKernels_of_hasEqualizersHasEqualizersHasCokernels_of_hasCoequalizersHasCoequalizersX₁X₂FKernelX₃GHas_limitAbelianImageToKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    CategoryTheory.Mono (CategoryTheory.ShortComplex.abelianImageToKernel S)
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Limits.cokernel S.f ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) h)) = CategoryTheory.CategoryStruct.comp 0 h
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) = 0
    source
    noncomputable def CategoryTheory.ShortComplex.abelianImageToKernelIsKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.ShortComplex.abelianImageToKernel S) ⋯)

    Abelian.image S.f is the kernel of kernel.ι S.g ≫ cokernel.π S.f

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
      (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).H = CategoryTheory.Abelian.coimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
      (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).π = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
      (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).i = CategoryTheory.Limits.kernel.ι S.g
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
      (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).K = CategoryTheory.Limits.kernel S.g
      source
      noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
      CategoryTheory.ShortComplex.LeftHomologyData S

      The canonical LeftHomologyData of a short complex S in an abelian category, for which the H field is Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
        CategoryTheory.Limits.cokernel S.f ⟶ CategoryTheory.Abelian.coimage S.g

        The canonical morphism cokernel S.f ⟶ Abelian.coimage S.g for a short complex S in an abelian category.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Abelian.coimage S.g ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π S.g) h
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) = CategoryTheory.Abelian.coimage.π S.g
          source
          instance CategoryTheory.ShortComplex.instEpiCokernelPreadditiveHasZeroMorphismsToPreadditiveX₁X₂FHas_colimitHasCokernels_of_hasCoequalizersHasCoequalizersCoimageHasKernels_of_hasEqualizersHasEqualizersX₃GCokernelToAbelianCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
          CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S)
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) = 0
          source
          noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) ⋯)

          Abelian.coimage S.g is the cokernel of kernel.ι S.g ≫ cokernel.π S.f

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
            (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).H = CategoryTheory.Abelian.image (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
            source
            @[simp]
            theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
            (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).ι = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
            source
            @[simp]
            theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
            (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).Q = CategoryTheory.Limits.cokernel S.f
            source
            @[simp]
            theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
            (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).p = CategoryTheory.Limits.cokernel.π S.f
            source
            noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
            CategoryTheory.ShortComplex.RightHomologyData S

            The canonical RightHomologyData of a short complex S in an abelian category, for which the H field is Abelian.image (kernel.ι S.g ≫ cokernel.π S.f).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def CategoryTheory.ShortComplex.HomologyData.ofAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
              CategoryTheory.ShortComplex.HomologyData S

              The canonical HomologyData of a short complex S in an abelian category.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance CategoryTheory.categoryWithHomology_of_abelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] :
                CategoryTheory.CategoryWithHomology C
                Equations
                • ⋯ = ⋯
                source
                noncomputable def CategoryTheory.ShortComplex.homology'IsoHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :
                homology' S.f S.g ⋯ ≅ CategoryTheory.ShortComplex.homology S

                Comparison isomorphism between two definitions of homology.

                Equations
                Instances For