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

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

Equations
Instances For

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

    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
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      Instances For

        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 ℕ).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem SimplicialObject.Split.nondegComplexFunctor_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ : S₁ S₂) (n : ) :
          (SimplicialObject.Split.nondegComplexFunctor.map Φ).f n = Φ.f n

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For