AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ}
{φ : Y ⟶ X.obj (Opposite.op (SimplexCategory.mk (n + 1)))},
AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = φ
This theorem states that for any category `C`, which is also a preadditive category, and for any simplicial object `X` in `C` and object `Y` in `C`, and for any natural numbers `n` and `q`, if a morphism `φ` from `Y` to the (`n+1`)-th object of `X` satisfies the higher faces vanish condition at `q`, then the composition of `φ` with the (`n+1`)-th morphism of the Dold-Kan correspondence at `q` is equal to `φ` itself.
In other words, it establishes that under the higher faces vanish condition, the `φ` morphism is a sort of identity for the composition operation with the Dold-Kan correspondence morphism. This is a property related to the structure of simplicial objects in a category within the context of algebraic topology.
More concisely: Given a preadditive category `C`, any simplicial object `X` in `C`, object `Y` in `C`, natural numbers `n` and `q`, and a morphism `φ` from `Y` to the `(n+1)`-th object of `X` satisfying the higher faces vanish condition at `q`, then `φ` is equal to the composition of `φ` with the `(n+1)`-th morphism of the Dold-Kan correspondence at `q`.
|
AlgebraicTopology.DoldKan.P_f_naturality
theorem AlgebraicTopology.DoldKan.P_f_naturality :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
{X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n)))
((AlgebraicTopology.DoldKan.P q).f n) =
CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n)
(f.app (Opposite.op (SimplexCategory.mk n)))
The theorem `AlgebraicTopology.DoldKan.P_f_naturality` states that for any category `C` that is preadditive, for any natural numbers `q` and `n`, and for any morphism `f` between two simplicial objects `X` and `Y` in `C`, the composition of the application of `f` to the opposite of the simplex category object created from `n`, and the application of the Dold-Kan correspondence `P` (for a given `q`) to `n`, is equal to the composition of the application of `P` to `n` and the application of `f` to the opposite of the simplex category object created from `n`. This essentially asserts the naturality of the Dold-Kan correspondence.
More concisely: For any preadditive category C, any natural numbers q and n, and any morphism f between simplicial objects X and Y in C, the diagram commutes: P(f)(Ob(n)) ≅ Ob(P(n)) ∘ f, where Ob denotes the application of the opposite functor to the simplex category object.
|
AlgebraicTopology.DoldKan.Q_f_naturality
theorem AlgebraicTopology.DoldKan.Q_f_naturality :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
{X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n)))
((AlgebraicTopology.DoldKan.Q q).f n) =
CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n)
(f.app (Opposite.op (SimplexCategory.mk n)))
This theorem, `AlgebraicTopology.DoldKan.Q_f_naturality`, states that for any category `C` with preadditive structure, any simplicial objects `X` and `Y` in `C`, any natural number `q` and `n`, and any morphism `f` from `X` to `Y`, the composition of the morphism `f` applied to the opposite of the simplex category object created from `n`, with the `n`-th face map of the complement projection `Q` associated with `q`, is the same as the composition of the `n`-th face map of `Q` associated with `q`, with the morphism `f` applied to the opposite of the simplex category object created from `n`. This can be seen as a statement about the naturality of the complement projection `Q` in the category of simplicial objects.
More concisely: For any preadditive category `C`, simplicial objects `X` and `Y`, natural number `q`, and morphism `f` in `C`, the diagram commuting between `f`, `Q_n` and `Q_n'` (where `Q` is the complement projection of `q`, `Q_n` is the `n`-th face map of `Q`, and `Q_n'` is the `n`-th face map of the morphism `f` applied to the opposite simplex category object) commutes.
|
AlgebraicTopology.DoldKan.Q_f_0_eq
theorem AlgebraicTopology.DoldKan.Q_f_0_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q : ℕ), (AlgebraicTopology.DoldKan.Q q).f 0 = 0
This theorem states that for any natural number `q`, in a category `C` that is preadditive and has a defined category structure, and for any simplicial object `X` in `C`, the morphism `Q q` applied to the 0th degree equals to zero. The simplicial object is a contravariant functor from the category of finite nonempty ordered sets, and `Q q` is the complement projection associated to `P q` in the alternating face map complex of the simplicial object `X`. Essentially, this theorem is about a property of the Dold-Kan correspondence in algebraic topology, asserting that all the complement projections coincide with zero in degree zero.
More concisely: For any preadditive category `C` with a defined category structure, and for any simplicial object `X` in `C`, the complement projection associated to `P q` in the alternating face map complex of `X` is the zero morphism for all natural numbers `q` in degree 0.
|
AlgebraicTopology.DoldKan.P_f_idem
theorem AlgebraicTopology.DoldKan.P_f_idem :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q n : ℕ),
CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) ((AlgebraicTopology.DoldKan.P q).f n) =
(AlgebraicTopology.DoldKan.P q).f n
This theorem, named `AlgebraicTopology.DoldKan.P_f_idem`, states that for any category `C` of type `u_1` that also satisfies the `CategoryTheory.Category` and `CategoryTheory.Preadditive` conditions, and any simplicial object `X` in `C`, for any natural numbers `q` and `n`, the composition of the `n`-th morphism of the `q`-th Dold-Kan correspondence with itself is equal to the `n`-th morphism of the `q`-th Dold-Kan correspondence itself. In other words, the operation `f n` in the `q`-th Dold-Kan correspondence is idempotent when composed with itself.
More concisely: For any simplicial object X in a preadditive category C, the `n`-th morphism of the `q`-th Dold-Kan correspondence with itself is equal to the `n`-th morphism of the `q`-th Dold-Kan correspondence in C. (i.e., the `f n` operation is idempotent in the `q`-th Dold-Kan correspondence.)
|
AlgebraicTopology.DoldKan.Q_f_idem
theorem AlgebraicTopology.DoldKan.Q_f_idem :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q n : ℕ),
CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) ((AlgebraicTopology.DoldKan.Q q).f n) =
(AlgebraicTopology.DoldKan.Q q).f n
This theorem states that for any category `C` that is preadditive, and any simplicial object `X` in `C`, the morphism `Q q` in the Dold-Kan correspondence is idempotent for any natural numbers `q` and `n`, i.e., the composition of `Q q` with itself equals to `Q q`. In other words, applying the function `Q q` twice to the same input has the same effect as applying it once. This property is known as idempotence in category theory and algebraic topology.
More concisely: For any preadditive category `C` and simplicial object `X` in `C`, the morphism `Q q` in the Dold-Kan correspondence is idempotent, i.e., `Q q ∘ Q q = Q q`.
|
AlgebraicTopology.DoldKan.HigherFacesVanish.of_P
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_P :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q n : ℕ),
AlgebraicTopology.DoldKan.HigherFacesVanish q ((AlgebraicTopology.DoldKan.P q).f (n + 1))
This theorem, named `AlgebraicTopology.DoldKan.HigherFacesVanish.of_P` in Lean 4, asserts that for a given simplicial object `X` in a category `C` that is preadditive, the composition of two morphisms `(P q).f (n+1)` and `X.δ k`, which maps from `X _[n+1]` to `X _[n]`, vanishes when `k` is not equal to `0` and `k` is greater than or equal to `n-q+2`. This theorem is related to the Dold-Kan correspondence in algebraic topology, which establishes an equivalence between the category of chain complexes and the category of simplicial abelian groups.
More concisely: For a preadditive simplicial object `X` in a category `C`, the composition of the higher face morphism `X.δ` with the `q`-th face morphism `(P q).f` of its associated chain complex vanishes for `k > n - q + 1`.
|
AlgebraicTopology.DoldKan.P_f_0_eq
theorem AlgebraicTopology.DoldKan.P_f_0_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{X : CategoryTheory.SimplicialObject C} (q : ℕ),
(AlgebraicTopology.DoldKan.P q).f 0 =
CategoryTheory.CategoryStruct.id ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X 0)
The theorem `AlgebraicTopology.DoldKan.P_f_0_eq` asserts that for any simplicial object `X` in a category `C` (which is a category and preadditive), the morphism `f` at index 0 of the `P` functor applied to any natural number `q` is equivalent to the identity morphism acting on `X` at index 0 in the alternating face map complex. In other words, all the `P(q)` coincide with the identity morphism when evaluated at degree 0. The alternating face map complex is a chain complex constructed from the simplicial object.
More concisely: For any simplicial object X in a preadditive category C, the identity morphism at index 0 of the `P` functor's application to X coincides with the alternating face map at index 0 in the complex formed by the `P` functor.
|