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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.ShortComplex C} : Add (S₁ ⟶ S₂)

Equations

• CategoryTheory.ShortComplex.instAddHom = { add := fun (φ φ' : S₁ ⟶ S₂) => { τ₁ := φ.τ₁ + φ'.τ₁, τ₂ := φ.τ₂ + φ'.τ₂, τ₃ := φ.τ₃ + φ'.τ₃, comm₁₂ := ⋯, comm₂₃ := ⋯ } }

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

Equations

• CategoryTheory.ShortComplex.instSubHom = { sub := fun (φ φ' : S₁ ⟶ S₂) => { τ₁ := φ.τ₁ - φ'.τ₁, τ₂ := φ.τ₂ - φ'.τ₂, τ₃ := φ.τ₃ - φ'.τ₃, comm₁₂ := ⋯, comm₂₃ := ⋯ } }

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

Equations

• CategoryTheory.ShortComplex.instNegHom = { neg := fun (φ : S₁ ⟶ S₂) => { τ₁ := -φ.τ₁, τ₂ := -φ.τ₂, τ₃ := -φ.τ₃, comm₁₂ := ⋯, comm₂₃ := ⋯ } }

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

Equations

• CategoryTheory.ShortComplex.instAddCommGroupHom = AddCommGroup.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.ShortComplex.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

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

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

Equations

• γ.neg = { φK := -γ.φK, φH := -γ.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• γ.add γ' = { φK := γ.φK + γ'.φK, φH := γ.φH + γ'.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• γ.neg = { φQ := -γ.φQ, φH := -γ.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• γ.add γ' = { φQ := γ.φQ + γ'.φQ, φH := γ.φH + γ'.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• γ.neg = { left := γ.left.neg, right := γ.right.neg }

@[simp]

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

@[simp]

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

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

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

Equations

• γ.add γ' = { left := γ.left.add γ'.left, right := γ.right.add γ'.right }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

structure CategoryTheory.ShortComplex.Homotopy {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.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 : CategoryTheory.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₃ : CategoryTheory.CategoryStruct.comp S₁.g self.h₃ = 0
• comm₁ : φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
• comm₂ : φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g self.h₂ + CategoryTheory.CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
• comm₃ : φ₁.τ₃ = self.h₃ + CategoryTheory.CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃

theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} {inst✝ : CategoryTheory.Category.{u_2, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {x y : CategoryTheory.ShortComplex.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.h₀ (CategoryTheory.CategoryStruct.comp S₂.f h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

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

The obvious homotopy between two equal morphisms of short complexes.

Equations

• CategoryTheory.ShortComplex.Homotopy.ofEq h = { h₀ := 0, h₀_f := ⋯, h₁ := 0, h₂ := 0, h₃ := 0, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.ShortComplex.Homotopy.refl φ = CategoryTheory.ShortComplex.Homotopy.ofEq ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The symmetry of homotopy between morphisms of short complexes.

Equations

• h.symm = { h₀ := -h.h₀, h₀_f := ⋯, h₁ := -h.h₁, h₂ := -h.h₂, h₃ := -h.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• h.neg = { h₀ := -h.h₀, h₀_f := ⋯, h₁ := -h.h₁, h₂ := -h.h₂, h₃ := -h.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The transitivity of homotopy between morphisms of short complexes.

Equations

• h₁₂.trans h₂₃ = { h₀ := h₁₂.h₀ + h₂₃.h₀, h₀_f := ⋯, h₁ := h₁₂.h₁ + h₂₃.h₁, h₂ := h₁₂.h₂ + h₂₃.h₂, h₃ := h₁₂.h₃ + h₂₃.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy between morphisms of short complexes is compatible with addition.

Equations

• h.add h' = { h₀ := h.h₀ + h'.h₀, h₀_f := ⋯, h₁ := h.h₁ + h'.h₁, h₂ := h.h₂ + h'.h₂, h₃ := h.h₃ + h'.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy between morphisms of short complexes is compatible with subtraction.

Equations

• h.sub h' = { h₀ := h.h₀ - h'.h₀, h₀_f := ⋯, h₁ := h.h₁ - h'.h₁, h₂ := h.h₂ - h'.h₂, h₃ := h.h₃ - h'.h₃, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy between morphisms of short complexes is compatible with precomposition.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy between morphisms of short complexes is compatible with postcomposition.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy between morphisms of short complexes is compatible with composition.

Equations

• h.comp h' = (h.compRight ψ₁).trans (h'.compLeft φ₂)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• h.op = { h₀ := h.h₃.op, h₀_f := ⋯, h₁ := h.h₂.op, h₂ := h.h₁.op, h₃ := h.h₀.op, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• h.unop = { h₀ := h.h₃.unop, h₀_f := ⋯, h₁ := h.h₂.unop, h₂ := h.h₁.unop, h₃ := h.h₀.unop, g_h₃ := ⋯, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

A morphism constructed with nullHomotopic is homotopic to zero.

Equations

• CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃ = { h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) : CategoryTheory.ShortComplex.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) : CategoryTheory.ShortComplex.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) : CategoryTheory.ShortComplex.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ S₂ : CategoryTheory.ShortComplex C) [S₁.HasLeftHomology] [S₂.HasLeftHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) : CategoryTheory.ShortComplex.leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

@[simp]

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

@[simp]

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

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

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

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

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

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

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

structure CategoryTheory.ShortComplex.HomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ S₂ : CategoryTheory.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 : CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp self.hom self.inv) (CategoryTheory.CategoryStruct.id S₁)

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

• homotopyInvHomId : CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp self.inv self.hom) (CategoryTheory.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 {C : Type u_1} {inst✝ : CategoryTheory.Category.{u_2, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.HomotopyEquiv S₂} (hom : x.hom = y.hom) (inv : x.inv = y.inv) (homotopyHomInvId : HEq x.homotopyHomInvId y.homotopyHomInvId) (homotopyInvHomId : HEq x.homotopyInvHomId y.homotopyInvHomId) : x = y

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The inverse of a homotopy equivalence.

Equations

• e.symm = { hom := e.inv, inv := e.hom, homotopyHomInvId := e.homotopyInvHomId, homotopyInvHomId := e.homotopyHomInvId }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The composition of homotopy equivalences.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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