Documentation

@[implicit_reducible]

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

Sub (S₁ ⟶ S₂)

@[implicit_reducible]

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

Neg (S₁ ⟶ S₂)

@[implicit_reducible]

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

AddCommGroup (S₁ ⟶ S₂)

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[implicit_reducible]

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

Preadditive (ShortComplex C)

def CategoryTheory.ShortComplex.LeftHomologyMapData.neg {C : Type u_1} [Category.{v_1, 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 -φ.

Instances For

@[simp]

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

γ.neg.φK = -γ.φK

@[simp]

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

γ.neg.φH = -γ.φH

def CategoryTheory.ShortComplex.LeftHomologyMapData.add {C : Type u_1} [Category.{v_1, 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 φ + φ'.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] [Limits.HasKernels C] [Limits.HasCokernels C] :

(leftHomologyFunctor C).Additive

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

(cyclesFunctor C).Additive

def CategoryTheory.ShortComplex.RightHomologyMapData.neg {C : Type u_1} [Category.{v_1, 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 -φ.

Instances For

@[simp]

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

γ.neg.φQ = -γ.φQ

@[simp]

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

γ.neg.φH = -γ.φH

def CategoryTheory.ShortComplex.RightHomologyMapData.add {C : Type u_1} [Category.{v_1, 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 φ + φ'.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] [Limits.HasKernels C] [Limits.HasCokernels C] :

(rightHomologyFunctor C).Additive

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

(opcyclesFunctor C).Additive

def CategoryTheory.ShortComplex.HomologyMapData.neg {C : Type u_1} [Category.{v_1, 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 -φ.

Instances For

@[simp]

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

γ.neg.right = γ.right.neg

@[simp]

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

γ.neg.left = γ.left.neg

def CategoryTheory.ShortComplex.HomologyMapData.add {C : Type u_1} [Category.{v_1, 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 φ + φ'.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.HomologyMapData.add_right {C : Type u_1} [Category.{v_1, 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.HomologyMapData.add_left {C : Type u_1} [Category.{v_1, 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.homologyMap'_neg {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] [CategoryWithHomology C] :

(homologyFunctor C).Additive

🔶 coverage

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

Type v_1

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 + φ₂.τ₃

Instances For

theorem CategoryTheory.ShortComplex.Homotopy.ext_iff {C : Type u_1} {inst✝ : Category.{v_1, 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₃

theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} {inst✝ : Category.{v_1, 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

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.g_h₃_assoc {C : Type u_1} [Category.{v_1, 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

def CategoryTheory.ShortComplex.nullHomotopic {C : Type u_1} [Category.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₂ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂) :

Homotopy φ₁ φ₂

The obvious homotopy between two equal morphisms of short complexes.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₃ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) :

Homotopy φ φ

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.refl_h₁ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) :

(refl φ).h₀ = 0

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

Homotopy φ₂ φ₁

The symmetry of homotopy between morphisms of short complexes.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.symm_h₂ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.neg_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.trans_h₂ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.add_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.sub_h₃ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₂ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.comp_h₁ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.op_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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ᵒᵖ.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.unop_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₀ {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.

Instances For

def CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic {C : Type u_1} [Category.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) [S₁.HasHomology] [S₂.HasHomology] :

homologyMap φ₁ = homologyMap φ₂