# 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} [] {S₁ : } {S₂ : } :
Equations
• CategoryTheory.ShortComplex.instAddHom = { add := fun (φ φ' : S₁ S₂) => { τ₁ := φ.τ₁ + φ'.τ₁, τ₂ := φ.τ₂ + φ'.τ₂, τ₃ := φ.τ₃ + φ'.τ₃, comm₁₂ := , comm₂₃ := } }
instance CategoryTheory.ShortComplex.instSubHom {C : Type u_1} [] {S₁ : } {S₂ : } :
Sub (S₁ S₂)
Equations
• CategoryTheory.ShortComplex.instSubHom = { sub := fun (φ φ' : S₁ S₂) => { τ₁ := φ.τ₁ - φ'.τ₁, τ₂ := φ.τ₂ - φ'.τ₂, τ₃ := φ.τ₃ - φ'.τ₃, comm₁₂ := , comm₂₃ := } }
instance CategoryTheory.ShortComplex.instNegHom {C : Type u_1} [] {S₁ : } {S₂ : } :
Neg (S₁ S₂)
Equations
• CategoryTheory.ShortComplex.instNegHom = { neg := fun (φ : S₁ S₂) => { τ₁ := -φ.τ₁, τ₂ := -φ.τ₂, τ₃ := -φ.τ₃, comm₁₂ := , comm₂₃ := } }
instance CategoryTheory.ShortComplex.instAddCommGroupHom {C : Type u_1} [] {S₁ : } {S₂ : } :
Equations
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₁ = φ.τ₁ + φ'.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₂ = φ.τ₂ + φ'.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₃ = φ.τ₃ + φ'.τ₃
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₁ = φ.τ₁ - φ'.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₂ = φ.τ₂ - φ'.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₃ = φ.τ₃ - φ'.τ₃
@[simp]
theorem CategoryTheory.ShortComplex.neg_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
(-φ).τ₁ = -φ.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.neg_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
(-φ).τ₂ = -φ.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.neg_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
(-φ).τ₃ = -φ.τ₃
Equations
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) :
γ.neg.φH = -γ.φH
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) :
γ.neg.φK = -γ.φK
def CategoryTheory.ShortComplex.LeftHomologyMapData.neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) :

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π := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) (γ' : ) :
(γ.add γ').φK = γ.φK + γ'.φK
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) (γ' : ) :
(γ.add γ').φH = γ.φH + γ'.φH
def CategoryTheory.ShortComplex.LeftHomologyMapData.add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : ) (γ' : ) :

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π := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap'_neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap'_neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap'_add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap'_add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap'_sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap'_sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap_neg {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap_neg {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap_add {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap_add {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap_sub {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.cyclesMap_sub {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) :
γ.neg.φQ = -γ.φQ
@[simp]
theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) :
γ.neg.φH = -γ.φH
def CategoryTheory.ShortComplex.RightHomologyMapData.neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) :

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ι := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) (γ' : ) :
(γ.add γ').φQ = γ.φQ + γ'.φQ
@[simp]
theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φH {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) (γ' : ) :
(γ.add γ').φH = γ.φH + γ'.φH
def CategoryTheory.ShortComplex.RightHomologyMapData.add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : ) (γ' : ) :

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ι := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap'_neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap'_neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap'_add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap'_add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap'_sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap'_sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap_neg {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap_neg {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap_add {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap_add {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.rightHomologyMap_sub {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.opcyclesMap_sub {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.ShortComplex.HomologyMapData.neg_left {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) :
γ.neg.left = γ.left.neg
@[simp]
theorem CategoryTheory.ShortComplex.HomologyMapData.neg_right {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) :
γ.neg.right = γ.right.neg
def CategoryTheory.ShortComplex.HomologyMapData.neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) :

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

Equations
• γ.neg = { left := γ.left.neg, right := γ.right.neg }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.HomologyMapData.add_left {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) (γ' : ) :
@[simp]
theorem CategoryTheory.ShortComplex.HomologyMapData.add_right {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) (γ' : ) :
def CategoryTheory.ShortComplex.HomologyMapData.add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : ) (γ' : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap'_neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap'_add {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap'_sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap_neg {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap_add {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] :
@[simp]
theorem CategoryTheory.ShortComplex.homologyMap_sub {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (φ' : S₁ S₂) [S₁.HasHomology] [S₂.HasHomology] :
Equations
• =
theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } {φ₁ φ₂ : S₁ S₂} (x y : ), x.h₀ = y.h₀x.h₁ = y.h₁x.h₂ = y.h₂x.h₃ = y.h₃x = y
theorem CategoryTheory.ShortComplex.Homotopy.ext_iff {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } {φ₁ φ₂ : S₁ S₂} (x y : ), x = y x.h₀ = y.h₀ x.h₁ = y.h₁ x.h₂ = y.h₂ x.h₃ = y.h₃
structure CategoryTheory.ShortComplex.Homotopy {C : Type u_1} [] {S₁ : } {S₂ : } (φ₁ : S₁ S₂) (φ₂ : 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.

Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.h₀_f {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.g_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) :
theorem CategoryTheory.ShortComplex.Homotopy.comm₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) :
φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
theorem CategoryTheory.ShortComplex.Homotopy.comm₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) :
φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g self.h₂ + CategoryTheory.CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
theorem CategoryTheory.ShortComplex.Homotopy.comm₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) :
φ₁.τ₃ = self.h₃ + CategoryTheory.CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) {Z : C} (h : S₂.X₂ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.g_h₃_assoc {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : ) {Z : C} (h : S₂.X₃ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.nullHomotopic_τ₂ {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : = 0) :
(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ =
@[simp]
theorem CategoryTheory.ShortComplex.nullHomotopic_τ₁ {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : = 0) :
(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ +
@[simp]
theorem CategoryTheory.ShortComplex.nullHomotopic_τ₃ {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : = 0) :
(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = + h₃
def CategoryTheory.ShortComplex.nullHomotopic {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : φ₁ = φ₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : φ₁ = φ₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : φ₁ = φ₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.ofEq_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : φ₁ = φ₂) :
def CategoryTheory.ShortComplex.Homotopy.ofEq {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : φ₁ = φ₂) :

The obvious homotopy between two equal morphisms of short complexes.

Equations
• = { h₀ := 0, h₀_f := , h₁ := 0, h₂ := 0, h₃ := 0, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.refl_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.refl_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.refl_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.refl_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
def CategoryTheory.ShortComplex.Homotopy.refl {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.symm_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.symm.h₂ = -h.h₂
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.symm_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.symm.h₀ = -h.h₀
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.symm_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.symm.h₃ = -h.h₃
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.symm_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.symm.h₁ = -h.h₁
def CategoryTheory.ShortComplex.Homotopy.symm {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.neg_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.neg.h₂ = -h.h₂
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.neg_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.neg.h₁ = -h.h₁
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.neg_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.neg.h₀ = -h.h₀
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.neg_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.neg.h₃ = -h.h₃
def CategoryTheory.ShortComplex.Homotopy.neg {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.trans_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : ) (h₂₃ : ) :
(h₁₂.trans h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.trans_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : ) (h₂₃ : ) :
(h₁₂.trans h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.trans_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : ) (h₂₃ : ) :
(h₁₂.trans h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.trans_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : ) (h₂₃ : ) :
(h₁₂.trans h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃
def CategoryTheory.ShortComplex.Homotopy.trans {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : ) (h₂₃ : ) :

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.add_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.add h').h₁ = h.h₁ + h'.h₁
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.add_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.add h').h₂ = h.h₂ + h'.h₂
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.add_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.add h').h₃ = h.h₃ + h'.h₃
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.add_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.add h').h₀ = h.h₀ + h'.h₀
def CategoryTheory.ShortComplex.Homotopy.add {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.sub_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.sub h').h₂ = h.h₂ - h'.h₂
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.sub_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.sub h').h₀ = h.h₀ - h'.h₀
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.sub_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.sub h').h₃ = h.h₃ - h'.h₃
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.sub_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
(h.sub h').h₁ = h.h₁ - h'.h₁
def CategoryTheory.ShortComplex.Homotopy.sub {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : ) (h' : ) :
CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₃) (φ₂ - φ₄)

Homotopy between morphisms of short complexes is compatible with substraction.

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₃ S₁) :
(h.compLeft ψ).h₃ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₃ S₁) :
(h.compLeft ψ).h₁ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₃ S₁) :
(h.compLeft ψ).h₂ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₃ S₁) :
(h.compLeft ψ).h₀ =
def CategoryTheory.ShortComplex.Homotopy.compLeft {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₃ S₁) :

Homotopy between morphisms of short complexes is compatible with precomposition.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₂ S₃) :
(h.compRight ψ).h₀ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₂ S₃) :
(h.compRight ψ).h₂ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₂ S₃) :
(h.compRight ψ).h₁ =
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₂ S₃) :
(h.compRight ψ).h₃ =
def CategoryTheory.ShortComplex.Homotopy.compRight {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (ψ : S₂ S₃) :

Homotopy between morphisms of short complexes is compatible with postcomposition.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.comp_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : ) :
(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} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : ) :
(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} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : ) :
(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} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : ) :
(h.comp h').h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₃
def CategoryTheory.ShortComplex.Homotopy.comp {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : ) :

Homotopy between morphisms of short complexes is compatible with composition.

Equations
• h.comp h' = (h.compRight ψ₁).trans (h'.compLeft φ₂)
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.op_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.op.h₁ = h.h₂.op
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.op_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.op.h₃ = h.h₀.op
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.op_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.op.h₂ = h.h₁.op
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.op_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.op.h₀ = h.h₃.op
def CategoryTheory.ShortComplex.Homotopy.op {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.unop_h₂ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.unop.h₂ = h.h₁.unop
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.unop_h₁ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.unop.h₁ = h.h₂.unop
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.unop_h₃ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.unop.h₃ = h.h₀.unop
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.unop_h₀ {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
h.unop.h₀ = h.h₃.unop
def CategoryTheory.ShortComplex.Homotopy.unop {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :

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₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.equivSubZero_symm_apply {C : Type u_1} [] {S₁ : } {S₂ : } (φ₁ : S₁ S₂) (φ₂ : S₁ S₂) (h : ) :
.symm h = ( ()).trans
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply {C : Type u_1} [] {S₁ : } {S₂ : } (φ₁ : S₁ S₂) (φ₂ : S₁ S₂) (h : ) :
= ().trans
def CategoryTheory.ShortComplex.Homotopy.equivSubZero {C : Type u_1} [] {S₁ : } {S₂ : } (φ₁ : S₁ S₂) (φ₂ : S₁ S₂) :

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.
Instances For
theorem CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) :
φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ h.h₁ h.h₂ h.h₃
@[simp]
theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₁ {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : = 0) :
(CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂
def CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic {C : Type u_1} [] (S₁ : ) (S₂ : ) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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
Instances For
def CategoryTheory.ShortComplex.LeftHomologyMapData.ofNullHomotopic {C : Type u_1} [] {S₁ : } {S₂ : } (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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.
Instances For
def CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic {C : Type u_1} [] {S₁ : } {S₂ : } (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic {C : Type u_1} [] {S₁ : } {S₂ : } (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] {S₁ : } {S₂ : } (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] {S₁ : } {S₂ : } (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) [S₁.HasLeftHomology] [S₂.HasLeftHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) [S₁.HasRightHomology] [S₂.HasRightHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] (S₁ : ) (S₂ : ) [S₁.HasHomology] [S₂.HasHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (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} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
theorem CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
theorem CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
theorem CategoryTheory.ShortComplex.Homotopy.leftHomologyMap_congr {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
theorem CategoryTheory.ShortComplex.Homotopy.rightHomologyMap_congr {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) [S₁.HasRightHomology] [S₂.HasRightHomology] :
theorem CategoryTheory.ShortComplex.Homotopy.homologyMap_congr {C : Type u_1} [] {S₁ : } {S₂ : } {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : ) [S₁.HasHomology] [S₂.HasHomology] :
theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } (x y : S₁.HomotopyEquiv S₂), x = y x.hom = y.hom x.inv = y.inv HEq x.homotopyHomInvId y.homotopyHomInvId HEq x.homotopyInvHomId y.homotopyInvHomId
theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } (x y : S₁.HomotopyEquiv S₂), x.hom = y.homx.inv = y.invHEq x.homotopyHomInvId y.homotopyHomInvIdHEq x.homotopyInvHomId y.homotopyInvHomIdx = y
structure CategoryTheory.ShortComplex.HomotopyEquiv {C : Type u_1} [] (S₁ : ) (S₂ : ) :
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 :

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

• homotopyInvHomId :

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

Instances For
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyHomInvId {C : Type u_1} [] (S : ) :
.homotopyHomInvId =
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyInvHomId {C : Type u_1} [] (S : ) :
.homotopyInvHomId =
def CategoryTheory.ShortComplex.HomotopyEquiv.refl {C : Type u_1} [] (S : ) :
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.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyHomInvId {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁.HomotopyEquiv S₂) :
e.symm.homotopyHomInvId = e.homotopyInvHomId
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyInvHomId {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁.HomotopyEquiv S₂) :
e.symm.homotopyInvHomId = e.homotopyHomInvId
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_inv {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁.HomotopyEquiv S₂) :
e.symm.inv = e.hom
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_hom {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁.HomotopyEquiv S₂) :
e.symm.hom = e.inv
def CategoryTheory.ShortComplex.HomotopyEquiv.symm {C : Type u_1} [] {S₁ : } {S₂ : } (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 }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
(e.trans e').homotopyHomInvId = (((e'.homotopyHomInvId.compRight e.inv).compLeft e.hom).trans ( e.homotopyHomInvId))
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_inv {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (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} [] {S₁ : } {S₂ : } {S₃ : } (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
(e.trans e').homotopyInvHomId = (((e.homotopyInvHomId.compRight e'.hom).compLeft e'.inv).trans ( e'.homotopyInvHomId))
@[simp]
theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_hom {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
(e.trans e').hom = CategoryTheory.CategoryStruct.comp e.hom e'.hom
def CategoryTheory.ShortComplex.HomotopyEquiv.trans {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (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.
Instances For