Homology of preadditive categories #

CategoryTheory.ShortComplex.instAddCommGroupHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex = AddCommGroup.mk ⋯

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

CategoryTheory.Preadditive (CategoryTheory.ShortComplex C)

Equations

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

source

@[simp]

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

(CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ).φK = -γ.φK

source

@[simp]

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

(CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ).φH = -γ.φH

source

def CategoryTheory.ShortComplex.LeftHomologyMapData.neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : 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

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

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.LeftHomologyMapData.add γ γ').φK = γ.φK + γ'.φK

source

@[simp]

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

(CategoryTheory.ShortComplex.LeftHomologyMapData.add γ γ').φH = γ.φH + γ'.φH

source

def CategoryTheory.ShortComplex.LeftHomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : 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

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

Instances For

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap (-φ) = -CategoryTheory.ShortComplex.leftHomologyMap φ

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap (-φ) = -CategoryTheory.ShortComplex.cyclesMap φ

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap (φ + φ') = CategoryTheory.ShortComplex.leftHomologyMap φ + CategoryTheory.ShortComplex.leftHomologyMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap (φ + φ') = CategoryTheory.ShortComplex.cyclesMap φ + CategoryTheory.ShortComplex.cyclesMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.leftHomologyMap (φ - φ') = CategoryTheory.ShortComplex.leftHomologyMap φ - CategoryTheory.ShortComplex.leftHomologyMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.cyclesMap (φ - φ') = CategoryTheory.ShortComplex.cyclesMap φ - CategoryTheory.ShortComplex.cyclesMap φ'

source

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.Functor.Additive (CategoryTheory.ShortComplex.leftHomologyFunctor C)

Equations

⋯ = ⋯

source

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.Functor.Additive (CategoryTheory.ShortComplex.cyclesFunctor C)

Equations

⋯ = ⋯

source

@[simp]

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

(CategoryTheory.ShortComplex.RightHomologyMapData.neg γ).φH = -γ.φH

source

@[simp]

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

(CategoryTheory.ShortComplex.RightHomologyMapData.neg γ).φQ = -γ.φQ

source

def CategoryTheory.ShortComplex.RightHomologyMapData.neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : 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

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

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.RightHomologyMapData.add γ γ').φQ = γ.φQ + γ'.φQ

source

@[simp]

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

(CategoryTheory.ShortComplex.RightHomologyMapData.add γ γ').φH = γ.φH + γ'.φH

source

def CategoryTheory.ShortComplex.RightHomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : 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

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

Instances For

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.rightHomologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.opcyclesMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.rightHomologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.opcyclesMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap (-φ) = -CategoryTheory.ShortComplex.rightHomologyMap φ

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap (-φ) = -CategoryTheory.ShortComplex.opcyclesMap φ

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap (φ + φ') = CategoryTheory.ShortComplex.rightHomologyMap φ + CategoryTheory.ShortComplex.rightHomologyMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap (φ + φ') = CategoryTheory.ShortComplex.opcyclesMap φ + CategoryTheory.ShortComplex.opcyclesMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.rightHomologyMap (φ - φ') = CategoryTheory.ShortComplex.rightHomologyMap φ - CategoryTheory.ShortComplex.rightHomologyMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.opcyclesMap (φ - φ') = CategoryTheory.ShortComplex.opcyclesMap φ - CategoryTheory.ShortComplex.opcyclesMap φ'

source

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.Functor.Additive (CategoryTheory.ShortComplex.rightHomologyFunctor C)

Equations

⋯ = ⋯

source

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.Functor.Additive (CategoryTheory.ShortComplex.opcyclesFunctor C)

Equations

⋯ = ⋯

source

@[simp]

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

(CategoryTheory.ShortComplex.HomologyMapData.neg γ).left = CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ.left

source

@[simp]

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

(CategoryTheory.ShortComplex.HomologyMapData.neg γ).right = CategoryTheory.ShortComplex.RightHomologyMapData.neg γ.right

source

def CategoryTheory.ShortComplex.HomologyMapData.neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : 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

CategoryTheory.ShortComplex.HomologyMapData.neg γ = { left := CategoryTheory.ShortComplex.LeftHomologyMapData.neg γ.left, right := CategoryTheory.ShortComplex.RightHomologyMapData.neg γ.right }

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.HomologyMapData.add γ γ').right = CategoryTheory.ShortComplex.RightHomologyMapData.add γ.right γ'.right

source

@[simp]

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

(CategoryTheory.ShortComplex.HomologyMapData.add γ γ').left = CategoryTheory.ShortComplex.LeftHomologyMapData.add γ.left γ'.left

source

def CategoryTheory.ShortComplex.HomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : 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

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

Instances For

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.homologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.homologyMap' φ' h₁ h₂

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap (-φ) = -CategoryTheory.ShortComplex.homologyMap φ

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap (φ + φ') = CategoryTheory.ShortComplex.homologyMap φ + CategoryTheory.ShortComplex.homologyMap φ'

source

@[simp]

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

CategoryTheory.ShortComplex.homologyMap (φ - φ') = CategoryTheory.ShortComplex.homologyMap φ - CategoryTheory.ShortComplex.homologyMap φ'

source

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

CategoryTheory.Functor.Additive (CategoryTheory.ShortComplex.homologyFunctor C)

Equations

⋯ = ⋯

source

theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂), x.h₀ = y.h₀ → x.h₁ = y.h₁ → x.h₂ = y.h₂ → x.h₃ = y.h₃ → x = y

source

theorem CategoryTheory.ShortComplex.Homotopy.ext_iff {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂), x = y ↔ x.h₀ = y.h₀ ∧ x.h₁ = y.h₁ ∧ x.h₂ = y.h₂ ∧ x.h₃ = y.h₃

source

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

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

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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

source

@[simp]

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

source

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (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.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = CategoryTheory.CategoryStruct.comp h₁ S₂.f + CategoryTheory.CategoryStruct.comp S₁.g h₂

source

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (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.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryTheory.CategoryStruct.comp h₂ S₂.g + h₃

source

@[simp]

theorem CategoryTheory.ShortComplex.nullHomotopic_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (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.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryTheory.CategoryStruct.comp S₁.f h₁

source

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

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.ofEq h).h₀ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.ofEq h).h₃ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.ofEq h).h₁ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.ofEq h).h₂ = 0

source

def CategoryTheory.ShortComplex.Homotopy.ofEq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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₃ := ⋯ }

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.refl φ).h₁ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.refl φ).h₀ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.refl φ).h₂ = 0

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.refl φ).h₃ = 0

