Homology of preadditive categories #

In this file, it is shown that if C is a preadditive category, then ShortComplex C is a preadditive category.

TODO: Introduce the notion of homotopy of morphisms of short complexes.

instance CategoryTheory.ShortComplex.instAddHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :

Add (S₁ ⟶ S₂)

source

instance CategoryTheory.ShortComplex.instSubHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :

Sub (S₁ ⟶ S₂)

source

instance CategoryTheory.ShortComplex.instNegHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :

Neg (S₁ ⟶ S₂)

source

instance CategoryTheory.ShortComplex.instAddCommGroupHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :

AddCommGroup (S₁ ⟶ S₂)

source

@[simp]

theorem CategoryTheory.ShortComplex.add_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ + φ').τ₁ = φ.τ₁ + φ'.τ₁

source

@[simp]

theorem CategoryTheory.ShortComplex.add_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ + φ').τ₂ = φ.τ₂ + φ'.τ₂

source

@[simp]

theorem CategoryTheory.ShortComplex.add_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ + φ').τ₃ = φ.τ₃ + φ'.τ₃

source

@[simp]

theorem CategoryTheory.ShortComplex.sub_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ - φ').τ₁ = φ.τ₁ - φ'.τ₁

source

@[simp]

theorem CategoryTheory.ShortComplex.sub_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ - φ').τ₂ = φ.τ₂ - φ'.τ₂

source

@[simp]

theorem CategoryTheory.ShortComplex.sub_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) :

(φ - φ').τ₃ = φ.τ₃ - φ'.τ₃

source

@[simp]

theorem CategoryTheory.ShortComplex.neg_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) :

(-φ).τ₁ = -φ.τ₁

source

@[simp]

theorem CategoryTheory.ShortComplex.neg_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) :

(-φ).τ₂ = -φ.τ₂

source

@[simp]

theorem CategoryTheory.ShortComplex.neg_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) :

(-φ).τ₃ = -φ.τ₃

source

instance CategoryTheory.ShortComplex.instPreadditiveShortComplexPreadditiveHasZeroMorphismsInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :

CategoryTheory.Preadditive (CategoryTheory.ShortComplex C)

source

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) :

(CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ).φK = -γ.φK

source

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) :

(CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ).φH = -γ.φH

source

def CategoryTheory.ShortComplex.LeftHomologyMapData.neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) :

CategoryTheory.ShortComplex.LeftHomologyMapData (-φ) h₁ h₂

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

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :

(CategoryTheory.ShortComplex.LeftHomologyMapData.add γ γ').φK = γ.φK + γ'.φK

source

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :

(CategoryTheory.ShortComplex.LeftHomologyMapData.add γ γ').φH = γ.φH + γ'.φH

source

def CategoryTheory.ShortComplex.LeftHomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :

CategoryTheory.ShortComplex.LeftHomologyMapData (φ + φ') h₁ h₂

Given left homology map data for morphisms φ and φ', this is induced left homology map data for φ + φ'.

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.leftHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap'_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.cyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.leftHomologyMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.cyclesMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.leftHomologyMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) :

CategoryTheory.ShortComplex.cyclesMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.leftHomologyMap (-φ) = -CategoryTheory.ShortComplex.leftHomologyMap φ

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.cyclesMap (-φ) = -CategoryTheory.ShortComplex.cyclesMap φ

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.leftHomologyMap (φ + φ') = CategoryTheory.ShortComplex.leftHomologyMap φ + CategoryTheory.ShortComplex.leftHomologyMap φ'

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.cyclesMap (φ + φ') = CategoryTheory.ShortComplex.cyclesMap φ + CategoryTheory.ShortComplex.cyclesMap φ'

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.leftHomologyMap (φ - φ') = CategoryTheory.ShortComplex.leftHomologyMap φ - CategoryTheory.ShortComplex.leftHomologyMap φ'

source

@[simp]

theorem CategoryTheory.ShortComplex.cyclesMap_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (φ' : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :

CategoryTheory.ShortComplex.cyclesMap (φ - φ') = CategoryTheory.ShortComplex.cyclesMap φ - CategoryTheory.ShortComplex.cyclesMap φ'

source

instance CategoryTheory.ShortComplex.leftHomologyFunctor_additive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :

CategoryTheory.Functor.Additive (CategoryTheory.ShortComplex.leftHomologyFunctor C)

source

instance CategoryTheory.ShortComplex.cyclesFunctor_additive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :

CategoryTheory.Functor.Additive (CategoryTheory.ShortComplex.cyclesFunctor C)