AlgebraicTopology.DoldKan.karoubi_PInfty_f
theorem AlgebraicTopology.DoldKan.karoubi_PInfty_f :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (n : ℕ),
(AlgebraicTopology.DoldKan.PInfty.f n).f =
CategoryTheory.CategoryStruct.comp (Y.p.app (Opposite.op (SimplexCategory.mk n)))
(AlgebraicTopology.DoldKan.PInfty.f n)
This theorem relates to the field of algebraic topology and specifically deals with simplicial objects and Dold-Kan correspondence. Given a type `C` which forms a category and is pre-additive, and an object `Y` from the Karoubi envelope of the category of simplicial objects in `C`, it states that for every natural number `n`, the morphism associated with the nth object of the simplicial object associated with `PInfty` is equivalent to the composition of the morphism associated with the nth object of `Y` and the morphism associated with the nth object of the simplicial object associated with `PInfty`. In mathematical terms, (PInfty.f n).f = Y.p.app (Opposite.op (SimplexCategory.mk n)) ≫ (PInfty.f n).
The lemma bridges the notion of the Karoubi envelope and the `PInfty` functor in the study of algebraic topology.
More concisely: For every natural number n, the morphism from the n-th object of the simplicial object associated with `PInfty` is equivalent to the composition of the morphism from the n-th object of the object `Y` in the Karoubi envelope and the morphism from the n-th object of the simplicial object associated with `PInfty` in the category of simplicial objects over a pre-additive category `C`.
|
AlgebraicTopology.DoldKan.PInfty_f_idem
theorem AlgebraicTopology.DoldKan.PInfty_f_idem :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (n : ℕ),
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (AlgebraicTopology.DoldKan.PInfty.f n) =
AlgebraicTopology.DoldKan.PInfty.f n
This theorem states that for any category `C` (which is of some type `u_1`, and is preadditive), and any simplicial object `X` in this category, the morphism `AlgebraicTopology.DoldKan.PInfty.f` is idempotent for any natural number `n`. In other words, composing `AlgebraicTopology.DoldKan.PInfty.f` with itself (using `CategoryTheory.CategoryStruct.comp`) results in the original morphism `AlgebraicTopology.DoldKan.PInfty.f`. This property is crucial in the study of algebraic topology, particularly in the exploration of Dold-Kan correspondences.
More concisely: For any preadditive category `C` and simplicial object `X` in `C`, the Dold-Kan morphism `AlgebraicTopology.DoldKan.PInfty.f` is idempotent.
|
AlgebraicTopology.DoldKan.PInfty_f_naturality
theorem AlgebraicTopology.DoldKan.PInfty_f_naturality :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
{X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n)))
(AlgebraicTopology.DoldKan.PInfty.f n) =
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
(f.app (Opposite.op (SimplexCategory.mk n)))
This theorem, named `AlgebraicTopology.DoldKan.PInfty_f_naturality`, asserts a principle of naturality for the Dold-Kan correspondence in algebraic topology. Specifically, for any category `C` which is preadditive, any natural number `n`, and any two simplicial objects `X` and `Y` in `C` with a morphism `f` from `X` to `Y`, the composition of `f` with the `n`-th Dold-Kan correspondence functor applied to `Y` is equal to the composition of the `n`-th Dold-Kan correspondence functor applied to `X` with `f`. In other words, the Dold-Kan correspondence functor commutes with morphisms in the category of simplicial objects.
More concisely: For any preadditive category `C`, the Dold-Kan correspondence functor from simplicial objects in `C` to chain complexes preserves natural transformations.
|
AlgebraicTopology.DoldKan.PInfty_f
theorem AlgebraicTopology.DoldKan.PInfty_f :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (n : ℕ),
AlgebraicTopology.DoldKan.PInfty.f n = (AlgebraicTopology.DoldKan.P n).f n
The theorem `AlgebraicTopology.DoldKan.PInfty_f` states that for any category `C` which is preadditive, and any `X` which is a simplicial object in `C`, the `f` operation (part of a functor or morphism in the category) of the `PInfty` construction at a natural number `n` is equal to the `f` operation of the `P` construction at the same `n`. This theorem is part of the Dold-Kan correspondence which relates simplicial objects and chain complexes in a certain way.
More concisely: For any preadditive category `C` and simplicial object `X` in `C`, the `n`-th `f` operation of the `PInfty` construction equals the `n`-th `f` operation of the `P` construction.
|