source

def CategoryTheory.ShortComplex.Homotopy.refl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {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 ⋯

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.symm h).h₀ = -h.h₀

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.symm h).h₂ = -h.h₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.symm h).h₃ = -h.h₃

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.symm h).h₁ = -h.h₁

source

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

CategoryTheory.ShortComplex.Homotopy φ₂ φ₁

The symmetry of homotopy between morphisms of short complexes.

Equations

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

(CategoryTheory.ShortComplex.Homotopy.neg h).h₂ = -h.h₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.neg h).h₃ = -h.h₃

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.neg h).h₀ = -h.h₀

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.neg h).h₁ = -h.h₁

source

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

CategoryTheory.ShortComplex.Homotopy (-φ₁) (-φ₂)

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

Equations

CategoryTheory.ShortComplex.Homotopy.neg h = { 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.trans_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} {φ₃ : S₁ ⟶ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃) :

(CategoryTheory.ShortComplex.Homotopy.trans h₁₂ h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.trans h₁₂ h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.trans h₁₂ h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.trans h₁₂ h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃

source

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

CategoryTheory.ShortComplex.Homotopy φ₁ φ₃

The transitivity of homotopy between morphisms of short complexes.

Equations

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

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.add h h').h₃ = h.h₃ + h'.h₃

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.add h h').h₁ = h.h₁ + h'.h₁

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.add h h').h₂ = h.h₂ + h'.h₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.add h h').h₀ = h.h₀ + h'.h₀

source

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

CategoryTheory.ShortComplex.Homotopy (φ₁ + φ₃) (φ₂ + φ₄)

Homotopy between morphisms of short complexes is compatible with addition.

Equations

CategoryTheory.ShortComplex.Homotopy.add h 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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} {φ₃ : S₁ ⟶ S₂} {φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :

(CategoryTheory.ShortComplex.Homotopy.sub h h').h₃ = h.h₃ - h'.h₃

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.sub h h').h₂ = h.h₂ - h'.h₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.sub h h').h₁ = h.h₁ - h'.h₁

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.sub h h').h₀ = h.h₀ - h'.h₀

source

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

CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₃) (φ₂ - φ₄)

Homotopy between morphisms of short complexes is compatible with substraction.

Equations

CategoryTheory.ShortComplex.Homotopy.sub h 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.compLeft_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₃ ⟶ S₁) :

