Documentation

Mathlib.Algebra.Homology.ShortComplex.Preadditive

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.

@[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₂) :
(φ + φ').τ₁ = φ.τ₁ + φ'.τ₁
@[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₂) :
(φ + φ').τ₂ = φ.τ₂ + φ'.τ₂
@[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₂) :
(φ + φ').τ₃ = φ.τ₃ + φ'.τ₃
@[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₂) :
(φ - φ').τ₁ = φ.τ₁ - φ'.τ₁
@[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₂) :
(φ - φ').τ₂ = φ.τ₂ - φ'.τ₂
@[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₂) :
(φ - φ').τ₃ = φ.τ₃ - φ'.τ₃

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

Instances For

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

    Instances For