CategoryTheory.ShortComplex.RightHomologyMapData.map_φH
theorem CategoryTheory.ShortComplex.RightHomologyMapData.map_φH :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
{h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D)
[inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F] [inst_6 : h₂.IsPreservedBy F],
(ψ.map F).φH = F.map ψ.φH
This theorem states that for any two short complexes `S₁` and `S₂` in categories `C` and `D` respectively, and a morphism `φ` from `S₁` to `S₂`, if we have right homology data `h₁` and `h₂` for `S₁` and `S₂`, and a right homology map data `ψ` that links `φ`, `h₁`, and `h₂`, then if we have a functor `F` from `C` to `D` that preserves zero morphisms and preserves the right homology data `h₁` and `h₂`, the right homology map data `ψ` produced by mapping `F` over `ψ` using `CategoryTheory.ShortComplex.RightHomologyMapData.map` has its `φH` component equal to the result of mapping `F` over the `φH` component of `ψ`.
More concisely: Given any two short complexes `S₁` and `S₂`, a morphism `φ: S₁ → S₂`, right homology data `h₁`, `h₂`, and a right homology map data `ψ` connecting `φ` and `h₁`, `h₂`, if `F : C → D` is a functor preserving zero morphisms and `h₁`, `h₂`, then `F.map (ψ)`.`φH` equals `F.(ψ.φH)`.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
{h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (F : CategoryTheory.Functor C D)
[inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F] [inst_6 : h₂.IsPreservedBy F],
(ψ.map F).φH = F.map ψ.φH
This theorem states that for any categories `C` and `D`, S₁ and S₂ as short complexes of `C`, a morphism `φ` from S₁ to S₂, left homology data `h₁` for S₁ and `h₂` for S₂, a left homology map data `ψ` for `φ`, and a functor `F` from `C` to `D` that preserves zero morphisms and for which the left homology data is preserved by `h₁` and `h₂`, the φH component of the map of the left homology map data `ψ` under the functor `F` is equal to the functor `F` applied to the φH component of `ψ`.
More concisely: For any categories `C` and `D`, functor `F:` `C` -> `D` preserving zero morphisms and left homology data, and short complexes `S₁` and `S₂` in `C` with morphism `φ:` `S₁` -> `S₂`, the induced map on left homology `F(ψφH) = F(ψ)F(φH)`, where `ψ` is a left homology map data for `φ`.
|
Mathlib.Algebra.Homology.ShortComplex.PreservesHomology._auxLemma.2
theorem Mathlib.Algebra.Homology.ShortComplex.PreservesHomology._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₃
The theorem `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology._auxLemma.2` asserts that for any category `C` with zero morphisms, and any three short complexes `S₁`, `S₂`, and `S₃` in `C`, if `φ₁` is a morphism from `S₁` to `S₂`, `φ₂` is a morphism from `S₂` to `S₃`, and `h₁`, `h₂`, and `h₃` are the left homology data of `S₁`, `S₂`, and `S₃` respectively, then the composition of the left homology maps induced by `φ₁` and `φ₂` is equal to the left homology map induced by the composition of `φ₁` and `φ₂`. In other words, the left homology maps respect the composition operation of the category.
More concisely: The theorem asserts that the left homology maps induced by composable morphisms between short complexes in a category with zero morphisms are equal.
|
CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap'
theorem CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap' :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_3, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
(hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : CategoryTheory.Functor C D)
[inst_4 : F.PreservesZeroMorphisms] [inst_5 : hl₁.IsPreservedBy F] [inst_6 : hl₂.IsPreservedBy F],
F.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) =
CategoryTheory.ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
This Lean theorem, `CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap'`, states that for any two short complexes `S₁` and `S₂` in categories `C` and `D` with zero morphisms, given a morphism `φ` from `S₁` to `S₂`, left homology data `hl₁` for `S₁` and `hl₂` for `S₂`, and a functor `F` from `C` to `D` which preserves zero morphisms and left homology data, the mapping of the left homology map of `φ` by `F` is equal to the left homology map of the mapping of `φ` by the short complex functor of `F`, with the mappings of `hl₁` and `hl₂` by `F` as the respective left homology data. Essentially, the theorem asserts that the process of mapping a left homology map by a functor is compatible with the process of mapping a morphism between short complexes by the short complex functor of the same functor and then taking the left homology map.
More concisely: Given short complexes $S\_1$ and $S\_2$ in categories $C$ and $D$ with zero morphisms, a morphism $\varphi$ from $S\_1$ to $S\_2$, left homology data $hł\_1$ for $S\_1$ and $hł\_2$ for $S\_2$, and a functor $F$ from $C$ to $D$ preserving zero morphisms and left homology data, the map of the left homology map of $\varphi$ by $F$ equals the left homology map of the map of $\varphi$ by the short complex functor of $F$, with the images of $hł\_1$ and $hł\_2$ under $F$ as the respective left homology data.
|