CategoryTheory.ShortComplex.LeftHomologyData.wi
theorem CategoryTheory.ShortComplex.LeftHomologyData.wi :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData),
CategoryTheory.CategoryStruct.comp self.i S.g = 0
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.wi` states that, for any category `C` that has zero morphisms, and for any short complex `S` in `C`, the composition of the morphism `i` from the left homology data of `S` and the morphism `g` from `S` equals the zero morphism. In other words, in the context of category theory and homological algebra, this theorem is stating a kernel condition for `i`, which is a fundamental property in the definition of homology.
More concisely: For any short complex S in a category with zero morphisms, the composition of the left homology data inclusion morphism i with any morphism g from S is the zero morphism.
|
CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc
theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {Z : C} (h_1 : S.X₂ ⟶ Z),
CategoryTheory.CategoryStruct.comp h.f' (CategoryTheory.CategoryStruct.comp h.i h_1) =
CategoryTheory.CategoryStruct.comp S.f h_1
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc` states that for any category `C` (of type `u_1`), which has zero morphisms, and for any short complex `S` of `C`, the composition of the morphisms `CategoryTheory.ShortComplex.LeftHomologyData.f' h` and the composition of `h.i` and `h_1` is equal to the composition of `S.f` and `h_1`. Here, `h` is a left homology data of `S` and `h_1` is a morphism from `S.X₂` to `Z` in `C`.
In terms of category theory, it means that in the specified context, the sequence of morphisms `CategoryTheory.ShortComplex.LeftHomologyData.f' h`, `h.i`, and `h_1` gives the same result as the sequence `S.f` and `h_1`. This demonstrates the associativity property of morphism composition in this particular setting.
More concisely: Given a category `C` with zero morphisms and a short complex `S` in `C`, for any left homology data `h` and morphism `h_1` from `S.X₂` to an object `Z`, we have `(h.i ∘ h'_i) = (S.f ∘ h_1)`.
|
CategoryTheory.ShortComplex.leftHomologyMap_comp
theorem CategoryTheory.ShortComplex.leftHomologyMap_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
[inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₁)
(CategoryTheory.ShortComplex.leftHomologyMap φ₂)
This theorem, `CategoryTheory.ShortComplex.leftHomologyMap_comp`, states that for any type `C` which forms a category and has zero morphisms, and any three short complexes `S₁`, `S₂`, and `S₃` in this category that have left homologies, the left homology map of the composition of two morphisms, `φ₁` from `S₁` to `S₂` and `φ₂` from `S₂` to `S₃`, is equal to the composition of the left homology map of `φ₁` and the left homology map of `φ₂`. That is, the left homology map is compatible with the composition of morphisms. This is an essential property in category theory, encapsulating the idea that homology behaves well with respect to morphism composition.
More concisely: Given any three short complexes `S₁`, `S₂`, and `S₃` in a category `C` with zero morphisms, and morphisms `φ₁ : S₁ -> S₂` and `φ₂ : S₂ -> S₃`, the left homology map of their composition `φ₁ ∘ φ₂` is equal to the composition of their left homology maps `L⁰(φ₁) ∘ L⁰(φ₂)`.
|
CategoryTheory.ShortComplex.LeftHomologyData.f'_i
theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.CategoryStruct.comp h.f' h.i = S.f
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.f'_i` states that for any category `C` with zero morphism, and any short complex `S` within this category, if `h` is a left homology data of `S`, then the composition of the morphism `f'` from the left homology data `h` and the morphism `i` from `h` is equal to the morphism `f` from the short complex `S`. In more informal terms, this theorem is about the specific way in which morphisms in the category theory concept of a short complex can be composed.
More concisely: For any short complex `S` in a category with zero morphism and any left homology data `h` of `S`, we have `f' ∘ i = f` in `S`.
|
CategoryTheory.ShortComplex.f'_cyclesMap'
theorem CategoryTheory.ShortComplex.f'_cyclesMap' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
CategoryTheory.CategoryStruct.comp h₁.f' (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) =
CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f'
This theorem, `CategoryTheory.ShortComplex.f'_cyclesMap'`, states that for any category `C` that has zero morphisms and any two short complexes `S₁` and `S₂` in this category, if we have a morphism `φ` from `S₁` to `S₂`, and `h₁` and `h₂` are the left homology data of `S₁` and `S₂` respectively, then the composition of the mapping `f'` of `h₁` and the `cyclesMap'` from `φ`, `h₁`, and `h₂` is equal to the composition of the morphism `τ₁` of `φ` and the mapping `f'` of `h₂`. In other words, `(f' of h₁) composed with (cyclesMap' from φ, h₁, h₂)` is equal to `φ.τ₁ composed with (f' of h₂)`.
More concisely: For any category with zero morphisms, given two short complexes and a morphism between them, the mapping of their left homology data composed with the cycles map from the morphism equals the composition of the morphism with the mapping of the right homology data.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.commi
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commi :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp self.φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂
The theorem `CategoryTheory.ShortComplex.LeftHomologyMapData.commi` states that for any category `C` with zero morphisms, given two short complexes `S₁` and `S₂` in `C`, a morphism `φ` from `S₁` to `S₂`, and left homology data `h₁` for `S₁` and `h₂` for `S₂`, if we have a left homology map data `self` from `φ`, `h₁`, and `h₂`, then the composition of `self.φK` and `h₂.i` is equal to the composition of `h₁.i` and `φ.τ₂`. This equality illustrates a commutation relationship between the morphisms in the category, which is essential in the structural study of categorical diagrams.
More concisely: For any short complexes $S\_1$, $S\_2$ in a category with zero morphisms, a morphism $\varphi$ from $S\_1$ to $S\_2$, and left homology data $h\_1$ for $S\_1$ and $h\_2$ for $S\_2$, if there is a given left homology map data $self$ from $\varphi$, $h\_1$, and $h\_2$, then $self.φK \circ h\_2.i = h\_1.i \circ \varphi.τ\_2$.
|
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.iCycles = h.i
This theorem states that for any category `C` with zero morphisms, and for any short complex `S` in `C` that has a left homology, the composition of the inverse of the cycles isomorphism from the left homology data of `S` and the inclusion from the cycles to the second object in `S` is equal to the inclusion from the cycles to the left homology. In simpler terms, it's a statement about the relationship between the structure of a short complex (a specific type of diagram in a category) and its homology (a way to measure its 'holes').
More concisely: For any short complex in a category with zero morphisms, the inclusion of cycles into the complex is equal to the composition of the cycles isomorphism and its inverse from the left homology data.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.commπ
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commπ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp h₁.π self.φH = CategoryTheory.CategoryStruct.comp self.φK h₂.π
This theorem is about the commutation relation with `π` in the context of category theory and specifically in short complex categories.
The theorem states that for any type `C` that forms a category with zero morphisms, and for any short complexes `S₁` and `S₂` in `C`, any morphism `φ` from `S₁` to `S₂`, and any left homology data `h₁` for `S₁` and `h₂` for `S₂`, the left homology map data `self` for the morphism `φ` and the homology data `h₁` and `h₂` satisfies a specific commutation relation.
This commutation relation says that the composition of `h₁.π` and `self.φH` is the same as the composition of `self.φK` and `h₂.π`. Here, `h₁.π` and `h₂.π` are the `π` components of the left homology data for `S₁` and `S₂` respectively, and `self.φH` and `self.φK` are components of the left homology map data.
In mathematical notation, this can be written as `h₁.π ∘ self.φH = self.φK ∘ h₂.π`.
More concisely: For any short complexes $S\_1$ and $S\_2$ in a category with zero morphisms $C$, and any morphism $\varphi$ from $S\_1$ to $S\_2$ and left homology data $(h\_1, h\_2)$, the maps $h\_1.\pi \circ \varphi^*.H = \varphi^*.K \circ h\_2.\pi$ in the homology groups.
|
CategoryTheory.ShortComplex.leftHomologyMap_id
theorem CategoryTheory.ShortComplex.leftHomologyMap_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.id S) =
CategoryTheory.CategoryStruct.id S.leftHomology
The theorem `CategoryTheory.ShortComplex.leftHomologyMap_id` states that for any category `C` with zero morphisms and any short complex `S` in `C` that has a left homology, the left homology map of the identity morphism on `S` is equal to the identity morphism on the left homology of `S`. In other words, this theorem is asserting that the left homology map respects the identity morphism, a fundamental property expected from maps in category theory.
More concisely: For any short complex S in a category C with zero morphisms, the left homology map of the identity morphism on S equals the identity morphism on the left homology of S.
|
CategoryTheory.ShortComplex.leftHomologyMap'_id
theorem CategoryTheory.ShortComplex.leftHomologyMap'_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h h =
CategoryTheory.CategoryStruct.id h.H
The theorem `CategoryTheory.ShortComplex.leftHomologyMap'_id` states that for any category `C` of a certain type, with `C` having zero morphisms, and for any short complex `S` of `C`, the left homology map applied to the identity morphism of `S` is equivalent to the identity morphism on the left homology data `h` of `S`. This is essentially stating that the left homology map respects the identity morphism in the categorical sense.
More concisely: For any short complex S in a zero-morphism category C, the left homology map applied to the identity morphism of S equals the identity on the left homology data of S.
|
CategoryTheory.ShortComplex.HasLeftHomology.mk'
theorem CategoryTheory.ShortComplex.HasLeftHomology.mk' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.LeftHomologyData → S.HasLeftHomology
This theorem, `CategoryTheory.ShortComplex.HasLeftHomology.mk'`, states that for any type `C` that forms a category with zero morphisms, and any short complex `S` of this category, if `S` has left homology data, then `S` has left homology. In the context of category theory, a complex is a sequence of morphisms such that the composition of any two consecutive morphisms is zero, and the homology of a complex measures the extent to which this sequence fails to be exact. Here, 'left homology' and 'left homology data' refer to the homology and homology data at the left end of the complex, respectively.
More concisely: If `C` is a category with zero morphisms and `S` is a short complex in `C` with left homology data, then `S` has defined left homology.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ = γ.φH
This theorem states that in the context of a category `C` with zero morphisms and given two short complexes `S₁` and `S₂` in `C`, and a morphism `φ` from `S₁` to `S₂`, along with left homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, for any left homology map data `γ` generated by `φ`, `h₁`, and `h₂`, the left homology map generated by `φ`, `h₁`, and `h₂` is equal to the homology map component of `γ`. This equality creates a link between the concept of a left homology map and the homology map component of a left homology map data.
More concisely: Given a category `C` with zero morphisms, two short complexes `S₁` and `S₂`, a morphism `φ` from `S₁` to `S₂`, and left homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, the homology map generated by `φ`, `h₁`, and `h₂` equals the homology map component of the left homology map data `γ` generated by `φ`, `h₁`, and `h₂`.
|
CategoryTheory.ShortComplex.leftHomologyMap'_comp
theorem CategoryTheory.ShortComplex.leftHomologyMap'_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
(h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData),
CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₂ h₃)
The theorem `CategoryTheory.ShortComplex.leftHomologyMap'_comp` states that for any category `C` which has zero morphisms, and for any three short complexes `S₁`, `S₂`, and `S₃` in `C`, with left homology data `h₁`, `h₂`, and `h₃` respectively, the composition of two morphisms `φ₁` and `φ₂` (from `S₁` to `S₂` and `S₂` to `S₃`, respectively) via the `leftHomologyMap'` function is equal to the composition of the `leftHomologyMap'` of `φ₁` and `h₁` to `h₂`, and the `leftHomologyMap'` of `φ₂` and `h₂` to `h₃`. This is essentially a statement about the compatibility of the `leftHomologyMap'` function with the composition of morphisms in the category, following the mathematics principle of associativity.
More concisely: For any short complexes $S\_1, S\_2, S\_3$ in a category $C$ with zero morphisms and left homology data $h\_1, h\_2, h\_3$, the diagram $(h\_1 \circ \varphi\_1) \circ \varphi\_2 = \varphi\_1 \circ h\_2 \circ \varphi\_2$ commutes, where $\varphi\_1 : S\_1 \to S\_2$ and $\varphi\_2 : S\_2 \to S\_3$ are morphisms and $h\_i = \mathrm{leftHomologyMap}'(S\_i)$ for $i = 1, 2, 3$.
|
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_f'
theorem CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_f' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).f' = 0
This theorem states that in the context of a category `C`, which has zero morphisms, for any short complex `S` in `C` where both the `f` and `g` morphisms are zeros, the `f'` morphism in the left homology data constructed from `S` using `ofZeros` is also a zero morphism.
More concisely: In a zero-object category `C`, if a short complex `S` has zero morphisms `f` and `g`, then the left homology `f'` constructed from `S` using `ofZeros` is also a zero morphism.
|
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
theorem CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.i = S.iCycles
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i` in Category Theory asserts that for any type `C` which forms a category and has zero-morphisms, and for any `S` of type `ShortComplex C` with a left homology, the composition of the morphism `cyclesIso h.hom` with `h.i` equals the inclusion of `S.cycles` to `S.X₂`. In simpler terms, this theorem establishes a particular relationship between the specific morphisms in the short complex of a category with left homology.
More concisely: For any ShortComplex C with left homology, the morphism `cyclesIso.hom` composed with `i` is equal to the inclusion of cycles into the second component of the complex.
|
CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc
theorem CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) {Z : C} (h : S.X₃ ⟶ Z),
CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp S.g h) =
CategoryTheory.CategoryStruct.comp 0 h
This theorem belongs to the category theory and it is about the composition of morphisms in a category. Specifically, it states that for any category `C` with zero morphisms, given a short complex `S` in `C` and a `LeftHomologyData` instance for `S`, the composition of the morphism `i` from the `LeftHomologyData` with the composition of the morphism `g` from the short complex `S` and any morphism `h` from `S.X₃` to any object `Z` in `C` is equal to the composition of the zero morphism with `h`. This is an important property that characterizes how morphisms interact with the zero morphism in category theory.
More concisely: For any short exact sequence S in a category C with zero morphisms and a given LeftHomologyData instance, the composition of i from the LeftHomologyData, g from S, and any morphism h from S.X₃ to Z equals the composition of the zero morphism with h.
|
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom
theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp S.leftHomologyπ h.leftHomologyIso.hom =
CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.π
This theorem states that for any category `C` with zero morphisms, given a short complex `S` of this category with left homology, and any left homology data `h` of `S`, the composition of the morphism `leftHomologyπ` of `S` and the homomorphism of the left homology isomorphism of `h` is equal to the composition of the homomorphism of the cycles isomorphism of `h` and the morphism `π` of `h`. This essentially provides a specific equality relation for the compositions of certain morphisms and homomorphisms in the context of category theory.
More concisely: For any short complex `S` in a category with zero morphisms, the composition of `leftHomologyπ` of `S` and the homomorphism of the left homology isomorphism of `h` equals the composition of the homomorphism of the cycles isomorphism of `h` and `π` of `h`.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.commf'
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commf' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp h₁.f' self.φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f'
The theorem `CategoryTheory.ShortComplex.LeftHomologyMapData.commf'` states that for any category `C` with zero morphisms, and for any two short complexes `S₁` and `S₂` in `C`, given a morphism `φ` from `S₁` to `S₂`, and given left homology data `h₁` for `S₁` and `h₂` for `S₂`, the composition of the morphism `h₁.f'` with the morphism `self.φK` (which is a part of the homology map data for the morphism `φ` from `S₁` to `S₂`) is equal to the composition of the morphism `φ.τ₁` with the morphism `h₂.f'`. This expresses a commutativity condition in the context of short complexes in a category.
More concisely: For any short complexes $S\_1, S\_2$ in a category with zero morphisms and given morphism $\varphi$ from $S\_1$ to $S\_2$ with corresponding left homology data $h\_1$ and $h\_2$, we have $h\_1.f'\circ self.\varphi K = \varphi.τ\_1 \circ h\_2.f'$.
|
CategoryTheory.ShortComplex.leftHomologyπ_naturality'
theorem CategoryTheory.ShortComplex.leftHomologyπ_naturality' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.π
The theorem `CategoryTheory.ShortComplex.leftHomologyπ_naturality'` states that for any Category `C` with zero morphisms, and any two short complexes `S₁` and `S₂` in `C`, given a morphism `φ : S₁ ⟶ S₂`, and left homology data `h₁` for `S₁` and `h₂` for `S₂`, the composition of `h₁.π` (the projection map of `h₁`) and `CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂` is equal to the composition of `CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂` and `h₂.π` (the projection map of `h₂`). In simple terms, this theorem shows the naturality of the left homology projection in the category of short complexes, under the setting of Category Theory.
More concisely: For any short complexes $S\_1$ and $S\_2$ in a zero-morphism category $C$, and a morphism $\varphi : S\_1 \to S\_2$ with associated left homology data $h\_1$ for $S\_1$ and $h\_2$ for $S\_2$, the composition of $h\_1.\pi$ and $CategoryTheory.ShortComplex.leftHomologyMap' \, \varphi h\_1 h\_2$ equals the composition of $CategoryTheory.ShortComplex.cyclesMap' \, \varphi h\_1 h\_2$ and $h\_2.\pi$.
|
CategoryTheory.ShortComplex.cyclesMap_comp
theorem CategoryTheory.ShortComplex.cyclesMap_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
[inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₁)
(CategoryTheory.ShortComplex.cyclesMap φ₂)
This theorem is about the composition of morphisms in the context of a mathematical structure known as a short complex in category theory. It states that for any type `C` that forms a category and has zero morphisms, and for any three short complexes `S₁`, `S₂`, and `S₃` each with left homology, the `cyclesMap` (a morphism mapping to cycles in the homology) of the composition of two morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃` is equal to the composition of the `cyclesMap` of `φ₁` and the `cyclesMap` of `φ₂`. This means that the operation of taking cycles commutes with the operation of composing morphisms.
More concisely: For any three short complexes `S₁`, `S₂`, and `S₃` in a category `C` with zero morphisms, the cycles map of their composition `S₁ ⟶ S₂ ⟶ S₃` equals the composition of the cycles maps `S₁ ⟶ S₂` and `S₂ ⟶ S₃`.
|
CategoryTheory.ShortComplex.cyclesMap_id
theorem CategoryTheory.ShortComplex.cyclesMap_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.id S) =
CategoryTheory.CategoryStruct.id S.cycles
This theorem states that in the context of category theory, for any given category `C` that has zero morphisms, and any short complex `S` in `C` that has left homology data, the map of the cycles of the short complex `S` under the identity morphism is equal to the identity morphism on the cycles of `S`. In simpler terms, applying the identity operation to the short complex and then mapping to its cycles is the same as directly applying the identity operation to the cycles of the short complex.
More concisely: In any category with zero morphisms, the identity morphism on the cycles of a short complex is equal to the cycles of the identity morphism on the complex.
|
CategoryTheory.ShortComplex.cyclesMap'_comp
theorem CategoryTheory.ShortComplex.cyclesMap'_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
(h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData),
CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.cyclesMap' φ₂ h₂ h₃)
This theorem is about the composition of morphisms in the context of a category theory. Specifically, it states that for any category `C` that has zero morphisms, and for any three short complexes `S₁`, `S₂`, and `S₃` in this category, if `φ₁` is a morphism from `S₁` to `S₂`, `φ₂` is a morphism from `S₂` to `S₃`, and `h₁`, `h₂`, `h₃` are left homology data for `S₁`, `S₂`, `S₃` respectively, then the cycle map of the composition of `φ₁` and `φ₂` from `h₁` to `h₃` is equal to the composition of the cycle map of `φ₁` from `h₁` to `h₂` and the cycle map of `φ₂` from `h₂` to `h₃`. This theorem is a fundamental property of morphisms in category theory which ensures the associative property of composition of morphisms.
More concisely: In any category with zero morphisms, the cycle map of the composition of two morphisms is equal to the composition of their cycle maps.
|
CategoryTheory.ShortComplex.cyclesMap_i
theorem CategoryTheory.ShortComplex.cyclesMap_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂),
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.iCycles =
CategoryTheory.CategoryStruct.comp S₁.iCycles φ.τ₂
This theorem in the category theory states that for any category `C` that has zero morphisms, and any two short complexes `S₁` and `S₂` in `C` that both have left homology, the composition of the cycles map of a morphism `φ` from `S₁` to `S₂` and the inclusion from the cycles of `S₂` to `S₂.X₂` is equal to the composition of the inclusion from the cycles of `S₁` to `S₁.X₂` and the differential `τ₂` of `φ`. In other words, the diagram commutes in the category `C` for the given morphism `φ`, which means that moving along any path in the diagram from the cycles of `S₁` to `S₂.X₂` results in the same morphism.
More concisely: For any category with zero morphisms `C` and short complexes `S₁` and `S₂` having left homology, the composition of the cycles inclusion of `S₁` into `S₁.X₂` and the differential of a morphism `φ` from `S₁` to `S₂`, and the cycles inclusion of `S₂` into `S₂.X₂`, is equal to the cycles inclusion of `S₁` into `S₂.X₂` and the composition of the cycles map of `φ` with the differential of `S₂.X₂`.
|
CategoryTheory.ShortComplex.cyclesMap'_id
theorem CategoryTheory.ShortComplex.cyclesMap'_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.id S) h h =
CategoryTheory.CategoryStruct.id h.K
This theorem pertains to the category theory in mathematics. Specifically, it deals with a "short complex", a specific structure in the category, denoted by 'C'. This theorem states that for any type 'C' that forms a category with zero morphisms, and for any short complex 'S' in 'C', if 'h' is the left homology data of 'S', then applying the 'cyclesMap' function to the identity morphism of 'S' and 'h' twice results in the identity morphism of 'h.K'. In simpler terms, it means that within the constraints of this category and short complex, a specific mapping operation involving the identity morphism doesn't change the underlying object 'h.K'.
More concisely: For any short complex 'S' in a category 'C' with zero morphisms, the composition of the cycles map applied to the identity morphism of 'S' and the cycles map of its homology data 'h' equals the identity morphism on 'h.K'.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ = γ.φK
This theorem states that for any category `C` with zero morphisms, given two short complexes `S₁` and `S₂` in `C`, a morphism `φ` from `S₁` to `S₂`, and left homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, for any left homology map data `γ` defined by `φ`, `h₁`, and `h₂`, the `cyclesMap'` of `φ`, `h₁`, and `h₂` in the short complex category is equal to the `φK` component of `γ`.
In simpler terms, it is about a particular association between the morphism of two short complexes and the left homology map data, where the cycles map of the morphism and the left homology data is the same as a certain component of the left homology map data.
More concisely: For any category with zero morphisms `C`, given short complexes `S₁` and `S₂`, a morphism `φ` from `S₁` to `S₂`, and left homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, the cycles map of `φ` with respect to `h₁` and `h₂` is equal to the `φK` component of the induced left homology map `γ` between `h₁` and `h₂`.
|
CategoryTheory.ShortComplex.cyclesMap'_i
theorem CategoryTheory.ShortComplex.cyclesMap'_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.i =
CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂
This theorem states that for any category 'C' with zero morphisms and any two short complexes 'S₁' and 'S₂' in 'C', as well as a morphism 'φ' from 'S₁' to 'S₂', and the left homology data 'h₁' and 'h₂' of 'S₁' and 'S₂' respectively, the composition of the 'cyclesMap' of 'φ', 'h₁', and 'h₂' with 'h₂.i' is equal to the composition of 'h₁.i' and 'φ.τ₂'. Essentially, this theorem expresses a certain commutativity property in the category of short complexes.
More concisely: For any category 'C' with zero morphisms, given short complexes 'S₁' and 'S₂', morphism 'φ' from 'S₁' to 'S₂', and their respective left homology data 'h₁' and 'h₂', the commutativity of their cycles maps holds: 'h₁.i ∘ φ.τ₂ = φ.τ₁ ∘ h₂.i'.
|
CategoryTheory.ShortComplex.LeftHomologyData.f'_π
theorem CategoryTheory.ShortComplex.LeftHomologyData.f'_π :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.CategoryStruct.comp h.f' h.π = 0
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.f'_π` states that for any Type `C` that is a category `CategoryTheory.Category` and has zero morphisms `CategoryTheory.Limits.HasZeroMorphisms`, and any `CategoryTheory.ShortComplex` `S`, for any left homology data `h` of `S`, the composition of the morphism `CategoryTheory.ShortComplex.LeftHomologyData.f' h` with the morphism `h.π` is a zero morphism. In other words, it refers to a condition in the category theory where the composition of two specific morphisms results in a zero morphism.
More concisely: For any category `C` with zero morphisms and any left homology data `h` of a short complex `S` in `C`, the composition of `CategoryTheory.ShortComplex.LeftHomologyData.f' h` and `h.π` is the zero morphism.
|
CategoryTheory.ShortComplex.iCycles_g
theorem CategoryTheory.ShortComplex.iCycles_g :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp S.iCycles S.g = 0
The theorem `CategoryTheory.ShortComplex.iCycles_g` states that for any category `C` with zero morphisms, and any short complex `S` in `C` that has left homology, the composition of the morphism representing the inclusion of `S.cycles` into `S.X₂` with the morphism `S.g` is a zero morphism. In other words, if you first include `S.cycles` into `S.X₂` and then apply `S.g`, you end up with the same result as if you had done nothing. This is typically a property you would expect in the context of homological algebra, where complexes and cycles play a crucial role.
More concisely: For any short complex S in a category with zero morphisms having left homology, the composition of the inclusion of S.cycles into S.X₂ with S.g is the zero morphism.
|
CategoryTheory.ShortComplex.LeftHomologyData.wπ
theorem CategoryTheory.ShortComplex.LeftHomologyData.wπ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData),
CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) self.π = 0
The theorem `CategoryTheory.ShortComplex.LeftHomologyData.wπ` states that for any category `C` with zero morphisms, given a short complex `S` in `C` and its left homology data `self`, the composition of `self.hi.lift` with `self.π`, where `self.hi.lift` is built using a kernel fork over `S.f`, is equal to the zero morphism. This is sometimes known as the cokernel condition for `π`.
More concisely: For any short complex `S` in a category `C` with zero morphisms, the composite of the morphism `self.π` with the lifted inclusion `self.hi.lift` into the quotient object of the kernel pair of `S.f` is the zero morphism.
|
CategoryTheory.ShortComplex.liftCycles_i
theorem CategoryTheory.ShortComplex.liftCycles_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
[inst_2 : S.HasLeftHomology], CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) S.iCycles = k
This theorem `CategoryTheory.ShortComplex.liftCycles_i` states that in the context of a category `C` with zero morphisms and a short complex `S` within `C` that has left homology, for any object `A` of `C` and a morphism `k` from `A` to `S.X₂` such that the composition of `k` and the morphism `S.g` equals to the zero morphism, the composition of the lift of cycles of `S` with `k` and the inclusion function from `S.cycles` to `S.X₂` is equal to `k`.
In more mathematical terms, if we have `k : A ⟶ S.X₂` such that `k ≫ S.g = 0`, then `(liftCycles S k hk) ≫ iCycles S = k`, where `liftCycles` and `iCycles` are specific morphisms related to the structure of the short complex `S`.
More concisely: Given a short complex `S` in a category `C` with zero morphisms and left homology, for any morphism `k : A ⟶ S.X₂` with `k ≫ S.g = 0`, the composition of the lift of cycles of `S` with `k` and the inclusion of cycles is equal to `k`.
|
CategoryTheory.ShortComplex.toCycles_i
theorem CategoryTheory.ShortComplex.toCycles_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
CategoryTheory.CategoryStruct.comp S.toCycles S.iCycles = S.f
The theorem `CategoryTheory.ShortComplex.toCycles_i` states that, for any category 'C' with zero morphisms and a short complex 'S' with left homology, the composition of the morphism 'toCycles' of 'S' and the inclusion of the cycles of 'S' into 'S.X₂', denoted by 'iCycles', is equal to the morphism 'f' of the short complex 'S'. In other words, in the category-theoretic context, it asserts that certain morphisms in a short complex form a commutative diagram.
More concisely: For any short complex in a category with zero morphisms and left homology, the morphism 'toCycles' composing with the inclusion of cycles equals the morphism 'f' in the complex.
|
CategoryTheory.ShortComplex.LeftHomologyData.liftK_i
theorem CategoryTheory.ShortComplex.LeftHomologyData.liftK_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0), CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.i = k
This theorem states that for any category `C` with zero morphisms, any short complex `S` in `C`, any left homology data `h` of `S`, and any morphism `k` from an object `A` to the third object `S.X₂` in `S` such that the composition of `k` and `S.g` (a morphism in `S`) is a zero morphism, the composition of the morphism obtained by lifting `k` with respect to `h` and the morphism `h.i` is equal to `k`. Essentially, this is a property of the lifting operation in the context of left homology data in a short complex in a category.
More concisely: For any short complex in a category with zero morphisms and any left homology data, the morphism obtained by lifting a given morphism through the homology data equals the morphism itself when composed with the appropriate chain map and homology inclusion.
|