CategoryTheory.ShortComplex.RightHomologyData.wp
theorem CategoryTheory.ShortComplex.RightHomologyData.wp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData),
CategoryTheory.CategoryStruct.comp S.f self.p = 0
The theorem `CategoryTheory.ShortComplex.RightHomologyData.wp` states that for any category `C` of some type `u_1` with zero morphisms, and any short complex `S` within that category, the composition of `S.f` and `self.p` in the right homology data of the short complex is equal to zero. In other words, `S.f` followed by `self.p` is a zero morphism. This is known as the cokernel condition for `p` in the context of category theory.
More concisely: For any short complex `S` in a category `C` with zero morphisms, the composition of `S.f` and `self.p` in the right homology data is the zero morphism.
|
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g'
theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g' :
∀ {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.RightHomologyData.ofZeros S hf hg).g' = 0
This theorem states that given a category `C` along with the assumption that it has zero morphisms, for any `ShortComplex` `S` in `C`, if the morphisms `f` and `g` in `S` are both zero, then the induced morphism `g'` is also zero. This `g'` is originally defined using the morphism `g` from `S` and the fact that `Q` is a cokernel of `f` in `S`. Thus, intuitively, the theorem asserts that zero morphisms in the short complex propagate to this constructed morphism `g'`.
More concisely: Given a short complex `S` in a category `C` with zero morphisms, if `f` and `g` in `S` are zero, then the induced morphism `g'` from `g` and the cokernel `Q` of `f` is zero.
|
CategoryTheory.ShortComplex.opcyclesMap'_comp
theorem CategoryTheory.ShortComplex.opcyclesMap'_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₁.RightHomologyData)
(h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData),
CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.opcyclesMap' φ₂ h₂ h₃)
The theorem `CategoryTheory.ShortComplex.opcyclesMap'_comp` states that for any category `C` that has zero morphisms, given three short complexes `S₁`, `S₂`, and `S₃` in `C`, and morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, the composition of the op-cycles maps induced by `φ₁` and `φ₂` is equal to the op-cycles map induced by the composition of `φ₁` and `φ₂`. Here, the op-cycles map is a specific map associated to a morphism in the category of short complexes, and the right homology data `h₁`, `h₂`, and `h₃` are associated to the short complexes `S₁`, `S₂`, and `S₃` respectively. The theorem thus establishes an important property about the interaction between morphism composition and the op-cycles map in the context of short complexes.
More concisely: For any category `C` with zero morphisms, given three short complexes `S₁`, `S₂`, `S₃` and morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, the op-cycles maps induced by their composition are equal to the composition of the op-cycles maps induced by each morphism.
|
CategoryTheory.ShortComplex.p_opcyclesMap'
theorem CategoryTheory.ShortComplex.p_opcyclesMap' :
∀ {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) =
CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p
The theorem `CategoryTheory.ShortComplex.p_opcyclesMap'` states that for any type `C` with structure of a category and zero morphisms, and any two short complexes `S₁` and `S₂` in `C`, given a morphism `φ` from `S₁` to `S₂` and right homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, the composition of `h₁.p` and `CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂` is equal to the composition of `φ.τ₂` and `h₂.p`. This theorem describes a property of the mapping between the cycles of two short complexes in the context of category theory.
More concisely: Given short complexes $S\_1$ and $S\_2$ in a category $C$ with zero morphisms, a morphism $\varphi \colon S\_1 \to S\_2$, and right homology data $h\_1$ and $h\_2$ for $S\_1$ and $S\_2$ respectively, the diagram commutes: $h\_1.p \circ CategoryTheory.ShortComplex.opcyclesMap' (\varphi) h\_1 h\_2 = \varphi.τ\_2 \circ h\_2.p$.
|
CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary
theorem CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary :
∀ {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 : S.X₂ ⟶ A) [inst_2 : S.HasRightHomology] (x : S.X₃ ⟶ A)
(hx : k = CategoryTheory.CategoryStruct.comp S.g x),
CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.descOpcycles k ⋯) = 0
This theorem is a statement in a category theory context. It declares that for any type `C` within a category that has zero morphisms, and given a short complex `S` of type `C`, if there exists a morphism `k` from `S.X₂` to another object `A`, and another morphism `x` from `S.X₃` to `A` such that `k` is the composition of `S.g` and `x`, then the composition of `CategoryTheory.ShortComplex.rightHomologyι S` and `CategoryTheory.ShortComplex.descOpcycles S k` is a zero morphism.
In other words, this theorem is about the composition of two specific morphisms in a category, and states that under certain conditions, the composition of these two morphisms is the zero morphism. This theorem is a key result in the theory of short complexes in category theory, which is a fundamental construct in algebraic topology and homological algebra.
More concisely: Given a short complex in a category with zero morphisms, if there exist morphisms `k` and `x` such that `k = g × x` and `k` factors through `x`, then the composition of the right homology invariant and the descendant cycle map with respect to `k` is the zero morphism.
|
CategoryTheory.ShortComplex.RightHomologyData.p_g'
theorem CategoryTheory.ShortComplex.RightHomologyData.p_g' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData),
CategoryTheory.CategoryStruct.comp h.p h.g' = S.g
The theorem `CategoryTheory.ShortComplex.RightHomologyData.p_g'` states that for any category `C`, which has zero morphisms, and for any short complex `S` in this category, the morphism `g'` induced by `S.g` and the fact that `h.Q` is a cokernel of `S.f`, when composed with `h.p`, is equal to `S.g`. This means that if we follow the morphism `h.p` from the object `h.Q`, and then `g'` from there to the object `S.X₃`, we end up at the same place as if we took `S.g` directly from `S.X₂` to `S.X₃`. This property is a crucial one for short complexes in category theory.
More concisely: Given a short complex `S` in a zero-morphism category `C`, the composite of `h.p` and `g'` is equal to `S.g`, where `h.Q` is a cokernel of `S.f`.
|
CategoryTheory.ShortComplex.rightHomologyMap'_id
theorem CategoryTheory.ShortComplex.rightHomologyMap'_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.RightHomologyData),
CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h h =
CategoryTheory.CategoryStruct.id h.H
The theorem `CategoryTheory.ShortComplex.rightHomologyMap'_id` states that for any category 'C' that has zero morphisms and a short complex 'S', the right homology map, when applied to the identity morphism of 'S' and any right homology data 'h' of 'S', returns the identity morphism of 'h'. In other words, the right homology map preserves the identity morphism in the context of short complexes in the category theory.
More concisely: For any short complex S in a category C with zero morphisms, the right homology map of the identity morphism of S with respect to any right homology data is the identity morphism of the right homology data.
|
CategoryTheory.ShortComplex.p_descOpcycles
theorem CategoryTheory.ShortComplex.p_descOpcycles :
∀ {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 : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
[inst_2 : S.HasRightHomology], CategoryTheory.CategoryStruct.comp S.pOpcycles (S.descOpcycles k hk) = k
The theorem `CategoryTheory.ShortComplex.p_descOpcycles` states that for any category having zero morphisms, given a short complex `S` in the category, and a morphism `k` from `S.X₂` to a category object `A` such that the composition of `S.f` and `k` is the zero morphism, if `S` has right homology then the composition of `CategoryTheory.ShortComplex.pOpcycles S` and `CategoryTheory.ShortComplex.descOpcycles S k hk` equals `k`.
In more detail, this theorem is about the interaction of certain morphisms in a short complex, a structure in category theory. If `S` is a short complex in a category `C`, `k` is a morphism from the second object of the complex `S.X₂` to an object `A` in `C`, and the composition of `S.f` and `k` is the zero morphism (represented in Lean as `CategoryTheory.CategoryStruct.comp S.f k = 0`), then when `S` has a property called right homology, the composition of the morphism from `S.X₂` to the 'opposite cycles' of `S` (`CategoryTheory.ShortComplex.pOpcycles S`) and the morphism from the 'opposite cycles' of `S` to `A` that is characterized by `k` (`CategoryTheory.ShortComplex.descOpcycles S k hk`) is `k` itself. The theorem thus describes a 'reversibility' property for this particular sequence of morphisms and operations in a short complex with right homology.
More concisely: Given a short complex in a category with zero morphisms and right homology, if a morphism from the second object to an object in the category making the composition with the complex's forward morphism zero is equal to the descent morphism of cycles through that morphism, then the morphisms are equal.
|
CategoryTheory.ShortComplex.rightHomologyMap_id
theorem CategoryTheory.ShortComplex.rightHomologyMap_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.HasRightHomology],
CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.id S) =
CategoryTheory.CategoryStruct.id S.rightHomology
This theorem, `CategoryTheory.ShortComplex.rightHomologyMap_id`, states that for any category `C` that has zero morphisms, and any short complex `S` in this category that has a right homology, the right homology map applied to the identity morphism of `S` is equal to the identity morphism of the right homology of `S`. In other words, the right homology map preserves identity morphisms in the category of short complexes.
More concisely: For any short complex `S` in a zero-morphism category `C` with right homology, the right homology map of the identity morphism of `S` equals the identity morphism of `S`'s right homology.
|
CategoryTheory.ShortComplex.RightHomologyMapData.commp
theorem CategoryTheory.ShortComplex.RightHomologyMapData.commp :
∀ {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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp h₁.p self.φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p
This theorem, named `CategoryTheory.ShortComplex.RightHomologyMapData.commp`, states that for any category `C` of type `u_1` (equipped with zero morphisms), any two short complexes `S₁` and `S₂` in `C`, any morphism `φ` from `S₁` to `S₂`, and any right homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, given a right homology map data `self` for `φ`, `h₁`, and `h₂`, the composition of `h₁.p` and `self.φQ` is equal to the composition of `φ.τ₂` and `h₂.p`. In other words, the diagram involving morphisms from short complex and right homology data commutes.
More concisely: Given two short complexes `S₁` and `S₂`, a morphism `φ` between them, and right homology data `h₁` for `S₁` and `h₂` for `S₂`, if there is a right homology map data `self` for `φ`, `h₁`, and `h₂`, then the composition of `h₁.p` and `self.φQ` equals the composition of `φ.τ₂` and `h₂.p`.
|
CategoryTheory.ShortComplex.opcyclesMap'_g'
theorem CategoryTheory.ShortComplex.opcyclesMap'_g' :
∀ {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₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h₂.g' =
CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃
The theorem `CategoryTheory.ShortComplex.opcyclesMap'_g'` in Lean 4 is a statement about the composition of morphisms in a category theoretical context, specifically dealing with the concept of short complexes. In more natural language, it states that for any category `C` (with zero morphisms), and for any two short complexes `S₁` and `S₂` in `C` with the morphism `φ : S₁ ⟶ S₂`, the composition of `opcyclesMap'` with `g'` for `h₂` (Right Homology Data of `S₂`) is equal to the composition of `g'` for `h₁` (Right Homology Data of `S₁`) with `φ.τ₃`. In other words, it is asserting that a certain diagram in the category of short complexes commutes, which is a fundamental concept in category theory. The morphisms `g'` are determined by the cokernels in the short complexes, and `φ.τ₃` is a part of the morphism from `S₁` to `S₂`.
More concisely: For any category `C` with zero morphisms, given short complexes `S₁` and `S₂` and morphism `φ : S₁ ⟶ S₂`, the diagram commutes: `opcyclesMap' (h₂) (g₂) ∘ g₁' (h₁) = g₂' (h₁) ∘ φ.τ₃`, where `g₁'` and `g₂'` are determined by the cokernels in `S₁` and `S₂`, respectively.
|
CategoryTheory.ShortComplex.HasRightHomology.mk'
theorem CategoryTheory.ShortComplex.HasRightHomology.mk' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.RightHomologyData → S.HasRightHomology
This theorem states that for any type 'C' which is a category with zero morphisms, and any short complex 'S' within this category, if 'S' has right homology data, then 'S' also has right homology. In other words, the right homology data of a short complex in a category with zero morphisms is sufficient to establish the existence of right homology for that short complex.
More concisely: If 'C' is a category with zero morphisms and 'S' is a short complex in 'C' with right homology data, then 'S' has defined right homologies.
|
CategoryTheory.ShortComplex.opcyclesMap_id
theorem CategoryTheory.ShortComplex.opcyclesMap_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.HasRightHomology],
CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.id S) =
CategoryTheory.CategoryStruct.id S.opcycles
This theorem states that, for any given category `C` with zero morphisms, and any short complex `S` with right homology, the operation `opcyclesMap`, when applied to the identity morphism of `S`, gives the same result as applying the identity morphism to the operation `opcycles` of `S`.
In other words, the `opcyclesMap` operation preserves the identity morphism in the category of short complexes, which is a crucial property needed for the definition of a category. This property ensures that the structures and relations between objects in the category are maintained under the `opcyclesMap` operation.
More concisely: For any short complex `S` in a category with zero morphisms, `opcyclesMap` applied to the identity morphism of `S` equals the identity morphism on its homology `opcycles`.
|
CategoryTheory.ShortComplex.p_opcyclesMap
theorem CategoryTheory.ShortComplex.p_opcyclesMap :
∀ {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₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
(φ : S₁ ⟶ S₂),
CategoryTheory.CategoryStruct.comp S₁.pOpcycles (CategoryTheory.ShortComplex.opcyclesMap φ) =
CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.pOpcycles
This theorem, `CategoryTheory.ShortComplex.p_opcyclesMap`, states that for any category `C` with zero morphisms, and any two short complexes `S₁` and `S₂` in `C` that have right homology, given a morphism `φ` from `S₁` to `S₂`, the composition of the projection from `S₁` to its associated opcycles with the opcycles map of `φ` is equal to the composition of `φ`'s τ₂ component with the projection from `S₂` to its associated opcycles. In other words, this theorem articulates a specific commutative property of these operations in the context of Category Theory and the structure of short complexes.
More concisely: For any short complexes `S₁` and `S₂` in a category with zero morphisms and right homology, and a morphism `φ` between them, the diagram commutes:
```
opcycles(S₁) ↓───────┐
| ⊣ p₂(S₁) opcycles(S₂) ↓───────┐
| |
| φ |
| |
↓─────────────────────────────────────────↓
H_(n+1)(S₁) ──┐----┐ H_(n+1)(S₂)
| P₂(S₁)|
└─────┘
```
where `opcycles` is the opcycles map, `p₂` is the projection to the second component, and `H_n` represents the n-th homology.
|
CategoryTheory.ShortComplex.RightHomologyData.ι_g'
theorem CategoryTheory.ShortComplex.RightHomologyData.ι_g' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), CategoryTheory.CategoryStruct.comp h.ι h.g' = 0
This theorem states that in any category `C` endowed with zero morphisms, given any short complex `S` of `C` and any right homology data `h` pertaining to `S`, the composition of `h.ι` and `g'` related to `h` is zero. Here `h.ι` is a morphism from `h.I` to `h.Q` and `CategoryTheory.ShortComplex.RightHomologyData.g' h` is the morphism from `h.Q` to `S.X₃` induced by `S.g` and the fact that `h.Q` is a cokernel of `S.f`. In essence, it's stating a property of the commutativity of the diagram involving those objects and morphisms in the category `C`.
More concisely: In any abelian category with zero morphisms, the composition of the right homology morphism with the connecting morphism induced by a short exact sequence is zero.
|
CategoryTheory.ShortComplex.RightHomologyData.wι
theorem CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData),
CategoryTheory.CategoryStruct.comp self.ι (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0
This theorem, `CategoryTheory.ShortComplex.RightHomologyData.wι`, states that for any category `C` (of type `u_1`) with morphisms (of type `u_2`) and equipped with zero-morphisms, given any `ShortComplex` `S` within this category and any 'RightHomologyData' `self` of `S`, the composition of the morphism `self.ι` and the cokernel cofork of `S.g`, described by `self.hp.desc`, equals to the zero morphism. In the context of category theory, this is the kernel condition for `ι`.
More concisely: For any ShortComplex `S` in category `C` with RightHomologyData `self`, the composition of `self.ι` with the cokernel cofork of `S.g` (`self.hp.desc`) is equal to the zero morphism.
|
CategoryTheory.ShortComplex.opcyclesMap_comp
theorem CategoryTheory.ShortComplex.opcyclesMap_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₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
[inst_4 : S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ₁)
(CategoryTheory.ShortComplex.opcyclesMap φ₂)
This is a theorem in the field of category theory, specifically dealing with short complexes. Given a category `C` with zero morphisms, and three short complexes `S1`, `S2`, and `S3` in `C` that have respective right homologies, the theorem states that for any two morphisms `φ1 : S1 ⟶ S2` and `φ2 : S2 ⟶ S₃`, the operation of the `opcyclesMap` function on the composition of `φ1` and `φ2` is the same as the composition of the `opcyclesMap` of `φ1` and the `opcyclesMap` of `φ2`. In mathematical terms, this asserts the compatibility of the `opcyclesMap` with morphism composition, i.e., `opcyclesMap (φ1 ≫ φ2) = (opcyclesMap φ1) ≫ (opcyclesMap φ2)`.
More concisely: The `opcyclesMap` function of the composition of two morphisms between short complexes in a category with zero morphisms is equal to the composition of the `opcyclesMap` functions of the individual morphisms.
|
CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles
theorem CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles :
∀ {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.HasRightHomology],
CategoryTheory.CategoryStruct.comp S.rightHomologyι S.fromOpcycles = 0
This theorem states that for any type `C` which forms a category and has zero morphisms, given a `ShortComplex` `S` of `C` that has a right homology, the composition of the morphisms `rightHomologyι S` and `fromOpcycles S` in the category structure of `ShortComplex` is a zero morphism. In other words, in the category of short complexes, we always have `rightHomologyι S` followed by `fromOpcycles S` equals to zero morphism.
More concisely: For any type `C` forming a category with zero morphisms and having right homology, the composition of `rightHomologyι` and `fromOpcycles` morphisms in the category of `ShortComplex` of `C` is the zero morphism.
|
CategoryTheory.ShortComplex.p_fromOpcycles
theorem CategoryTheory.ShortComplex.p_fromOpcycles :
∀ {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.HasRightHomology],
CategoryTheory.CategoryStruct.comp S.pOpcycles S.fromOpcycles = S.g
The theorem `CategoryTheory.ShortComplex.p_fromOpcycles` states that for any Category `C` that has zero morphisms, and any Short Complex `S` in that Category that has right homology, the composition of the projection `S.X₂ ⟶ S.opcycles` (represented as `CategoryTheory.ShortComplex.pOpcycles S`) and the morphism `fromOpcycles S` is equal to the morphism `S.g`. In other words, in the context of category theory, this theorem demonstrates that certain morphisms in a short complex satisfy a specific compositional relationship.
More concisely: For any Short Complex `S` in a Category with zero morphisms having right homology, `CategoryTheory.ShortComplex.pOpcycles S` composing with `fromOpcycles S` equals `S.g`.
|
CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc
theorem CategoryTheory.ShortComplex.RightHomologyData.p_g'_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.RightHomologyData) {Z : C} (h_1 : S.X₃ ⟶ Z),
CategoryTheory.CategoryStruct.comp h.p (CategoryTheory.CategoryStruct.comp h.g' h_1) =
CategoryTheory.CategoryStruct.comp S.g h_1
The theorem `CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc` states that for any Category `C` with zero morphisms, any `ShortComplex` `S` of `C`, any `RightHomologyData` `h` of `S`, and any morphism `h_1` from `S.X₃` to some object `Z` in `C`, the composition of `h.p` with the composition of `h.g'` and `h_1` is equal to the composition of `S.g` and `h_1`. This theorem is expressing a certain associativity property in the context of Category Theory and Homological Algebra.
More concisely: For any Category `C` with zero morphisms, any ShortComplex `S` in `C`, any RightHomologyData `h` of `S`, and any morphism `h_1` from `S.X₃` to an object `Z` in `C`, we have `h.p ∘ (h.g' ∘ h_1) = (S.g ∘ h_1)`.
|
CategoryTheory.ShortComplex.RightHomologyMapData.commι
theorem CategoryTheory.ShortComplex.RightHomologyMapData.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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp self.φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι self.φQ
The theorem `CategoryTheory.ShortComplex.RightHomologyMapData.commι` states that in any category `C` with zero morphisms, given two Short Complex objects `S₁` and `S₂`, a morphism `φ` from `S₁` to `S₂`, and `RightHomologyData` instances `h₁` and `h₂` for `S₁` and `S₂` respectively, for any `RightHomologyMapData` instance (denoted by `self`), the composition of `self.φH` and `h₂.ι` is equal to the composition of `h₁.ι` and `self.φQ`. In mathematical terms, it's saying that in the context of category theory and homology, certain compositions of morphisms commute, i.e., `(self.φH) ≫ (h₂.ι) = (h₁.ι) ≫ (self.φQ)`.
More concisely: In any category with zero morphisms equipped with Right Homology Data instances, the composition of the horizontal homomorphism and the chain map induced by a morphism is equal to the composition of the chain map and the horizontal homomorphism for the other complex.
|
CategoryTheory.ShortComplex.RightHomologyData.p_descQ
theorem CategoryTheory.ShortComplex.RightHomologyData.p_descQ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0), CategoryTheory.CategoryStruct.comp h.p (h.descQ k hk) = k
The theorem `CategoryTheory.ShortComplex.RightHomologyData.p_descQ` states that for any category `C` with zero morphisms, and given a short complex `S` in `C`, and any `RightHomologyData` `h` for `S` and any object `A` in `C` with a morphism `k` from `S.X₂` to `A` such that the composition of `S.f` and `k` is the zero morphism, the composition of `h.p` and the `descQ` morphism derived from `h`, `k`, and `hk` equals `k`. This theorem is essentially formalizing a property of short complex diagrams in category theory in the context of homological algebra.
More concisely: Given a short complex in a category with zero morphisms, the `p` morphism of its right homology data and the `descQ` morphism derived from a morphism from the second complex element to an object, commute if the composition of the complex morphism and the given morphism is zero.
|
CategoryTheory.ShortComplex.RightHomologyMapData.commg'
theorem CategoryTheory.ShortComplex.RightHomologyMapData.commg' :
∀ {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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.CategoryStruct.comp self.φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃
The theorem `CategoryTheory.ShortComplex.RightHomologyMapData.commg'` states that for any objects `S₁` and `S₂` in a category `C` with zero morphisms, given morphism `φ : S₁ ⟶ S₂` and `RightHomologyData` objects `h₁` and `h₂` associated with `S₁` and `S₂` respectively, for any `RightHomologyMapData` object derived from `φ`, `h₁`, and `h₂`, the composition of `self.φQ` and `h₂.g'` is equal to the composition of `h₁.g'` and `φ.τ₃`. In simpler terms, this theorem is about the commutativity of certain mappings in the context of short complexes in category theory.
More concisely: For any morphism φ in a zero-morphism category C and associated RightHomologyData objects h₁ and h₂, the diagram commutes: h₁.g' ∘ φ = φ.τ₃ ∘ h₂.g'.
|
CategoryTheory.ShortComplex.opcyclesMap'_id
theorem CategoryTheory.ShortComplex.opcyclesMap'_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.RightHomologyData),
CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.id S) h h =
CategoryTheory.CategoryStruct.id h.Q
This theorem states that for any category `C` with zero morphisms, given a short complex `S` and a right homology data `h` of `S`, applying the `opcyclesMap'` function with the identity morphism on `S` as its argument, to `h` and `h` itself, is the same as applying the identity morphism on `h.Q`. In other words, for any object in the category, applying the `opcyclesMap'` function with the identity morphism is effectively the same as applying the identity morphism on the object's homology data.
More concisely: For any short complex in a category with zero morphisms and associated homology data, applying the `opcyclesMap'` function with the identity morphism to the homology data is equal to the identity morphism on the quotient object of the complex.
|
CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq
theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ = γ.φQ
This theorem states that in a category `C` with zero morphisms and for any two short complexes `S₁` and `S₂` with right homology data `h₁` and `h₂` respectively, and a morphism `φ` from `S₁` to `S₂`, the `opcyclesMap'` of `φ`, `h₁`, and `h₂` in the ShortComplex category theory is equal to the `φQ` property of the right homology map data `γ` associated with `φ`, `h₁`, and `h₂.
More concisely: In the ShortComplex category theory, the `opcyclesMap'` of a morphism `φ` between two short complexes with right homology data `h₁` and `h₂` equals the `φQ` property of the right homology map data `γ` associated with `φ`, `h₁`, and `h₂`.
|
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι
theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
CategoryTheory.CategoryStruct.comp h.rightHomologyIso.inv S.rightHomologyι =
CategoryTheory.CategoryStruct.comp h.ι h.opcyclesIso.inv
The given theorem is about categories, morphisms, and complexes in category theory. It states that for any type `C` that forms a category with zero morphisms, and for any `ShortComplex` `S` of this category `C`, the inverse of the right homology isomorphism composed with the right homology ι function is equal to the composition of the ι function of the right homology data and the inverse of the opcycles isomorphism of the right homology data.
This theorem essentially discusses the relationship between the inverse of the right homology isomorphism, the right homology ι function, and the inverse of the opcycles isomorphism in the context of short complexes in a category.
More concisely: For any category `C` with zero morphisms and any short complex `S` in `C`, the inverse of the right homology isomorphism and the right homology ι function, followed by the inverse of the opcycles isomorphism of the right homology data, is equal to the composition of the ι function of the right homology data and the inverse of the opcycles isomorphism.
|
CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc
theorem CategoryTheory.ShortComplex.RightHomologyData.p_descQ_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.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0) {Z : C} (h_1 : A ⟶ Z),
CategoryTheory.CategoryStruct.comp h.p (CategoryTheory.CategoryStruct.comp (h.descQ k hk) h_1) =
CategoryTheory.CategoryStruct.comp k h_1
The theorem `CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc` states that in the context of a category `C` which has zero morphisms, for any short complex `S` in `C` and any right homology data `h` of `S`, given a morphism `k` from `S.X₂` to some object `A` in `C` such that the composition of `S.f` and `k` is zero, and another morphism `h_1` from `A` to some object `Z` in `C`, the composition of `h.p` with the composition of the description `descQ` of `h` with `k` and `h_1` is equal to the composition of `k` and `h_1`. In simpler terms, it is a property of composition of morphisms in the context of a short complex and its right homology data in a category with zero morphisms.
More concisely: In a category with zero morphisms, for any short complex and its right homology data, the composition of the homology data's `p` map with the description of `h` through a zero-composing morphism and another morphism is equal to the composition of those morphisms.
|
CategoryTheory.ShortComplex.rightHomologyMap_comp
theorem CategoryTheory.ShortComplex.rightHomologyMap_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₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
[inst_4 : S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ₁)
(CategoryTheory.ShortComplex.rightHomologyMap φ₂)
The theorem `CategoryTheory.ShortComplex.rightHomologyMap_comp` states that for any category `C` that has zero morphisms, and for any three short complexes `S1`, `S2`, and `S3` (all in the category `C`) that have right homology maps, the right homology map of the composition of two morphisms `φ1 : S1 ⟶ S2` and `φ2 : S2 ⟶ S3` is equal to the composition of the right homology maps of `φ1` and `φ2`. In other words, the right homology map respects the composition in the category, which is a characteristic property of functorial behavior in category theory.
More concisely: For any three short complexes `S1`, `S2`, `S3` in a category `C` with zero morphisms, and morphisms `φ1 : S1 ⟶ S2` and `φ2 : S2 ⟶ S3` having right homology maps, the right homology map of their composition is equal to the composition of their right homology maps.
|
CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq
theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ = γ.φH
This theorem states that in a category `C` with zero morphisms, given two short complexes `S₁` and `S₂`, a morphism `φ` from `S₁` to `S₂`, and right homology data `h₁` and `h₂` for `S₁` and `S₂`, respectively, if `γ` is the right homology map data associated with `φ`, `h₁`, and `h₂`, then the right homology map associated with `φ`, `h₁`, and `h₂` is equal to `γ.φH`, the morphism of homologies in `γ`.
More concisely: In a category with zero morphisms, given two short complexes, a morphism between them, and right homology data, the right homology map of the morphism is equal to the composition of the morphism with the morphism of homologies in the right homology data.
|
CategoryTheory.ShortComplex.rightHomologyMap'_comp
theorem CategoryTheory.ShortComplex.rightHomologyMap'_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₁.RightHomologyData)
(h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData),
CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃)
This theorem is about the composition of morphisms in category theory, specifically within the context of short complexes. It states that for any category `C` that has zero morphisms, and for any three short complexes `S₁`, `S₂`, and `S₃` within `C`, if we have morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, along with right homology data `h₁`, `h₂`, and `h₃` for `S₁`, `S₂`, and `S₃` respectively, then the right homology map of the composition of `φ₁` and `φ₂` from `S₁` to `S₃` is equal to the composition of the right homology map of `φ₁` from `S₁` to `S₂` and the right homology map of `φ₂` from `S₂` to `S₃`. In essence, this theorem is expressing a property of functoriality of the right homology in the category of short complexes.
More concisely: Given any category `C` with zero morphisms and three short complexes `S₁`, `S₂`, `S₃`, along with morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, and right homology data `h₁`, `h₂`, and `h₃`, the right homology map of the composition `φ₁ ∘ φ₂` from `S₁` to `S₃` equals the composition of `h₁` and `h₂`.
|
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p
theorem CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p :
∀ {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₂.RightHomologyData)
[inst_2 : CategoryTheory.Epi φ.τ₁] [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).p =
CategoryTheory.CategoryStruct.comp φ.τ₂ h.p
This theorem is in the context of category theory, specifically the study of short complexes. A short complex in a category is a sequence of objects and morphisms with certain interacting properties. The theorem states that for any category `C` with zero morphisms and any short complexes `S₁` and `S₂` in `C`, given a morphism `φ` from `S₁` to `S₂` and a right homology data `h` for `S₂`, if `φ.τ₁` is an epimorphism, `φ.τ₂` is an isomorphism, and `φ.τ₃` is a monomorphism, then the morphism `p` obtained from `φ` and `h` using `RightHomologyData.ofEpiOfIsIsoOfMono'` is equal to the composition of `φ.τ₂` and `h.p`. The terms epimorphism, isomorphism, and monomorphism refer to specific types of morphisms in category theory, with epimorphisms generalizing the concept of surjectivity, isomorphisms generalizing bijections, and monomorphisms generalizing injections.
More concisely: Given short complexes $S\_1$ and $S\_2$ in a category $C$ with zero morphisms, a morphism $\varphi : S\_1 \to S\_2$, and right homology data $h$ for $S\_2$, if $\varphi.\tau\_1$ is an epimorphism, $\varphi.\tau\_2$ is an isomorphism, and $\varphi.\tau\_3$ is a monomorphism, then $RightHomologyData.ofEpiOfIsIsoOfMono' (\varphi, h) = \varphi.\tau\_2 \circ h.p$.
|
CategoryTheory.ShortComplex.rightHomologyι_naturality'
theorem CategoryTheory.ShortComplex.rightHomologyι_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₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.ι =
CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
This theorem, `CategoryTheory.ShortComplex.rightHomologyι_naturality'`, asserts that for any two short complexes `S₁` and `S₂` in a category `C` that has zero morphisms, and a morphism `φ` from `S₁` to `S₂`, the composition of the right homology map of `φ` and embedding map `h₂.ι` is equal to the composition of the embedding map `h₁.ι` and the map of chain complexes of `φ`. More formally, if `h₁` and `h₂` are the right homology data for `S₁` and `S₂` respectively, then the composition `(CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) ≫ h₂.ι` is equal to `h₁.ι ≫ (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)`. This asserts the naturality of the embedding map in the context of short complexes in category theory.
More concisely: Given short complexes $S\_1$, $S\_2$ in a category with zero morphisms, a morphism $\varphi$ from $S\_1$ to $S\_2$, and their respective right homology data $h\_1$ and $h\_2$, the composition of the right homology map of $\varphi$ with $h\_2.\ι$ equals the composition of $h\_1.\ι$ with the map of chain complexes of $\varphi$. In other words, $(h\_2.\ι \circ \text{rightHomologyMap'} \_\varphi \_ {h\_1} \_ {h\_2}) = (h\_1.\ι \circ \text{opcyclesMap'} \_\varphi \_ {h\_1} \_ {h\_2})$.
|
CategoryTheory.ShortComplex.f_pOpcycles
theorem CategoryTheory.ShortComplex.f_pOpcycles :
∀ {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.HasRightHomology],
CategoryTheory.CategoryStruct.comp S.f S.pOpcycles = 0
The theorem `CategoryTheory.ShortComplex.f_pOpcycles` asserts that for any given Short Complex `S` in a category `C` with zero morphisms, the composition of the morphism `S.f` with the projection `S.pOpcycles` is equal to the zero morphism. This holds under the assumption that `S` has a right homology. In mathematical terms, this is saying that $S.f \circ S.pOpcycles = 0$.
More concisely: Given a Short Complex `S` in a category `C` with zero morphisms and having right homology, the composite of `S.f` with `S.pOpcycles` equals the zero morphism.
|