Documentation

Mathlib.Algebra.Homology.ShortComplex.Linear

Homology of linear categories #

In this file, it is shown that if C is an R-linear category, then ShortComplex C is an R-linear category. Various homological notions are also shown to be linear.

source
@[instance_reducible]
instance CategoryTheory.ShortComplex.instSMulHom {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} :
SMul R (S₁ ⟶ S₂)
Equations
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₁ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₁ = a • φ.τ₁
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₂ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₂ = a • φ.τ₂
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₃ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₃ = a • φ.τ₃
source
@[instance_reducible]
instance CategoryTheory.ShortComplex.instModuleHom {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} :
Module R (S₁ ⟶ S₂)
Equations
source
@[instance_reducible]
instance CategoryTheory.ShortComplex.instLinear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] :
Linear R (ShortComplex C)
Equations
source
def CategoryTheory.ShortComplex.LeftHomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : LeftHomologyMapData φ h₁ h₂) (a : R) :
LeftHomologyMapData (a • φ) h₁ h₂

Given a left homology map data for morphism φ, this is the induced left homology map data for a • φ.

Equations
  • γ.smul a = { φK := a • γ.φK, φH := a • γ.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }
Instances For
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : LeftHomologyMapData φ h₁ h₂) (a : R) :
    (γ.smul a).φH = a • γ.φH
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : LeftHomologyMapData φ h₁ h₂) (a : R) :
    (γ.smul a).φK = a • γ.φK
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.leftHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R) :
    leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.cyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R) :
    cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.leftHomologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    leftHomologyMap (a • φ) = a • leftHomologyMap φ
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.cyclesMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    cyclesMap (a • φ) = a • cyclesMap φ
    source
    instance CategoryTheory.ShortComplex.leftHomologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [Limits.HasKernels C] [Limits.HasCokernels C] :
    Functor.Linear R (leftHomologyFunctor C)
    source
    instance CategoryTheory.ShortComplex.cyclesFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [Limits.HasKernels C] [Limits.HasCokernels C] :
    Functor.Linear R (cyclesFunctor C)
    source
    def CategoryTheory.ShortComplex.RightHomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) (a : R) :
    RightHomologyMapData (a • φ) h₁ h₂

    Given a right homology map data for morphism φ, this is the induced right homology map data for a • φ.

    Equations
    • γ.smul a = { φQ := a • γ.φQ, φH := a • γ.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }
    Instances For
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) (a : R) :
      (γ.smul a).φQ = a • γ.φQ
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) (a : R) :
      (γ.smul a).φH = a • γ.φH
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.rightHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R) :
      rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.opcyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R) :
      opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.rightHomologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [S₁.HasRightHomology] [S₂.HasRightHomology] :
      rightHomologyMap (a • φ) = a • rightHomologyMap φ
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.opcyclesMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [S₁.HasRightHomology] [S₂.HasRightHomology] :
      opcyclesMap (a • φ) = a • opcyclesMap φ
      source
      instance CategoryTheory.ShortComplex.rightHomologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [Limits.HasKernels C] [Limits.HasCokernels C] :
      Functor.Linear R (rightHomologyFunctor C)
      source
      instance CategoryTheory.ShortComplex.opcyclesFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [Limits.HasKernels C] [Limits.HasCokernels C] :
      Functor.Linear R (opcyclesFunctor C)
      source
      def CategoryTheory.ShortComplex.HomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) (a : R) :
      HomologyMapData (a • φ) h₁ h₂

      Given a homology map data for a morphism φ, this is the induced homology map data for a • φ.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.HomologyMapData.smul_right {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) (a : R) :
        (γ.smul a).right = γ.right.smul a
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.HomologyMapData.smul_left {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) (a : R) :
        (γ.smul a).left = γ.left.smul a
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.homologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (a : R) :
        homologyMap' (a • φ) h₁ h₂ = a • homologyMap' φ h₁ h₂
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.homologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [S₁.HasHomology] [S₂.HasHomology] :
        homologyMap (a • φ) = a • homologyMap φ
        source
        instance CategoryTheory.ShortComplex.homologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [CategoryWithHomology C] :
        Functor.Linear R (homologyFunctor C)
        source
        def CategoryTheory.ShortComplex.Homotopy.smul {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) :
        Homotopy (a • φ₁) (a • φ₂)

        Homotopy between morphisms of short complexes is compatible with the scalar multiplication.

        Equations
        • h.smul a = { h₀ := a • h.h₀, h₀_f := ⋯, h₁ := a • h.h₁, h₂ := a • h.h₂, h₃ := a • h.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.Homotopy.smul_h₀ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) :
          (h.smul a).h₀ = a • h.h₀
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.Homotopy.smul_h₁ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) :
          (h.smul a).h₁ = a • h.h₁
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.Homotopy.smul_h₃ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) :
          (h.smul a).h₃ = a • h.h₃
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.Homotopy.smul_h₂ {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) :
          (h.smul a).h₂ = a • h.h₂