HomologicalComplex.homologyι_naturality
theorem HomologicalComplex.homologyι_naturality :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
[inst_3 : L.HasHomology i],
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (L.homologyι i) =
CategoryTheory.CategoryStruct.comp (K.homologyι i) (HomologicalComplex.opcyclesMap φ i)
The theorem `HomologicalComplex.homologyι_naturality` states that for any two homological complexes `K` and `L` in a category `C` with zero morphisms, if `K` and `L` have homology in degree `i`, then the composition of the homology map `φ` from `K` to `L` and the inclusion map of `L` at degree `i` is equal to the composition of the inclusion map of `K` at degree `i` and the map of cycles induced by `φ`. This theorem captures the natural behavior of homology in the context of category theory.
The underlying mathematics involves concepts from algebraic topology and category theory, including homological complexes, homology, and the composition of morphisms in a category.
More concisely: Given homological complexes K and L in a category with zero morphisms, the inclusion-induced map of i-th homology cycles is equal to the composition of the i-th homology map from K to L and the inclusion map of L.
|
HomologicalComplex.isoHomologyπ_hom_inv_id_assoc
theorem HomologicalComplex.isoHomologyπ_hom_inv_id_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
[inst_2 : K.HasHomology j] {Z : C} (h_1 : K.cycles j ⟶ Z),
CategoryTheory.CategoryStruct.comp (K.homologyπ j)
(CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv h_1) =
h_1
This theorem states that for any category `C` (with zero morphisms), a `ComplexShape` `c`, and a `HomologicalComplex` `K` based on `C` and `c`, given indices `i` and `j` such that the `prev` function of `c` maps `j` to `i`, and the morphism from `i` to `j` in `K` is zero, if `K` has homology in degree `j`, then for any morphism from the cycles in degree `j` of `K` to some object `Z`, the composition of the `homologyπ` of `K` in degree `j` and the inverse of `isoHomologyπ` of `K` for `i`, `j` followed by the given morphism is equal to the given morphism itself. This essentially asserts that a certain naturally defined morphism behaves as an identity under specific conditions.
More concisely: For any category `C` with zero morphisms, a `ComplexShape` `c`, a `HomologicalComplex` `K` based on `C` and `c`, indices `i` and `j` with `prev(j) = i` and `K(i, j) = 0`, and a morphism from the cycles in degree `j` of `K` to some object `Z`, the composition of `homologyπ(K)(j)`, `isoHomologyπ(K).inv` for `i`, `j`, and the given morphism equals the given morphism itself.
|
HomologicalComplex.homologyMap_id
theorem HomologicalComplex.homologyMap_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.id K) i =
CategoryTheory.CategoryStruct.id (K.homology i)
The theorem `HomologicalComplex.homologyMap_id` states that for any category `C` with zero morphisms, any complex shape `c`, and any homological complex `K` in `C` with shape `c`, and for any object `i` in `ι` where `K` has homology in degree `i`, the homology map applied to the identity morphism on `K` in degree `i` is the same as the identity morphism on the homology of `K` in degree `i`. Essentially, the homology map preserves the identity, which is a necessary characteristic for any functor in category theory.
More concisely: For any homological complex `K` in a category `C` with zero morphisms and shape `c`, the homology map of the identity morphism on `K` in degree `i` equals the identity morphism on the homology of `K` in degree `i`, where `i` is an object such that `K` has homology in degree `i`.
|
HomologicalComplex.p_descOpcycles
theorem HomologicalComplex.p_descOpcycles :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
(k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0),
CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.descOpcycles k j hj hk) = k
Theorem `HomologicalComplex.p_descOpcycles` states that for any category `C` with zero morphisms, any complex shape `c`, and any homological complex `K` in `C` which has homology at index `i`, if `A` is an object in `C`, `k` is a morphism from `K.X i` to `A`, `j` is an index such that `j` is the previous index of `i` in the complex shape `c`, and the composition of the differentials `K.d j i` and `k` is the zero morphism, then the composition of the projection to the opcycles of `K` at `i` and the descendent opcycles of `K` with `k`, `j`, `hj`, and `hk` is equal to `k`. In essence, this theorem describes how differentials and morphisms behave in relation to the opcycles of a homological complex.
More concisely: Given a homological complex `K` in a category `C` with zero morphisms, if the composition of the differential `K.d j i` and morphism `k` from `K.X i` to an object `A` is zero, then the composition of `K.Z i`.`proj`, `K.Z j`.`desc`, `hj`, `hk`, and `k` equals `k`.
|
HomologicalComplex.liftCycles_i
theorem HomologicalComplex.liftCycles_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
(k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0),
CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (K.iCycles i) = k
The theorem `HomologicalComplex.liftCycles_i` states that for any homological complex `K` of a category `C` (where `C` is a category with zero morphisms), given an index `i` such that `K` has homology at `i`, a morphism `k` from some object `A` to `K.X i`, and another index `j` such that `j` is the next index after `i` in the complex shape `c`, if the composition of `k` and the differential `K.d i j` is the zero morphism, then the composition of `HomologicalComplex.liftCycles K k j hj hk` and the inclusion of cycles `HomologicalComplex.iCycles K i` equals `k`.
In other words, this theorem demonstrates that we can lift cycles in a homological complex such that they are mapped correctly by the inclusion of cycles, aligning with the expected behavior in homology theory.
More concisely: Given a homological complex `K` in a category `C` with zero morphisms, a morphism `k` from an object `A` to `K.X i`, and indices `i` and `j` such that `i` has homology, `j` is the next index, and `k ∘ K.d i j` is the zero morphism, the cycle lifting map `HomologicalComplex.liftCycles K k j hj hk` equals `k` when composed with the inclusion of cycles `HomologicalComplex.iCycles K i`.
|
HomologicalComplex.p_fromOpcycles
theorem HomologicalComplex.p_fromOpcycles :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i],
CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.fromOpcycles i j) = K.d i j
The theorem `HomologicalComplex.p_fromOpcycles` states that for any category `C` with zero morphisms, and for any homological complex `K` of a certain complex shape with homology in degree `i`, the composition of the projection to the opcycles of `K` at `i` and the morphism from opcycles of `K` between `i` and `j`, is equal to the differential `d` of `K` between `i` and `j`.
In other words, if you have a homological complex `K`, and pick two degrees `i` and `j`, the process of first projecting to the opcycles at `i` and then mapping from opcycles between `i` and `j`, is the same as directly applying the differential from `i` to `j`. This theorem essentially asserts a compatibility condition between the differential and the projection to/from the opcycles.
More concisely: For any homological complex in a category with zero morphisms, the projection to opcycles followed by the morphism between opcycles is equal to the differential between the corresponding degrees.
|
HomologicalComplex.toCycles_i
theorem HomologicalComplex.toCycles_i :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j],
CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.iCycles j) = K.d i j
This theorem, `HomologicalComplex.toCycles_i`, states that for any category `C` with zero morphisms, and any complex shape `c` indexed by `ι`, given a homological complex `K` of category `C` with shape `c`, and two indices `i` and `j` from `ι`, when `K` has homology at index `j`, the composition of the morphism `toCycles` from `i` to `j` in `K` and the inclusion morphism of the cycles at `j` in `K` is equal to the morphism `d` from `i` to `j` in `K`. In other words, in the language of category theory, the diagram involving the `toCycles`, `iCycles`, and `d` morphisms commutes.
More concisely: For any homological complex in a zero-morphism category, the composition of `toCycles` from `i` to `j` and the inclusion of `j`-cycles is equal to the differential `d` from `i` to `j`.
|
HomologicalComplex.homologyMap_comp
theorem HomologicalComplex.homologyMap_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
[inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i],
HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i =
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyMap ψ i)
The theorem `HomologicalComplex.homologyMap_comp` establishes the associativity of homology maps in a homological complex. Specifically, given a category `C` with zero morphisms, and `K`, `L`, and `M` as homological complexes in `C`, along with morphisms `φ` from `K` to `L` and `ψ` from `L` to `M`, for any index `i` such that `K`, `L`, and `M` all have homology at `i`, the composition of the homology maps corresponding to `φ` and `ψ` is equal to the homology map corresponding to the composition of `φ` and `ψ`. In mathematical notation, this can be represented as `(φ * ψ)_* = φ_* * ψ_*`, where `_ *` denotes the homology map of a morphism.
More concisely: For homological complexes $K$, $L$, $M$ in a category with zero morphisms and morphisms $\varphi: K \to L$ and $\psi: L \to M$, the homology maps satisfy $(\varphi \circ \psi)_\ast = \varphi_\ast \circ \psi_\ast$.
|