# mathlib3documentation

algebraic_topology.dold_kan.split_simplicial_object

# Split simplicial objects in preadditive categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define a functor nondeg_complex : simplicial_object.split C ⥤ chain_complex C ℕ when C is a preadditive category with finite coproducts, and get an isomorphism to_karoubi_nondeg_complex_iso_N₁ : nondeg_complex ⋙ to_karoubi _ ≅ forget C ⋙ dold_kan.N₁.

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

noncomputable def simplicial_object.splitting.π_summand {C : Type u_1} {Δ : simplex_categoryᵒᵖ}  :

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

Equations
@[simp]
@[simp]
theorem simplicial_object.splitting.ι_π_summand_eq_zero_assoc {C : Type u_1} {Δ : simplex_categoryᵒᵖ} (h : B A) {X' : C} (f' : s.N (opposite.unop B.fst).len X') :
s.ι_summand A s.π_summand B f' = 0 f'
@[simp]
theorem simplicial_object.splitting.σ_comp_π_summand_id_eq_zero_assoc {C : Type u_1} {n : } (i : fin (n + 1)) {X' : C} (f' : X') :
X.σ i = 0 f'
@[simp]
theorem simplicial_object.splitting.σ_comp_π_summand_id_eq_zero {C : Type u_1} {n : } (i : fin (n + 1)) :
X.σ i = 0

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

theorem simplicial_object.splitting.comp_P_infty_eq_zero_iff {C : Type u_1} {Z : C} {n : } (f : Z X.obj ) :
@[simp]
@[simp]
theorem simplicial_object.splitting.P_infty_comp_π_summand_id_assoc {C : Type u_1} (n : ) {X' : C} (f' : X') :
@[simp]
@[simp]
@[simp]
noncomputable def simplicial_object.splitting.d {C : Type u_1} (i j : ) :
s.N i s.N 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.

Equations
@[simp]
theorem simplicial_object.splitting.nondeg_complex_X {C : Type u_1} (ᾰ : ) :
s.nondeg_complex.X = s.N
noncomputable def simplicial_object.splitting.nondeg_complex {C : Type u_1}  :

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.

Equations
@[simp]
theorem simplicial_object.splitting.nondeg_complex_d {C : Type u_1} (i j : ) :
s.nondeg_complex.d i j = s.d i j

The chain complex s.nondeg_complex 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 (chain_complex C ℕ).

Equations
@[simp]
@[simp]
@[simp]
noncomputable def simplicial_object.split.nondeg_complex_functor {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.

Equations
@[simp]
theorem simplicial_object.split.nondeg_complex_functor_map_f {C : Type u_1} (S₁ S₂ : simplicial_object.split C) (Φ : S₁ S₂) (n : ) :
@[simp]
@[simp]

The natural isomorphism (in karoubi (chain_complex 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.

Equations