CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility
theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h₁ h₁' : S.LeftHomologyData) (h₂ h₂' : S.RightHomologyData),
CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h₁')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂')
(CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h₂' h₂))
The theorem `CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility` states that for any category `C` with zero morphisms and any short complex `S` in `C`, given two pairs of left and right homology data `(h₁, h₂)` and `(h₁', h₂')` of `S`, the left-right homology comparison of `(h₁, h₂)` is equal to the composition of the left homology map of `(h₁, h₁')` and the composition of the left-right homology comparison of `(h₁', h₂')` and the right homology map of `(h₂', h₂)`. In other words, this theorem tells us that certain maps involving homology data in a short complex of a category are compatible with each other under composition.
More concisely: For any short complex in a category with zero morphisms, the left-right homology comparison of two pairs of homology data is equal to the composition of the corresponding left and right homology maps between the two pairs.
|
CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom
theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) (h : S.LeftHomologyData) [inst_2 : S.HasHomology],
CategoryTheory.CategoryStruct.comp S.homologyπ h.homologyIso.hom =
CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.π
This theorem, `CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom`, states that for any type `C` that forms a category with zero morphisms, and any short complex `S` in this category, as well as any left homology data `h` for this short complex, if `S` has homology, then the composition of the homology morphism of `S` and the homomorphism part of the homology isomorphism of `h` is equal to the composition of the homomorphism part of the cycles isomorphism of `h` and left homology morphism of `h`.
In terms of category theory, this theorem asserts an equality of two composed morphisms in certain conditions, which is a fundamental type of statement in the theory of categories and their morphisms.
More concisely: For any short complex `S` in a category with zero morphisms, and given left homology data `h` for `S` when it has homology, the composition of homology morphism of `S` and homomorphism part of homology isomorphism `h` equals the composition of homomorphism part of cycles isomorphism and left homology morphism of `h`.
|
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality
theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
(h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom
This theorem, `CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality`, specifies the naturality condition for the homology of short complexes in a category. Given any category `C` that has zero morphisms, and two short complexes `S₁` and `S₂` in `C` that have homology, this theorem states that for any morphism `φ` from `S₁` to `S₂`, and homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, the composition of the homology isomorphism of `h₁` and the right homology map of `φ`, `h₁` and `h₂` is equal to the composition of the homology map of `φ` and the homology isomorphism of `h₂`. This essentially states that the process of mapping the short complexes and then applying the homology isomorphism is the same as first applying the homology map and then the homology isomorphism, which is the characteristic property of natural transformations in category theory.
More concisely: Given any category with zero morphisms and two short complexes with homology, the homology isomorphism of one complex and the right homology map of a morphism between them is equal to the composition of the right homology map of the morphism and the homology isomorphism of the other complex.
|
CategoryTheory.ShortComplex.homologyMap_comp
theorem CategoryTheory.ShortComplex.homologyMap_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
[inst_4 : S₃.HasHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ₁)
(CategoryTheory.ShortComplex.homologyMap φ₂)
The `CategoryTheory.ShortComplex.homologyMap_comp` theorem states that for any category `C` with zero morphisms and any three 'short complexes' `S₁`, `S₂`, and `S₃` in that category, the homology map of the composite of two morphisms `φ₁` and `φ₂` (where `φ₁` maps `S₁` to `S₂` and `φ₂` maps `S₂` to `S₃`) is equal to the composite of the homology maps of `φ₁` and `φ₂`. In mathematical terms, this theorem asserts the functoriality of the homology map in the category of short complexes, that is, the homology map commutes with the composition of morphisms.
More concisely: The homology map between complexes commutes with composition of morphisms.
|
CategoryTheory.ShortComplex.homologyMap_id
theorem CategoryTheory.ShortComplex.homologyMap_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.id S) =
CategoryTheory.CategoryStruct.id S.homology
The theorem `CategoryTheory.ShortComplex.homologyMap_id` states that for any type `C`, given the category structure on `C` and assuming `C` has zero morphisms, for any short complex `S` in `C` that has a homology, the homology map of the identity morphism on `S` is equal to the identity morphism on the homology of `S`. In other words, this identity shows that the homology map behaves correctly with respect to identity morphisms in the category of short complexes.
More concisely: For any short complex `S` in a zero-morphism category `C` with homology, the homology map of the identity morphism on `S` equals the identity morphism on the homology of `S`.
|
CategoryTheory.ShortComplex.HomologyData.comm
theorem CategoryTheory.ShortComplex.HomologyData.comm :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (self : S.HomologyData),
CategoryTheory.CategoryStruct.comp self.left.π (CategoryTheory.CategoryStruct.comp self.iso.hom self.right.ι) =
CategoryTheory.CategoryStruct.comp self.left.i self.right.p
This theorem, called `CategoryTheory.ShortComplex.HomologyData.comm`, states that for any given category `C` of type `u`, which has zero morphisms, and a short complex `S` of `C`, the composition of morphisms satisfies a specific "pentagon" relation. This pentagon relation expresses the compatibility of the left and right homology data. More precisely, the composition of the morphism `self.left.π` and the composition of `self.iso.hom` and `self.right.ι` is equal to the composition of `self.left.i` and `self.right.p`. This illustrates that the morphisms of the left and right homology data in a short complex interact in a particular, structured way.
More concisely: Given a short complex in a zero-morphism category C, the composition of `self.left.π` with `self.iso.hom` and `self.right.ι` equals the composition of `self.left.i` and `self.right.p`.
|
CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι
theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
CategoryTheory.CategoryStruct.comp h₁.π
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.ι) =
CategoryTheory.CategoryStruct.comp h₁.i h₂.p
This theorem, `CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι`, states that for any type `C` which forms a category with zero morphisms, and for any short complex `S` of this category, given two pieces of homology data, `h₁` from the left and `h₂` from the right, the composition of morphisms `h₁.π` and `(CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) ≫ h₂.ι` is equal to the composition of morphisms `h₁.i` and `h₂.p`. This composition of morphisms is part of the structure of a category and is represented in Lean 4 by the function `CategoryTheory.CategoryStruct.comp`. This equality represents the coherency condition between the homology data from the left and right of a short complex.
More concisely: For any short complex in a category with zero morphisms, the composition of `h₁.π`, `CategoryTheory.ShortComplex.leftRightHomologyComparison' `h₁ `h₂`, and `h₂.ι` equals the composition of `h₁.i` and `h₂.p`. (This is the coherence condition for homology data of a short complex.)
|
CategoryTheory.ShortComplex.HasHomology.mk'
theorem CategoryTheory.ShortComplex.HasHomology.mk' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.HomologyData → S.HasHomology
This theorem states that for any type `C` that forms a category with zero morphisms, and any short complex `S` of this category, if `S` has homology data, then `S` also has homology. In other words, a short complex in a category that has zero morphisms and homology data is guaranteed to have homology. This is a foundation theorem in the field of category theory, a branch of mathematics focused on abstract structure and relationships.
More concisely: Given a type `C` forming a category with zero morphisms, every short complex `S` in `C` with homology data has well-defined homologies.
|
CategoryTheory.ShortComplex.homologyMap'_comp
theorem CategoryTheory.ShortComplex.homologyMap'_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.HomologyData)
(h₂ : S₂.HomologyData) (h₃ : S₃.HomologyData),
CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.homologyMap' φ₂ h₂ h₃)
The theorem `CategoryTheory.ShortComplex.homologyMap'_comp` states that for any category `C` of a certain type, given that `C` has zero morphisms, and given three short complexes `S₁`, `S₂` and `S₃` in `C`, along with morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, and their corresponding homology data `h₁`, `h₂`, and `h₃` respectively, the homology map of the composition of `φ₁` and `φ₂` from `h₁` to `h₃` is equal to the composition of the homology map of `φ₁` from `h₁` to `h₂` and the homology map of `φ₂` from `h₂` to `h₃`. This essentially expresses the compatibility of the homology maps with the composition in the category, a fundamental property in category theory.
More concisely: Given categories `C` with zero morphisms, short complexes `S₁`, `S₂`, `S₃`, morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, and their corresponding homology data `h₁`, `h₂`, `h₃`, the homology maps of their composition agree: `h₃.Hom(φ₁ ∘ φ₂) = h₂.Hom(φ₁) ∘ h₁.Hom(φ₂)`.
|
CategoryTheory.ShortComplex.HasHomology.condition
theorem CategoryTheory.ShortComplex.HasHomology.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} [self : S.HasHomology], Nonempty S.HomologyData
This theorem states that for any given category `C` with zero morphisms, and any short complex `S` in that category that has a homology, there exists a homology data associated with the short complex `S`. In other words, whenever we have a short complex with a homology in a category with zero morphisms, we can always find a structure of homology data for that short complex.
More concisely: Given a short complex in a category with zero morphisms, there exists a homology data structure for it if it has a defined homology.
|
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData
theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
S.rightHomologyData.homologyIso = S.rightHomologyIso.symm
This theorem in category theory states that for any short complex 'S' of a category 'C', assuming 'C' has zero morphisms and 'S' has right homology, the homology isomorphism given by the chosen right homology data of the short complex 'S' equals the inverse of the right homology isomorphism of the short complex 'S'. This ties the explicit construction of a right homology object to the abstract definition by the universal property.
More concisely: For any short complex S in a zero-object category C with right homology, the right homology isomorphism of S is the inverse of the right homology isomorphism given by its chosen data.
|
CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac
theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) [inst_2 : S.HasHomology],
CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv h₂.homologyIso.hom
This theorem, `CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac`, asserts that for any category `C` with zero morphisms and any short complex `S` within that category, given `LeftHomologyData` as `h₁` and `RightHomologyData` as `h₂` of `S`, and assuming that `S` has homology, the comparison of the left and right homology of `S` is equivalent to the composition of the inverse of the homology isomorphism for `h₁` and the homology isomorphism for `h₂`. In other words, the theorem provides a relationship between the left and right homologies of a short complex within a category.
More concisely: Given a short complex `S` in a category with zero morphisms and homology, the comparison of its left and right homology isomorphisms is equivalent to the composition of the inverse of the left homology isomorphism with the right homology isomorphism.
|
Mathlib.Algebra.Homology.ShortComplex.Homology._auxLemma.2
theorem Mathlib.Algebra.Homology.ShortComplex.Homology._auxLemma.2 :
∀ {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.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂)
(CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₂ h₃) =
CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃
This theorem states that for any category `C` equipped with zero morphisms, and given any three `ShortComplex` objects `S₁`, `S₂`, `S₃` in that category, along with morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, and left homology data `h₁`, `h₂`, `h₃` corresponding to these objects, the composition of the left homology maps corresponding to the morphisms `φ₁` and `φ₂` is equal to the left homology map corresponding to the composition of the morphisms `φ₁` and `φ₂`. In mathematical terms, we have `(φ₁ * φ₂) * h = φ₁ * (φ₂ * h)` where `*` denotes the composition of morphisms, showing that the operation of taking left homology maps is compatible with the composition of morphisms.
More concisely: Given any three objects `S₁`, `S₂`, `S₃` in a category with zero morphisms, and morphisms `φ₁ : S₁ ⟶ S₂` and `φ₂ : S₂ ⟶ S₃`, the left homology maps satisfy `(φ₁ * φ₂) * h = φ₁ * (φ₂ * h)`, where `*` denotes composition of morphisms.
|
CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData
theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
S.leftHomologyData.homologyIso = S.leftHomologyIso.symm
This theorem states that for any category `C` with zero morphisms, and any short complex `S` within that category that possesses a homology, the isomorphism generated by the left homology data of `S` is the inverse of the isomorphism generated by the left homology of `S`. In other words, it affirms the compatibility of the homology data with the actual left homology in a short complex in a mathematical category, providing a symmetry between these two constructions.
More concisely: In a category with zero morphisms, the left homology isomorphisms of any short complex with homology coincide.
|
CategoryTheory.ShortComplex.homologyπ_naturality
theorem CategoryTheory.ShortComplex.homologyπ_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
CategoryTheory.CategoryStruct.comp S₁.homologyπ (CategoryTheory.ShortComplex.homologyMap φ) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.homologyπ
The theorem `CategoryTheory.ShortComplex.homologyπ_naturality` states that for any given category `C` which has zero morphisms, and for any two short complexes `S₁` and `S₂` in `C` with existent homologies, the composition of the homology π-function of `S₁` and the homology map of a morphism `φ` from `S₁` to `S₂` is equal to the composition of the cycles map of `φ` and the homology π-function of `S₂`. In simpler terms, it means that when you map from one short complex to another, applying the homology π-function first, then the homology map, gives you the same result as applying the cycles map first, then the homology π-function. This is a form of naturality condition in the context of category theory.
More concisely: For any short complexes $S\_1$ and $S\_2$ in a category with zero morphisms and existent homologies, the diagram commutes: $\pi\_{n}(S\_1) \circ \phi = \pi\_{n}(S\_2) \circ \zeta\_\phi$ for all $n$, where $\pi\_{n}$ denotes the $n$th homology $\pi$-function, $\phi$ is a morphism from $S\_1$ to $S\_2$, and $\zeta\_\phi$ is the corresponding homology map.
|
CategoryTheory.ShortComplex.homologyMap'_id
theorem CategoryTheory.ShortComplex.homologyMap'_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.id S) h h =
CategoryTheory.CategoryStruct.id h.left.H
The theorem `CategoryTheory.ShortComplex.homologyMap'_id` states that for any category `C` with zero morphisms, and any short complex `S` in `C`, if `h` is a homology data of `S`, then the homology map of the identity morphism on `S` from `h` to `h` is the identity morphism on the left homology object of `h`. In simpler terms, it says that the homology map of the identity on a short complex is the identity on the homology. This is a fundamental property expected of any homological functor.
More concisely: For any short complex in a category with zero morphisms, the homology map of the identity morphism is the identity on the homology object.
|
CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq
theorem CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
CategoryTheory.ShortComplex.leftRightHomologyComparison' h.left h.right = h.iso.hom
This theorem states that for any Category `C` that has zero morphisms, and any `ShortComplex` `S` in `C`, given a `HomologyData` `h` for `S`, the left-right homology comparison of the left and right data of `h` is equal to the `homomorphism` of the `iso` of `h`. In the language of category theory, this is a statement about the relation between the homological properties of short complexes and their associated homology data.
More concisely: Given a Category `C` with zero morphisms and any ShortComplex `S` in `C` with HomologyData `h`, the left-right homology comparison of `h` equals the homomorphism of `h`'s isomorphism.
|
CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq
theorem CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
(γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = γ.left.φH
The theorem `CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq` states that for any category `C` with zero morphisms, given two objects `S₁` and `S₂` in the category of short complexes over `C`, a morphism `φ` from `S₁` to `S₂`, homology data `h₁` and `h₂` for `S₁` and `S₂` respectively, and a homology map data `γ` for the morphism `φ` with respect to `h₁` and `h₂`, the homology map derived from `φ`, `h₁` and `h₂` is equal to the left part of the homology map in `γ`.
More concisely: For any short complexes $S\_1$ and $S\_2$ over a category $C$ with zero morphisms, given homology data $h\_1$ for $S\_1$, $h\_2$ for $S\_2$, a morphism $\varphi$ from $S\_1$ to $S\_2$, and homology map data $\gamma$ for $\varphi$ and $h\_1$, $h\_2$: the homology map of $\varphi$ derived from $h\_1$ and $h\_2$ equals the left part of the homology map in $\gamma$.
|
CategoryTheory.ShortComplex.homologyι_naturality
theorem CategoryTheory.ShortComplex.homologyι_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.homologyι =
CategoryTheory.CategoryStruct.comp S₁.homologyι (CategoryTheory.ShortComplex.opcyclesMap φ)
This theorem states that given any category `C` with zero morphisms, and two short complexes `S₁` and `S₂` in `C`, for any morphism `φ` from `S₁` to `S₂`, the composition of the homology map of `φ` and the homology insertion of `S₂` is equal to the composition of the homology insertion of `S₁` and the cycles map of `φ`. This essentially showcases the naturality of the homology insertion in the context of short complexes in a category.
More concisely: Given any category with zero morphisms, for short complexes $S\_1$ and $S\_2$, and a morphism $\varphi$ from $S\_1$ to $S\_2$, the homology insertion of $S\_2$ and the homology map of $\varphi$ are naturally equal to the homology insertion of $S\_1$ and the cycles map of $\varphi$.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
CategoryTheory.ShortComplex.homologyMap φ =
CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom
(CategoryTheory.CategoryStruct.comp γ.φH h₂.homologyIso.inv)
The theorem `CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq` asserts that for any category `C` with zero morphisms, given two short complexes `S₁` and `S₂` in `C` and a morphism `φ` from `S₁` to `S₂`, and assuming `S₁` and `S₂` both have a left homology, then the homology map of `φ` is equal to the composition of the homomorphism of the homology isomorphism of `h₁`, the morphism `φH` of the left homology map data `γ`, and the inverse of the homology isomorphism of `h₂`, where `h₁` and `h₂` are the left homology data of `S₁` and `S₂` respectively. In other words, the theorem describes a specific commutative diagram in the context of short complexes in a category.
More concisely: Given two short complexes in a category with zero morphisms and a morphism between them, if both complexes have defined left homologies, then the homology map of the morphism is equal to the composition of the inverse of the left homology isomorphism of the target complex, the morphism itself, and the left homology isomorphism of the source complex.
|