# Documentation

Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

# Split simplicial objects in preadditive categories #

In this file we define a functor nondegComplex : SimplicialObject.Split C ⥤ ChainComplex C ℕ when C is a preadditive category with finite coproducts, and get an isomorphism toKaroubiNondegComplexFunctorIsoN₁ : nondegComplex ⋙ toKaroubi _ ≅ forget C ⋙ DoldKan.N₁.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

noncomputable def SimplicialObject.Splitting.πSummand {C : Type u_1} [] (s : ) {Δ : } :

The projection on a summand of the coproduct decomposition given by a splitting of a simplicial object.

Instances For
@[simp]
theorem SimplicialObject.Splitting.ι_πSummand_eq_id_assoc {C : Type u_1} [] (s : ) {Δ : } {Z : C} (h : SimplicialObject.Splitting.N s (SimplexCategory.len A.fst.unop) Z) :
@[simp]
@[simp]
theorem SimplicialObject.Splitting.ι_πSummand_eq_zero_assoc {C : Type u_1} [] (s : ) {Δ : } (h : B A) {Z : C} (h : SimplicialObject.Splitting.N s (SimplexCategory.len B.fst.unop) Z) :
@[simp]
theorem SimplicialObject.Splitting.decomposition_id {C : Type u_1} [] (s : ) (Δ : ) :
CategoryTheory.CategoryStruct.id (X.obj Δ) = Finset.sum Finset.univ fun A =>
@[simp]
theorem SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc {C : Type u_1} [] (s : ) {n : } (i : Fin (n + 1)) {Z : C} (h : Z) :
@[simp]
theorem SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero {C : Type u_1} [] (s : ) {n : } (i : Fin (n + 1)) :
theorem SimplicialObject.Splitting.ιSummand_comp_PInfty_eq_zero {C : Type u_1} [] (s : ) {n : } :
CategoryTheory.CategoryStruct.comp () (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = 0

If a simplicial object X in an additive category is split, then PInfty vanishes on all the summands of X _[n] which do not correspond to the identity of [n].

theorem SimplicialObject.Splitting.comp_PInfty_eq_zero_iff {C : Type u_1} [] (s : ) {Z : C} {n : } (f : Z X.obj ()) :
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = 0
@[simp]
theorem SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc {C : Type u_1} [] (s : ) (n : ) {Z : C} (h : Z) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) () =
@[simp]
theorem SimplicialObject.Splitting.PInfty_comp_πSummand_id {C : Type u_1} [] (s : ) (n : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) () =
noncomputable def SimplicialObject.Splitting.d {C : Type u_1} [] (s : ) (i : ) (j : ) :

The differentials s.d i j : s.N i ⟶ s.N j on nondegenerate simplices of a split simplicial object are induced by the differentials on the alternating face map complex.

Instances For
@[simp]
theorem SimplicialObject.Splitting.nondegComplex_d {C : Type u_1} [] (s : ) (i : ) (j : ) :
@[simp]
theorem SimplicialObject.Splitting.nondegComplex_X {C : Type u_1} [] (s : ) :
noncomputable def SimplicialObject.Splitting.nondegComplex {C : Type u_1} [] (s : ) :

If s is a splitting of a simplicial object X in a preadditive category, s.nondeg_complex is a chain complex which is given in degree n by the nondegenerate n-simplices of X.

Instances For
@[simp]
noncomputable def SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ {C : Type u_1} [] (s : ) :
AlgebraicTopology.DoldKan.N₁.obj X

The chain complex s.nondegComplex attached to a splitting of a simplicial object X becomes isomorphic to the normalized Moore complex N₁.obj X defined as a formal direct factor in the category Karoubi (ChainComplex C ℕ).

Instances For
@[simp]
theorem SimplicialObject.Split.nondegComplexFunctor_map_f {C : Type u_1} [] {S₁ : } {S₂ : } (Φ : S₁ S₂) (n : ) :
HomologicalComplex.Hom.f (SimplicialObject.Split.nondegComplexFunctor.map Φ) n =
@[simp]
theorem SimplicialObject.Split.nondegComplexFunctor_obj {C : Type u_1} [] (S : ) :
SimplicialObject.Split.nondegComplexFunctor.obj S =
noncomputable def SimplicialObject.Split.nondegComplexFunctor {C : Type u_1} [] :

The functor which sends a split simplicial object in a preadditive category to the chain complex which consists of nondegenerate simplices.

Instances For
@[simp]
theorem SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f {C : Type u_1} [] (X : ) (n : ) :
HomologicalComplex.Hom.f (SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app X).f n =
@[simp]
theorem SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f {C : Type u_1} [] (X : ) (n : ) :
HomologicalComplex.Hom.f (SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.hom.app X).f n = CategoryTheory.CategoryStruct.comp () (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n)
noncomputable def SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ {C : Type u_1} [] :
CategoryTheory.Functor.comp SimplicialObject.Split.nondegComplexFunctor () CategoryTheory.Functor.comp () AlgebraicTopology.DoldKan.N₁

The natural isomorphism (in Karoubi (ChainComplex C ℕ)) between the chain complex of nondegenerate simplices of a split simplicial object and the normalized Moore complex defined as a formal direct factor of the alternating face map complex.

Instances For