(CategoryTheory.ShortComplex.Homotopy.compLeft h ψ).h₃ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₃

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def CategoryTheory.ShortComplex.Homotopy.compLeft {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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.

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.compRight h ψ).h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ.τ₁

source

@[simp]

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

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

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.compRight h ψ).h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ.τ₂

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.compRight h ψ).h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ.τ₃

source

def CategoryTheory.ShortComplex.Homotopy.compRight {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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.

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def CategoryTheory.ShortComplex.Homotopy.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {ψ₁ : S₂ ⟶ S₃} {ψ₂ : 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

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

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.op h).h₃ = h.h₀.op

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.op h).h₂ = h.h₁.op

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.op h).h₁ = h.h₂.op

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.op h).h₀ = h.h₃.op

source

def CategoryTheory.ShortComplex.Homotopy.op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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

CategoryTheory.ShortComplex.Homotopy.op h = { 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.unop_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) :

(CategoryTheory.ShortComplex.Homotopy.unop h).h₃ = h.h₀.unop

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.unop h).h₁ = h.h₂.unop

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.unop h).h₂ = h.h₁.unop

source

@[simp]

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

(CategoryTheory.ShortComplex.Homotopy.unop h).h₀ = h.h₃.unop

source

def CategoryTheory.ShortComplex.Homotopy.unop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ : S₁ ⟶ S₂} {φ₂ : 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

CategoryTheory.ShortComplex.Homotopy.unop h = { 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.equivSubZero_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) :

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

source

@[simp]

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

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

source

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

Instances For

source

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

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (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₀

source

@[simp]

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

source

def CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (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 (CategoryTheory.ShortComplex.nullHomotopic S₁ 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

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

source

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (H₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (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' (CategoryTheory.ShortComplex.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

source

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : CategoryTheory.ShortComplex.HomologyData S₁) (H₂ : CategoryTheory.ShortComplex.HomologyData S₂) (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' (CategoryTheory.ShortComplex.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

source

@[simp]

theorem CategoryTheory.ShortComplex.leftHomologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] (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 (CategoryTheory.ShortComplex.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

@[simp]

theorem CategoryTheory.ShortComplex.rightHomologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] (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 (CategoryTheory.ShortComplex.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

@[simp]

theorem CategoryTheory.ShortComplex.homologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] (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 (CategoryTheory.ShortComplex.nullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

source

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

CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₁ h₂

source

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

CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₁ h₂

source

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

CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.homologyMap' φ₂ h₁ h₂

source

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

CategoryTheory.ShortComplex.leftHomologyMap φ₁ = CategoryTheory.ShortComplex.leftHomologyMap φ₂

source

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

CategoryTheory.ShortComplex.rightHomologyMap φ₁ = CategoryTheory.ShortComplex.rightHomologyMap φ₂

source

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

CategoryTheory.ShortComplex.homologyMap φ₁ = CategoryTheory.ShortComplex.homologyMap φ₂

source

theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : CategoryTheory.ShortComplex.HomotopyEquiv S₁ S₂), x = y ↔ x.hom = y.hom ∧ x.inv = y.inv ∧ HEq x.homotopyHomInvId y.homotopyHomInvId ∧ HEq x.homotopyInvHomId y.homotopyInvHomId

source

theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : CategoryTheory.ShortComplex.HomotopyEquiv S₁ S₂), x.hom = y.hom → x.inv = y.inv → HEq x.homotopyHomInvId y.homotopyHomInvId → HEq x.homotopyInvHomId y.homotopyInvHomId → x = y

source

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

Instances For

source

@[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 ⋯

source

@[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

source

@[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

source

@[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 ⋯

source

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

CategoryTheory.ShortComplex.HomotopyEquiv S 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

source

@[simp]

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

(CategoryTheory.ShortComplex.HomotopyEquiv.symm e).hom = e.inv

source

@[simp]

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

(CategoryTheory.ShortComplex.HomotopyEquiv.symm e).homotopyHomInvId = e.homotopyInvHomId

source

@[simp]

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

(CategoryTheory.ShortComplex.HomotopyEquiv.symm e).homotopyInvHomId = e.homotopyHomInvId

source

@[simp]

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

(CategoryTheory.ShortComplex.HomotopyEquiv.symm e).inv = e.hom

source

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

CategoryTheory.ShortComplex.HomotopyEquiv S₂ S₁

The inverse of a homotopy equivalence.

Equations

CategoryTheory.ShortComplex.HomotopyEquiv.symm e = { hom := e.inv, inv := e.hom, homotopyHomInvId := e.homotopyInvHomId, homotopyInvHomId := e.homotopyHomInvId }