AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ) {θ : Δ ⟶ Δ'} {Δ'' : SimplexCategory} {e : Δ'.unop ⟶ Δ''}
{i : Δ'' ⟶ A.fst.unop} [inst_3 : CategoryTheory.Epi e] [inst_4 : CategoryTheory.Mono i],
CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A)
(AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) =
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
(CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ')
(SimplicialObject.Splitting.IndexSet.mk e))
This theorem states that in the context of algebraic topology and specifically within the Dold-Kan correspondence, for a chain complex `K` in a category `C` with finite coproducts and a given simplex category morphism `θ` from `Δ` to `Δ'`, if we have an epimorphism `e` from `Δ'.unop` to `Δ''` and a monomorphism `i` from `Δ''` to `A.fst.unop` such that the composition of `e` and `i` is equal to the composition of `θ.unop` and the epimorphism associated to `A`, then the composition of the b-th inclusion into the sigma object over `Γ₀.Obj.summand K Δ` and `Γ₀.Obj.map K θ` is equal to the composition of `Γ₀.Obj.Termwise.mapMono K i` and the b-th inclusion into the sigma object over `Γ₀.Obj.summand K Δ'` associated to the splitting index set created by `e`. This theorem essentially establishes a sort of commutative diagram involving these morphisms in the bigger picture of Dold-Kan correspondence.
More concisely: Given a chain complex `K` in a category `C` with finite coproducts, a simplex category morphism `θ` from `Δ` to `Δ'`, an epimorphism `e` from `Δ'.unop` to `Δ''`, and a monomorphism `i` from `Δ''` to `A.fst.unop`, if the composition of `e` and `i` is equal to the composition of `θ.unop` and the epimorphism associated to `A`, then the b-th inclusions into the sigma objects of `Γ₀.Obj.summand K Δ` and `Γ₀.Obj.summand K Δ'` are equal up to the composition of `Γ₀.Obj.Termwise.mapMono K i`.
|
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(K : ChainComplex C ℕ) (Δ : SimplexCategory),
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.id Δ) =
CategoryTheory.CategoryStruct.id (K.X Δ.len)
This theorem is a property of Dold-Kan correspondences in algebraic topology. It states that for any chain complex `K` indexed by natural numbers in a preadditive category `C`, and for any natural number `Δ` considered as an object in the simplex category, the termwise application of the monomorphism mapping function with respect to the identity morphism on `Δ` is equal to the identity morphism on the module `K.X` at the length of `Δ`. In other words, applying the morphism mapping function to the identity morphism does not change the module in the chain complex.
More concisely: For any chain complex `K` in a preadditive category `C` and natural number `Δ`, the termwise application of the monomorphism mapping function with respect to the identity morphism on `Δ` is equal to the identity morphism on `K.X` at length `Δ`.
|
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory} {e : Δ'.unop ⟶ Δ''}
{i : Δ'' ⟶ A.fst.unop} [inst_3 : CategoryTheory.Epi e] [inst_4 : CategoryTheory.Mono i],
CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A)
((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) =
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
(((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (SimplicialObject.Splitting.IndexSet.mk e))
The theorem `AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand` states that for a given chain complex `K` in a category `C` with finite coproducts, and given elements of the simplex category and their morphisms such that the composition `e i` is equal to the composition `θ.unop (SimplicialObject.Splitting.IndexSet.e A)`, the composition of the "injection" into the cofan and the map `θ` in the Dold-Kan correspondence is equal to the composition of the termwise mapping of a monomorphism `i` and the "injection" into the cofan associated to the epimorphism `e`.
In simpler terms, this theorem is about the relationship between certain composed morphisms in a category theory context, especially in the context of homological algebra and algebraic topology. It's dealing with the consistency of different paths in a diagram in the category, a fundamental idea in category theory.
More concisely: Given a chain complex in a category with finite coproducts, the map from the termwise application of a monomorphism to the cofan and the map from the cofan associated to an epimorphism, both in the context of the Dold-Kan correspondence, are equal when their compositions with specific simplices and morphisms satisfy a given condition.
|