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.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₂)
@[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₂)
:
@[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₂)
:
@[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₂)
:
@[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₂)
:
@[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₂)
:
@[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₂)
:
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₂)
:
Given a left homology map data for morphism φ
, this is induced left homology
map data for -φ
.
Instances For
@[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
@[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
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
@[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₂)
:
@[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₂
@[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₂
@[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₂
@[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₂
@[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₂
@[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₂]
:
@[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₂]
:
@[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₂]
:
@[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₂]
:
@[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₂]
:
@[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₂]
: