mathlib documentation

algebraic_topology.dold_kan.split_simplicial_object

Split simplicial objects in preadditive categories #

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₁.

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

Equations

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].

@[simp]

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

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

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

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

Equations

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