AlgebraicTopology.inclusionOfMooreComplexMap_f
theorem AlgebraicTopology.inclusionOfMooreComplexMap_f :
∀ {A : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} A] [inst_1 : CategoryTheory.Abelian A]
(X : CategoryTheory.SimplicialObject A) (n : ℕ),
(AlgebraicTopology.inclusionOfMooreComplexMap X).f n =
(AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow
This theorem, `AlgebraicTopology.inclusionOfMooreComplexMap_f`, states that for any category `A` having a category theory structure and an Abelian structure, and for any simplicial object `X` in `A` and any natural number `n`, the `n`-th component of the functor `AlgebraicTopology.inclusionOfMooreComplexMap` applied to `X` is equal to the arrow from the `n`-th object of the Normalized Moore Complex of `X` to its ambient object in the category `A`. The Normalized Moore Complex and its `n`-th object `objX` form part of a construction in algebraic topology involving simplicial objects and Abelian categories, where the arrow represents a specific morphism in the category `A`.
More concisely: For any simplicial object X in an Abelian category A with a category structure, the n-th component of the inclusion of Moore Complex functor equals the morphism from the n-th object of X's Normalized Moore Complex to X in A.
|
AlgebraicTopology.AlternatingFaceMapComplex.d_squared
theorem AlgebraicTopology.AlternatingFaceMapComplex.d_squared :
∀ {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.AlternatingFaceMapComplex.objD X (n + 1))
(AlgebraicTopology.AlternatingFaceMapComplex.objD X n) =
0
This theorem, named `AlgebraicTopology.AlternatingFaceMapComplex.d_squared`, is a statement about the chain complex relation `d ≫ d` in algebraic topology. It states that for any category `C` with preadditive structure, and any simplicial object `X` in `C`, the composition of the differentials (the face maps of the alternating face map complex) `objD` at levels `n+1` and `n` is equal to zero. This satisfies the property that the composition of the boundary maps in a chain complex is zero, often written as `d^2 = 0` in mathematical notation.
More concisely: For any simplicial object `X` in a preadditive category `C`, the composition of the face maps `d` of the alternating face map complex of `X` at levels `n+1` and `n` is zero: `objD(n+1) ∘ objD(n) = 0`.
|