Homology of preadditive categories

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

instance CategoryTheory.ShortComplex.instAddHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} : Add (S₁ ⟶ S₂)

instance CategoryTheory.ShortComplex.instSubHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} : Sub (S₁ ⟶ S₂)

instance CategoryTheory.ShortComplex.instNegHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} : Neg (S₁ ⟶ S₂)

instance CategoryTheory.ShortComplex.instAddCommGroupHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} : AddCommGroup (S₁ ⟶ S₂)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) : γ.neg.φH = -γ.φH

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) : γ.neg.φQ = -γ.φQ

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

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

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) (γ' : RightHomologyMapData φ' h₁ h₂) : (γ.add γ').φQ = γ.φQ + γ'.φQ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_neg {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap (-φ) = -rightHomologyMap φ

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_neg {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : opcyclesMap (-φ) = -opcyclesMap φ

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_add {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap (φ + φ') = rightHomologyMap φ + rightHomologyMap φ'

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_add {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : opcyclesMap (φ + φ') = opcyclesMap φ + opcyclesMap φ'

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_sub {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap (φ - φ') = rightHomologyMap φ - rightHomologyMap φ'

@[simp]

theorem CategoryTheory.ShortComplex.opcyclesMap_sub {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : opcyclesMap (φ - φ') = opcyclesMap φ - opcyclesMap φ'

instance CategoryTheory.ShortComplex.rightHomologyFunctor_additive {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasKernels C] [Limits.HasCokernels C] : (rightHomologyFunctor C).Additive

instance CategoryTheory.ShortComplex.opcyclesFunctor_additive {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasKernels C] [Limits.HasCokernels C] : (opcyclesFunctor C).Additive

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

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

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.neg_left {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) : γ.neg.left = γ.left.neg

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.neg_right {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) : γ.neg.right = γ.right.neg

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

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

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.add_left {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) (γ' : HomologyMapData φ' h₁ h₂) : (γ.add γ').left = γ.left.add γ'.left

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.add_right {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : HomologyMapData φ h₁ h₂) (γ' : HomologyMapData φ' h₁ h₂) : (γ.add γ').right = γ.right.add γ'.right

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_neg {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] : homologyMap (-φ) = -homologyMap φ

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_add {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] : homologyMap (φ + φ') = homologyMap φ + homologyMap φ'

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_sub {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ φ' : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] : homologyMap (φ - φ') = homologyMap φ - homologyMap φ'

instance CategoryTheory.ShortComplex.homologyFunctor_additive {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [CategoryWithHomology C] : (homologyFunctor C).Additive

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

A homotopy between two morphisms of short complexes S₁ ⟶ S₂ consists of various maps and conditions which will be sufficient to show that they induce the same morphism in homology.

• h₀ : S₁.X₁ ⟶ S₂.X₁

  a morphism S₁.X₁ ⟶ S₂.X₁

• h₀_f : CategoryStruct.comp self.h₀ S₂.f = 0
• h₁ : S₁.X₂ ⟶ S₂.X₁

  a morphism S₁.X₂ ⟶ S₂.X₁

• h₂ : S₁.X₃ ⟶ S₂.X₂

  a morphism S₁.X₃ ⟶ S₂.X₂

• h₃ : S₁.X₃ ⟶ S₂.X₃

  a morphism S₁.X₃ ⟶ S₂.X₃

• g_h₃ : CategoryStruct.comp S₁.g self.h₃ = 0
• comm₁ : φ₁.τ₁ = CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
• comm₂ : φ₁.τ₂ = CategoryStruct.comp S₁.g self.h₂ + CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
• comm₃ : φ₁.τ₃ = self.h₃ + CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃

theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Preadditive C} {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {x y : Homotopy φ₁ φ₂} (h₀ : x.h₀ = y.h₀) (h₁ : x.h₁ = y.h₁) (h₂ : x.h₂ = y.h₂) (h₃ : x.h₃ = y.h₃) : x = y

theorem CategoryTheory.ShortComplex.Homotopy.ext_iff {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Preadditive C} {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {x y : Homotopy φ₁ φ₂} : x = y ↔ x.h₀ = y.h₀ ∧ x.h₁ = y.h₁ ∧ x.h₂ = y.h₂ ∧ x.h₃ = y.h₃

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.g_h₃_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : Homotopy φ₁ φ₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryStruct.comp S₁.g (CategoryStruct.comp self.h₃ h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : Homotopy φ₁ φ₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryStruct.comp self.h₀ (CategoryStruct.comp S₂.f h) = CategoryStruct.comp 0 h

def CategoryTheory.ShortComplex.nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : S₁ ⟶ S₂

Constructor for null homotopic morphisms, see also Homotopy.ofNullHomotopic and Homotopy.eq_add_nullHomotopic.

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryStruct.comp S₁.f h₁

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = CategoryStruct.comp h₁ S₂.f + CategoryStruct.comp S₁.g h₂

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryStruct.comp h₂ S₂.g + h₃

def CategoryTheory.ShortComplex.Homotopy.ofEq {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) : Homotopy φ₁ φ₂

The obvious homotopy between two equal morphisms of short complexes.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) : (ofEq h).h₁ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) : (ofEq h).h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) : (ofEq h).h₃ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) : (ofEq h).h₀ = 0

def CategoryTheory.ShortComplex.Homotopy.refl {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : Homotopy φ φ

The obvious homotopy between a morphism of short complexes and itself.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.refl_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (refl φ).h₁ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.refl_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (refl φ).h₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.refl_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (refl φ).h₃ = 0

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.refl_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (refl φ).h₀ = 0

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

The symmetry of homotopy between morphisms of short complexes.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.symm_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.symm.h₂ = -h.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.symm_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.symm.h₀ = -h.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.symm_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.symm.h₁ = -h.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.symm_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.symm.h₃ = -h.h₃

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

If two maps of short complexes are homotopic, their opposites also are.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.neg_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.neg.h₀ = -h.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.neg_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.neg.h₁ = -h.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.neg_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.neg.h₂ = -h.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.neg_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.neg.h₃ = -h.h₃

def CategoryTheory.ShortComplex.Homotopy.trans {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : Homotopy φ₁ φ₂) (h₂₃ : Homotopy φ₂ φ₃) : Homotopy φ₁ φ₃

The transitivity of homotopy between morphisms of short complexes.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.trans_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : Homotopy φ₁ φ₂) (h₂₃ : Homotopy φ₂ φ₃) : (h₁₂.trans h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.trans_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : Homotopy φ₁ φ₂) (h₂₃ : Homotopy φ₂ φ₃) : (h₁₂.trans h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.trans_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : Homotopy φ₁ φ₂) (h₂₃ : Homotopy φ₂ φ₃) : (h₁₂.trans h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.trans_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : Homotopy φ₁ φ₂) (h₂₃ : Homotopy φ₂ φ₃) : (h₁₂.trans h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂

def CategoryTheory.ShortComplex.Homotopy.add {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : Homotopy (φ₁ + φ₃) (φ₂ + φ₄)

Homotopy between morphisms of short complexes is compatible with addition.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.add_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.add h').h₀ = h.h₀ + h'.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.add_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.add h').h₂ = h.h₂ + h'.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.add_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.add h').h₁ = h.h₁ + h'.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.add_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.add h').h₃ = h.h₃ + h'.h₃

def CategoryTheory.ShortComplex.Homotopy.sub {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : Homotopy (φ₁ - φ₃) (φ₂ - φ₄)

Homotopy between morphisms of short complexes is compatible with subtraction.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.sub_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.sub h').h₀ = h.h₀ - h'.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.sub_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.sub h').h₂ = h.h₂ - h'.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.sub_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.sub h').h₁ = h.h₁ - h'.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.sub_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h' : Homotopy φ₃ φ₄) : (h.sub h').h₃ = h.h₃ - h'.h₃

def CategoryTheory.ShortComplex.Homotopy.compLeft {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) : Homotopy (CategoryStruct.comp ψ φ₁) (CategoryStruct.comp ψ φ₂)

Homotopy between morphisms of short complexes is compatible with precomposition.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) : (h.compLeft ψ).h₃ = CategoryStruct.comp ψ.τ₃ h.h₃

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) : (h.compLeft ψ).h₂ = CategoryStruct.comp ψ.τ₃ h.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) : (h.compLeft ψ).h₁ = CategoryStruct.comp ψ.τ₂ h.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) : (h.compLeft ψ).h₀ = CategoryStruct.comp ψ.τ₁ h.h₀

def CategoryTheory.ShortComplex.Homotopy.compRight {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₂ ⟶ S₃) : Homotopy (CategoryStruct.comp φ₁ ψ) (CategoryStruct.comp φ₂ ψ)

Homotopy between morphisms of short complexes is compatible with postcomposition.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₂ ⟶ S₃) : (h.compRight ψ).h₃ = CategoryStruct.comp h.h₃ ψ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₂ ⟶ S₃) : (h.compRight ψ).h₂ = CategoryStruct.comp h.h₂ ψ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₂ ⟶ S₃) : (h.compRight ψ).h₀ = CategoryStruct.comp h.h₀ ψ.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (ψ : S₂ ⟶ S₃) : (h.compRight ψ).h₁ = CategoryStruct.comp h.h₁ ψ.τ₁

def CategoryTheory.ShortComplex.Homotopy.comp {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : Homotopy ψ₁ ψ₂) : Homotopy (CategoryStruct.comp φ₁ ψ₁) (CategoryStruct.comp φ₂ ψ₂)

Homotopy between morphisms of short complexes is compatible with composition.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.comp_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : Homotopy ψ₁ ψ₂) : (h.comp h').h₂ = CategoryStruct.comp h.h₂ ψ₁.τ₂ + CategoryStruct.comp φ₂.τ₃ h'.h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.comp_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : Homotopy ψ₁ ψ₂) : (h.comp h').h₁ = CategoryStruct.comp h.h₁ ψ₁.τ₁ + CategoryStruct.comp φ₂.τ₂ h'.h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.comp_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : Homotopy ψ₁ ψ₂) : (h.comp h').h₀ = CategoryStruct.comp h.h₀ ψ₁.τ₁ + CategoryStruct.comp φ₂.τ₁ h'.h₀

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.comp_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : Homotopy ψ₁ ψ₂) : (h.comp h').h₃ = CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryStruct.comp φ₂.τ₃ h'.h₃

def CategoryTheory.ShortComplex.Homotopy.op {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : Homotopy (opMap φ₁) (opMap φ₂)

The homotopy between morphisms in ShortComplex Cᵒᵖ that is induced by a homotopy between morphisms in ShortComplex C.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.op_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.op.h₂ = h.h₁.op

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.op_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.op.h₃ = h.h₀.op

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.op_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.op.h₀ = h.h₃.op

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.op_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.op.h₁ = h.h₂.op

def CategoryTheory.ShortComplex.Homotopy.unop {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : Homotopy (unopMap φ₁) (unopMap φ₂)

The homotopy between morphisms in ShortComplex C that is induced by a homotopy between morphisms in ShortComplex Cᵒᵖ.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.unop_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.unop.h₁ = h.h₂.unop

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.unop_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.unop.h₀ = h.h₃.unop

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.unop_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.unop.h₃ = h.h₀.unop

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.unop_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : h.unop.h₂ = h.h₁.unop

def CategoryTheory.ShortComplex.Homotopy.equivSubZero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ₁ φ₂ : S₁ ⟶ S₂) : Homotopy φ₁ φ₂ ≃ Homotopy (φ₁ - φ₂) 0

Equivalence expressing that two morphisms are homotopic iff their difference is homotopic to zero.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ₁ φ₂ : S₁ ⟶ S₂) (h : Homotopy φ₁ φ₂) : (equivSubZero φ₁ φ₂) h = (h.sub (refl φ₂)).trans (ofEq ⋯)

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.equivSubZero_symm_apply {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ₁ φ₂ : S₁ ⟶ S₂) (h : Homotopy (φ₁ - φ₂) 0) : (equivSubZero φ₁ φ₂).symm h = ((ofEq ⋯).trans (h.add (refl φ₂))).trans (ofEq ⋯)

theorem CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯

def CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : Homotopy (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) 0

A morphism constructed with nullHomotopic is homotopic to zero.

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₁ = h₁

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₃ = h₃

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : (ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₀ = h₀

def CategoryTheory.ShortComplex.LeftHomologyMapData.ofNullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : LeftHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

The left homology map data expressing that null homotopic maps induce the zero morphism in left homology.

def CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : RightHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

The right homology map data expressing that null homotopic maps induce the zero morphism in right homology.

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap'_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) [S₁.HasLeftHomology] [S₂.HasLeftHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) [S₁.HasRightHomology] [S₂.HasRightHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_nullHomotopic {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) [S₁.HasHomology] [S₂.HasHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryStruct.comp S₁.g h₃ = 0) : homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

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

theorem CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

theorem CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

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

theorem CategoryTheory.ShortComplex.Homotopy.rightHomologyMap_congr {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) [S₁.HasRightHomology] [S₂.HasRightHomology] : rightHomologyMap φ₁ = rightHomologyMap φ₂

theorem CategoryTheory.ShortComplex.Homotopy.homologyMap_congr {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) [S₁.HasHomology] [S₂.HasHomology] : homologyMap φ₁ = homologyMap φ₂

structure CategoryTheory.ShortComplex.HomotopyEquiv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S₁ S₂ : ShortComplex C) : Type u_2

An homotopy equivalence between two short complexes S₁ and S₂ consists of morphisms hom : S₁ ⟶ S₂ and inv : S₂ ⟶ S₁ such that both compositions hom ≫ inv and inv ≫ hom are homotopic to the identity.

• hom : S₁ ⟶ S₂

  the forward direction of a homotopy equivalence.

• inv : S₂ ⟶ S₁

  the backwards direction of a homotopy equivalence.

• homotopyHomInvId : Homotopy (CategoryStruct.comp self.hom self.inv) (CategoryStruct.id S₁)

  the composition of the two directions of a homotopy equivalence is homotopic to the identity of the source

• homotopyInvHomId : Homotopy (CategoryStruct.comp self.inv self.hom) (CategoryStruct.id S₂)

  the composition of the two directions of a homotopy equivalence is homotopic to the identity of the target

theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Preadditive C} {S₁ S₂ : ShortComplex C} {x y : S₁.HomotopyEquiv S₂} : x = y ↔ x.hom = y.hom ∧ x.inv = y.inv ∧ x.homotopyHomInvId ≍ y.homotopyHomInvId ∧ x.homotopyInvHomId ≍ y.homotopyInvHomId

theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Preadditive C} {S₁ S₂ : ShortComplex C} {x y : S₁.HomotopyEquiv S₂} (hom : x.hom = y.hom) (inv : x.inv = y.inv) (homotopyHomInvId : x.homotopyHomInvId ≍ y.homotopyHomInvId) (homotopyInvHomId : x.homotopyInvHomId ≍ y.homotopyInvHomId) : x = y

def CategoryTheory.ShortComplex.HomotopyEquiv.refl {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S : ShortComplex C) : S.HomotopyEquiv S

The homotopy equivalence from a short complex to itself that is induced by the identity.

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyHomInvId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S : ShortComplex C) : (refl S).homotopyHomInvId = Homotopy.ofEq ⋯

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_inv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S : ShortComplex C) : (refl S).inv = CategoryStruct.id S

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S : ShortComplex C) : (refl S).hom = CategoryStruct.id S

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyInvHomId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (S : ShortComplex C) : (refl S).homotopyInvHomId = Homotopy.ofEq ⋯

def CategoryTheory.ShortComplex.HomotopyEquiv.symm {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) : S₂.HomotopyEquiv S₁

The inverse of a homotopy equivalence.

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) : e.symm.hom = e.inv

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyInvHomId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) : e.symm.homotopyInvHomId = e.homotopyHomInvId

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyHomInvId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) : e.symm.homotopyHomInvId = e.homotopyInvHomId

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_inv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) : e.symm.inv = e.hom

def CategoryTheory.ShortComplex.HomotopyEquiv.trans {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) : S₁.HomotopyEquiv S₃

The composition of homotopy equivalences.

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) : (e.trans e').homotopyHomInvId = (Homotopy.ofEq ⋯).trans (((e'.homotopyHomInvId.compRight e.inv).compLeft e.hom).trans ((Homotopy.ofEq ⋯).trans e.homotopyHomInvId))

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) : (e.trans e').homotopyInvHomId = (Homotopy.ofEq ⋯).trans (((e.homotopyInvHomId.compRight e'.hom).compLeft e'.inv).trans ((Homotopy.ofEq ⋯).trans e'.homotopyInvHomId))

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) : (e.trans e').hom = CategoryStruct.comp e.hom e'.hom

@[simp]

theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_inv {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S₁ S₂ S₃ : ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) : (e.trans e').inv = CategoryStruct.comp e'.inv e.inv