Documentation

Mathlib.Algebra.Homology.ShortComplex.Linear

Homology of linear categories #

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

Equations
  • CategoryTheory.ShortComplex.instSMulHom = { smul := fun (a : R) (φ : S₁ S₂) => { τ₁ := a φ.τ₁, τ₂ := a φ.τ₂, τ₃ := a φ.τ₃, comm₁₂ := , comm₂₃ := } }
@[simp]
@[simp]
@[simp]
Equations
  • CategoryTheory.ShortComplex.instModuleHom = Module.mk
Equations
  • CategoryTheory.ShortComplex.instLinear = { homModule := inferInstance, smul_comp := , comp_smul := }
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R) :
(γ.smul a).φH = a γ.φH
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R) :
(γ.smul a).φK = a γ.φK

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
    @[simp]
    theorem CategoryTheory.ShortComplex.leftHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R) :
    @[simp]
    theorem CategoryTheory.ShortComplex.cyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R) :
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R) :
    (γ.smul a).φH = a γ.φH
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R) :
    (γ.smul a).φQ = a γ.φQ

    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
      @[simp]
      theorem CategoryTheory.ShortComplex.rightHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R) :
      @[simp]
      theorem CategoryTheory.ShortComplex.opcyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R) :
      @[simp]
      theorem CategoryTheory.ShortComplex.HomologyMapData.smul_left {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (a : R) :
      (γ.smul a).left = γ.left.smul a
      @[simp]
      theorem CategoryTheory.ShortComplex.HomologyMapData.smul_right {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (a : R) :
      (γ.smul a).right = γ.right.smul a

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

      Equations
      • γ.smul a = { left := γ.left.smul a, right := γ.right.smul a }
      Instances For
        @[simp]
        theorem CategoryTheory.ShortComplex.homologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (a : R) :
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₃ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (h.smul a).h₃ = a h.h₃
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₁ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (h.smul a).h₁ = a h.h₁
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₂ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (h.smul a).h₂ = a h.h₂
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₀ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (h.smul a).h₀ = a h.h₀

        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