Homology of preadditive categories #

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

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

Add (S₁ ⟶ S₂)

Equations

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

source

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

Sub (S₁ ⟶ S₂)

Equations

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

source

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

Neg (S₁ ⟶ S₂)

Equations

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

source

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

AddCommGroup (S₁ ⟶ S₂)

Equations

CategoryTheory.ShortComplex.instAddCommGroupHom = AddCommGroup.mk ⋯

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

Preadditive (ShortComplex C)

Equations

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

source

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

LeftHomologyMapData (-φ) h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

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

LeftHomologyMapData (φ + φ') h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

(γ.add γ').φH = γ.φH + γ'.φH

source

@[simp]

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

(γ.add γ').φK = γ.φK + γ'.φK

source

@[simp]

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

leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

source

@[simp]

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

cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

source

@[simp]

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

leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

source

@[simp]

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

cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

source

@[simp]

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

leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ - leftHomologyMap' φ' h₁ h₂

source

@[simp]

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

cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ - cyclesMap' φ' h₁ h₂

source

@[simp]

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

leftHomologyMap (-φ) = -leftHomologyMap φ

source

@[simp]

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

cyclesMap (-φ) = -cyclesMap φ

source

@[simp]

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

leftHomologyMap (φ + φ') = leftHomologyMap φ + leftHomologyMap φ'

source

@[simp]

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

cyclesMap (φ + φ') = cyclesMap φ + cyclesMap φ'

source

@[simp]

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

leftHomologyMap (φ - φ') = leftHomologyMap φ - leftHomologyMap φ'

source

@[simp]

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

cyclesMap (φ - φ') = cyclesMap φ - cyclesMap φ'

source

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

(leftHomologyFunctor C).Additive

source

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

(cyclesFunctor C).Additive

source

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

RightHomologyMapData (-φ) h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

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

RightHomologyMapData (φ + φ') h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

(γ.add γ').φH = γ.φH + γ'.φH

source

@[simp]

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

(γ.add γ').φQ = γ.φQ + γ'.φQ

source

@[simp]

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

rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

source

@[simp]

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

opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

source

@[simp]

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

rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

source

@[simp]

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

opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

source

@[simp]

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

rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂

source

@[simp]

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

opcyclesMap' (φ - φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ - opcyclesMap' φ' h₁ h₂

source

@[simp]

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

rightHomologyMap (-φ) = -rightHomologyMap φ

source

@[simp]

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

opcyclesMap (-φ) = -opcyclesMap φ

source

@[simp]

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

rightHomologyMap (φ + φ') = rightHomologyMap φ + rightHomologyMap φ'

source

@[simp]

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

opcyclesMap (φ + φ') = opcyclesMap φ + opcyclesMap φ'

source

@[simp]

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

rightHomologyMap (φ - φ') = rightHomologyMap φ - rightHomologyMap φ'

source

@[simp]

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

opcyclesMap (φ - φ') = opcyclesMap φ - opcyclesMap φ'

source

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

(rightHomologyFunctor C).Additive

source

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

(opcyclesFunctor C).Additive

source

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

HomologyMapData (-φ) h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

γ.neg.right = γ.right.neg

source

@[simp]

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

γ.neg.left = γ.left.neg

source

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

HomologyMapData (φ + φ') h₁ h₂

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

Equations

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

Instances For

source

@[simp]

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

(γ.add γ').left = γ.left.add γ'.left

source

@[simp]

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

(γ.add γ').right = γ.right.add γ'.right

source

@[simp]

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

homologyMap' (-φ) h₁ h₂ = -homologyMap' φ h₁ h₂

source

@[simp]

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

homologyMap' (φ + φ') h₁ h₂ = homologyMap' φ h₁ h₂ + homologyMap' φ' h₁ h₂

source

@[simp]

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

homologyMap' (φ - φ') h₁ h₂ = homologyMap' φ h₁ h₂ - homologyMap' φ' h₁ h₂

source

@[simp]

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

homologyMap (-φ) = -homologyMap φ

source

@[simp]

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

homologyMap (φ + φ') = homologyMap φ + homologyMap φ'

source

@[simp]

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

homologyMap (φ - φ') = homologyMap φ - homologyMap φ'

source

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

(homologyFunctor C).Additive

source

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

Type u_2

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

h₀ : S₁.X₁ ⟶ S₂.X₁
a morphism S₁.X₁ ⟶ S₂.X₁
h₀_f : CategoryStruct.comp self.h₀ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
a morphism S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
a morphism S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
a morphism S₁.X₃ ⟶ S₂.X₃
g_h₃ : CategoryStruct.comp S₁.g self.h₃ = 0
comm₁ : φ₁.τ₁ = CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
comm₂ : φ₁.τ₂ = CategoryStruct.comp S₁.g self.h₂ + CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
comm₃ : φ₁.τ₃ = self.h₃ + CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃

Instances For

source

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

x = y

source

@[simp]

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

CategoryStruct.comp self.h₀ (CategoryStruct.comp S₂.f h) = CategoryStruct.comp 0 h

source

@[simp]

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

CategoryStruct.comp S₁.g (CategoryStruct.comp self.h₃ h) = CategoryStruct.comp 0 h

source

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

S₁ ⟶ S₂

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

Equations

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

Instances For

source

@[simp]

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

(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryStruct.comp S₁.f h₁

source

@[simp]

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

(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = CategoryStruct.comp h₁ S₂.f + CategoryStruct.comp S₁.g h₂

source

@[simp]

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

(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryStruct.comp h₂ S₂.g + h₃

source

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

Homotopy φ₁ φ₂

The obvious homotopy between two equal morphisms of short complexes.

Equations

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

Instances For

source

@[simp]

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

(ofEq h).h₃ = 0

source

@[simp]

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

(ofEq h).h₁ = 0

source

@[simp]

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

(ofEq h).h₂ = 0

source

@[simp]

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

(ofEq h).h₀ = 0

source

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

Homotopy φ φ

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

Equations

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

Instances For

source

@[simp]

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

(refl φ).h₂ = 0

source

@[simp]

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

(refl φ).h₁ = 0

source

@[simp]

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

(refl φ).h₃ = 0

source

@[simp]

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

(refl φ).h₀ = 0

source

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

Homotopy φ₂ φ₁

The symmetry of homotopy between morphisms of short complexes.

Equations

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

Instances For

source

@[simp]

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

h.symm.h₂ = -h.h₂

source

@[simp]

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

h.symm.h₀ = -h.h₀

source

@[simp]

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

h.symm.h₃ = -h.h₃

source

@[simp]

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

h.symm.h₁ = -h.h₁

source

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

Homotopy (-φ₁) (-φ₂)

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

Equations

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

Instances For

source

@[simp]

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

h.neg.h₀ = -h.h₀

source

@[simp]

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

h.neg.h₃ = -h.h₃

source

@[simp]

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

h.neg.h₂ = -h.h₂

source

@[simp]

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

h.neg.h₁ = -h.h₁

source

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

Homotopy φ₁ φ₃

The transitivity of homotopy between morphisms of short complexes.

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

source

@[simp]

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

(h₁₂.trans h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁

source

@[simp]

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

(h₁₂.trans h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃

source

@[simp]

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

(h₁₂.trans h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂

source

@[simp]

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

(h₁₂.trans h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀

source

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

Homotopy (φ₁ + φ₃) (φ₂ + φ₄)

Homotopy between morphisms of short complexes is compatible with addition.

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

source

@[simp]

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

(h.add h').h₁ = h.h₁ + h'.h₁

source

@[simp]

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

(h.add h').h₀ = h.h₀ + h'.h₀

source

@[simp]

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

(h.add h').h₂ = h.h₂ + h'.h₂

source

@[simp]

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

(h.add h').h₃ = h.h₃ + h'.h₃

source

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

Homotopy (φ₁ - φ₃) (φ₂ - φ₄)

Homotopy between morphisms of short complexes is compatible with subtraction.

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

source

@[simp]

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

(h.sub h').h₃ = h.h₃ - h'.h₃

source

@[simp]

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

(h.sub h').h₂ = h.h₂ - h'.h₂

source

@[simp]

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

(h.sub h').h₀ = h.h₀ - h'.h₀

source

@[simp]

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

(h.sub h').h₁ = h.h₁ - h'.h₁

source

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

Homotopy (CategoryStruct.comp ψ φ₁) (CategoryStruct.comp ψ φ₂)

Homotopy between morphisms of short complexes is compatible with precomposition.

Equations

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

Instances For

source

@[simp]

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

(h.compLeft ψ).h₃ = CategoryStruct.comp ψ.τ₃ h.h₃

source

@[simp]

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

(h.compLeft ψ).h₂ = CategoryStruct.comp ψ.τ₃ h.h₂

source

@[simp]

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

(h.compLeft ψ).h₁ = CategoryStruct.comp ψ.τ₂ h.h₁

source

@[simp]

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

(h.compLeft ψ).h₀ = CategoryStruct.comp ψ.τ₁ h.h₀

source

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

Homotopy (CategoryStruct.comp φ₁ ψ) (CategoryStruct.comp φ₂ ψ)

Homotopy between morphisms of short complexes is compatible with postcomposition.

Equations

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

Instances For

source

@[simp]

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

(h.compRight ψ).h₂ = CategoryStruct.comp h.h₂ ψ.τ₂

source

@[simp]

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

(h.compRight ψ).h₃ = CategoryStruct.comp h.h₃ ψ.τ₃

source

@[simp]

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

(h.compRight ψ).h₀ = CategoryStruct.comp h.h₀ ψ.τ₁

source

@[simp]

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

(h.compRight ψ).h₁ = CategoryStruct.comp h.h₁ ψ.τ₁

source

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

Homotopy (CategoryStruct.comp φ₁ ψ₁) (CategoryStruct.comp φ₂ ψ₂)

Homotopy between morphisms of short complexes is compatible with composition.

Equations

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

Instances For

source

@[simp]

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

(h.comp h').h₃ = CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryStruct.comp φ₂.τ₃ h'.h₃

source

@[simp]

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

(h.comp h').h₀ = CategoryStruct.comp h.h₀ ψ₁.τ₁ + CategoryStruct.comp φ₂.τ₁ h'.h₀

source

@[simp]

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

(h.comp h').h₁ = CategoryStruct.comp h.h₁ ψ₁.τ₁ + CategoryStruct.comp φ₂.τ₂ h'.h₁

source

@[simp]

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

(h.comp h').h₂ = CategoryStruct.comp h.h₂ ψ₁.τ₂ + CategoryStruct.comp φ₂.τ₃ h'.h₂

source

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

Homotopy (opMap φ₁) (opMap φ₂)

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

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

source

@[simp]

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

h.op.h₀ = h.h₃.op

source

@[simp]

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

h.op.h₃ = h.h₀.op

source

@[simp]

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

h.op.h₂ = h.h₁.op

source

@[simp]

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

h.op.h₁ = h.h₂.op

source

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

Homotopy (unopMap φ₁) (unopMap φ₂)

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

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

source

@[simp]

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

h.unop.h₂ = h.h₁.unop

source

@[simp]

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

h.unop.h₁ = h.h₂.unop

source

@[simp]

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

h.unop.h₃ = h.h₀.unop

source

@[simp]

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

h.unop.h₀ = h.h₃.unop

source

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

Homotopy φ₁ φ₂ ≃ Homotopy (φ₁ - φ₂) 0

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

Equations

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

Instances For

source

@[simp]

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

(equivSubZero φ₁ φ₂) h = (h.sub (refl φ₂)).trans (ofEq ⋯)

source

@[simp]

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

(equivSubZero φ₁ φ₂).symm h = ((ofEq ⋯).trans (h.add (refl φ₂))).trans (ofEq ⋯)

source

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

φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯

source

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

Homotopy (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) 0

A morphism constructed with nullHomotopic is homotopic to zero.

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₃ := ⋯ }

Instances For

source

@[simp]

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

(ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂

source

@[simp]

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

(ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₃ = h₃

source

@[simp]

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

(ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₁ = h₁

source

@[simp]

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

(ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₀ = h₀

source

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

LeftHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

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

Equations

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

Instances For

source

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

RightHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

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

Equations

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

Instances For

source

@[simp]

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

leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

source

@[simp]

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

rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

source

@[simp]

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

homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

source

@[simp]

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

leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

@[simp]

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

rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

@[simp]

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

homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

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

leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

source

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

rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

source

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

homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

source

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

leftHomologyMap φ₁ = leftHomologyMap φ₂

source

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

rightHomologyMap φ₁ = rightHomologyMap φ₂

source

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

homologyMap φ₁ = homologyMap φ₂

source

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

Type u_2

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

hom : S₁ ⟶ S₂
the forward direction of a homotopy equivalence.
inv : S₂ ⟶ S₁
the backwards direction of a homotopy equivalence.
homotopyHomInvId : Homotopy (CategoryStruct.comp self.hom self.inv) (CategoryStruct.id S₁)
the composition of the two directions of a homotopy equivalence is homotopic to the identity of the source
homotopyInvHomId : Homotopy (CategoryStruct.comp self.inv self.hom) (CategoryStruct.id S₂)
the composition of the two directions of a homotopy equivalence is homotopic to the identity of the target