CategoryTheory.ShortComplex.leftHomologyMap'_neg
theorem CategoryTheory.ShortComplex.leftHomologyMap'_neg :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
CategoryTheory.ShortComplex.leftHomologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂
This theorem states that, in the context of category theory, given two objects `S₁` and `S₂` in a short complex `C` of a preadditive category, and a morphism `φ` between them, if we negate this morphism to obtain `-φ`, then the left homology map of `-φ` is just the negation of the left homology map of `φ`. In other words, the left homology map of a negated morphism is the negation of the original left homology map. This property holds for any left homology data `h₁` for `S₁` and `h₂` for `S₂`.
More concisely: Given a short complex in a preadditive category and morphism `φ` between objects `S₁` and `S₂`, the negation of the left homology map of `φ` is equal to the negation of the left homology map of `-φ`.
|
CategoryTheory.ShortComplex.leftHomologyMap'_add
theorem CategoryTheory.ShortComplex.leftHomologyMap'_add :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
CategoryTheory.ShortComplex.leftHomologyMap' (φ + φ') h₁ h₂ =
CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂
This theorem states that, in the context of a given category of type `C`, which is preadditive, for any two short complexes `S₁` and `S₂` and any two morphisms `φ` and `φ'` between them, and given the left homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, the left homology map of the sum of `φ` and `φ'` is equal to the sum of the left homology maps of `φ` and `φ'`. This establishes the additive property of the left homology map in the category theoretical context, specifically for short complexes.
More concisely: In a preadditive category `C`, the left homology map of the sum of two morphisms between short complexes is equal to the sum of their individual left homology maps.
|
CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic
theorem CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
This theorem states that in the context of a category `C`, which is preadditive (i.e., has a structure of an additive category), for any two morphisms `φ₁` and `φ₂` from one short complex `S₁` to another `S₂` such that there exists a homotopy `h` between them, `φ₁` is equal to the sum of `φ₂` and a "null-homotopic" morphism. The null-homotopic morphism is defined using `h.h₀`, `h.h₁`, `h.h₂`, `h.h₃`, etc., which are presumably the data defining the homotopy `h`. In other words, any morphism can be decomposed into another morphism and a null-homotopic one, given that there exists a homotopy between them.
More concisely: In a preadditive category `C`, any two morphisms between complexes with a homotopy between them can be expressed as the sum of one morphism and a null-homotopic morphism using the homotopy data.
|
CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic
theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁)
(h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂)
(h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
CategoryTheory.ShortComplex.leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
The theorem `CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic` states that for any category `C` that is preadditive, and any two short complexes `S₁` and `S₂` in `C` with given left homology data `H₁` and `H₂`, the left homology map of a null-homotopic map between `S₁` and `S₂`, given by morphisms `h₀`, `h₁`, `h₂`, and `h₃`, where the composition of `h₀` with `S₂.f` is 0 and the composition of `S₁.g` with `h₃` is also 0, is equal to 0. In simpler terms, under these conditions, null-homotopic maps do not change the left homology of short complexes.
More concisely: In a preadditive category, the left homology map of a null-homotopic morphism between short complexes is the identity on their respective left homology groups.
|
CategoryTheory.ShortComplex.rightHomologyMap'_add
theorem CategoryTheory.ShortComplex.rightHomologyMap'_add :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
CategoryTheory.ShortComplex.rightHomologyMap' (φ + φ') h₁ h₂ =
CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ +
CategoryTheory.ShortComplex.rightHomologyMap' φ' h₁ h₂
This theorem states that in a given category `C` that is preadditive (i.e., has the structure of an abelian group on its hom-sets), for any two short complexes `S₁` and `S₂` and any two morphisms `φ` and `φ'` from `S₁` to `S₂`, the right homology map of the sum of `φ` and `φ'` is equal to the sum of the right homology maps of `φ` and `φ'`. In simple terms, the right homology map preserves the addition operation on the morphisms. This property is fundamental in the study of homological algebra where we are interested in the algebraic invariants of complex morphisms.
More concisely: In a preadditive category, the right homology map commutes with addition of morphisms.
|