AlgebraicTopology.DoldKan.cs_down_0_not_rel_left
theorem AlgebraicTopology.DoldKan.cs_down_0_not_rel_left : ∀ (j : ℕ), ¬AlgebraicTopology.DoldKan.c.Rel 0 j
This theorem, named `AlgebraicTopology.DoldKan.cs_down_0_not_rel_left`, states that for all natural numbers `j`, the relation `Rel` of the complex shape `AlgebraicTopology.DoldKan.c` (which is defined to be the 'down' direction of a chain complex indexed by `ℕ`, where the relation is true if and only if `n+1=m`) does not hold when the first argument is `0`. In other words, there is no natural number `j` such that `j+1=0` in the context of this chain complex. This is intended to be used with the lemma `nullHomotopicMap'_f_of_not_rel_left`.
More concisely: The relation in the `AlgebraicTopology.DoldKan.c` chain complex is not defined for the index 0.
|
AlgebraicTopology.DoldKan.Hσ_eq_zero
theorem AlgebraicTopology.DoldKan.Hσ_eq_zero :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q : ℕ), (AlgebraicTopology.DoldKan.Hσ q).f 0 = 0
The theorem `AlgebraicTopology.DoldKan.Hσ_eq_zero` states that for any natural number `q`, the null homotopic map `Hσ` applied to `q` and evaluated at degree `0` is zero. This holds for any category `C` (denoted by the type `C : Type`) that is both a category (i.e., it satisfies the axioms of a category as per `CategoryTheory.Category`) and is preadditive (i.e., it has a structure of an additive category as per `CategoryTheory.Preadditive`). Furthermore, this category `C` should act on a simplicial object `X` (which is a contravariant functor from the Simplex Category to `C`).
More concisely: For any preadditive category `C` acting on a simplicial object `X`, the null homotopic map `Hσ` evaluated at degree 0 is equal to zero.
|
AlgebraicTopology.DoldKan.hσ'_naturality
theorem AlgebraicTopology.DoldKan.hσ'_naturality :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n m : ℕ)
(hnm : AlgebraicTopology.DoldKan.c.Rel m n) {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n)))
(AlgebraicTopology.DoldKan.hσ' q n m hnm) =
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.hσ' q n m hnm)
(f.app (Opposite.op (SimplexCategory.mk m)))
This theorem, `AlgebraicTopology.DoldKan.hσ'_naturality`, states that for any category `C` which is a preadditive category, for any natural numbers `q`, `n`, and `m`, for any relation `hnm` that holds if `n+1=m`, and for any morphism `f` from a simplicial object `X` to a simplicial object `Y` in `C`, the composition of `f` applied to the `n`-th object of the simplicial object and the map `hσ'` applied to `q`, `n`, `m`, and `hnm`, is equal to the composition of `hσ'` applied to `q`, `n`, `m`, and `hnm`, and `f` applied to the `m`-th object. This is essentially saying that the maps `hσ' q n m hnm` are natural transformations on the simplicial objects in the category `C`.
More concisely: For any preadditive category `C`, any natural numbers `q`, `n`, `m`, and relation `hnm` with `n+1=m`, and any morphism `f` between simplicial objects `X` and `Y` in `C`, the diagram commutes:
```
X_n ➔ X_m (hσ' q n m hnm) ∘ f
| |
| v
Y_n ➔ Y_m f ∘ (hσ' q n m hnm)
```
Therefore, `hσ' q n m hnm` is a natural transformation from the `n`-th object functor to the `m`-th object functor on the category of simplicial objects in `C`.
|
AlgebraicTopology.DoldKan.c_mk
theorem AlgebraicTopology.DoldKan.c_mk : ∀ (i j : ℕ), j + 1 = i → AlgebraicTopology.DoldKan.c.Rel i j
The theorem `AlgebraicTopology.DoldKan.c_mk` states that for every pair of natural numbers `(i, j)`, if `j + 1` is equal to `i`, then the relation `Rel i j` holds under the complex shape `AlgebraicTopology.DoldKan.c` which is defined as the downward direction in natural numbers. This might be needed when we are working with chain complexes indexed by `ℕ` and we require the relation `Rel i j` where `j + 1 = i`.
More concisely: For the complex `AlgebraicTopology.DoldKan.c`, the relation `Rel` holds between indices `i` and `j` when `j + 1 = i`.
|
AlgebraicTopology.DoldKan.map_hσ'
theorem AlgebraicTopology.DoldKan.map_hσ' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{D : Type u_2} [inst_2 : CategoryTheory.Category.{u_3, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
(G : CategoryTheory.Functor C D) [inst_4 : G.Additive] (X : CategoryTheory.SimplicialObject C) (q n m : ℕ)
(hnm : AlgebraicTopology.DoldKan.c.Rel m n),
AlgebraicTopology.DoldKan.hσ' q n m hnm = G.map (AlgebraicTopology.DoldKan.hσ' q n m hnm)
This theorem states that for two categories `C` and `D` that have preadditive structures, and a functor `G` from `C` to `D` that preserves the additive structure, the maps `hσ' q n m hnm`, which are associated with a simplicial object `X` in `C` and a certain condition on integers `m` and `n`, commute with the application of the functor `G`. In other words, applying `hσ'` to `q n m hnm` and then applying the functor `G` gives the same result as first applying the functor to `hσ' q n m hnm`.
More concisely: For functors G between preadditive categories preserving additive structures, the diagram commutes:
hσ' (G(q) n m (G(hnm))) ≈ G(hσ' q n m hnm)
|
AlgebraicTopology.DoldKan.map_Hσ
theorem AlgebraicTopology.DoldKan.map_Hσ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{D : Type u_2} [inst_2 : CategoryTheory.Category.{u_3, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
(G : CategoryTheory.Functor C D) [inst_4 : G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ),
(AlgebraicTopology.DoldKan.Hσ q).f n = G.map ((AlgebraicTopology.DoldKan.Hσ q).f n)
The theorem `AlgebraicTopology.DoldKan.map_Hσ` states that the null homotopic maps `Hσ` are compatible with the application of additive functors. More specifically, for any category `C` that is preadditive (meaning that it has an abelian group structure on its hom-sets), any category `D` that is also preadditive, any additive functor `G` from `C` to `D`, any simplicial object `X` in `C`, and any natural numbers `q` and `n`, the `n`-th element of the map `Hσ q` equals to the map of the `n`-th element of `Hσ q` under functor `G`. In other words, this theorem is asserting the compatibility of null homotopic maps and additive functors.
More concisely: For any preadditive categories `C` and `D`, additive functor `G` from `C` to `D`, simplicial object `X` in `C`, and natural numbers `q` and `n`, the map `Hσ q` of the `n`-th element of the simplicial object `X` in category `C` is equal to the map `G(Hσ q X)` of the `n`-th element of the image of `X` under `G` in category `D`.
|