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
      • s.nondegComplex = { X := s.N, d := s.d, shape := , d_comp_d' := }
      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

          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
            @[simp]
            theorem SimplicialObject.Split.nondegComplexFunctor_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ S₂ : SimplicialObject.Split C} (Φ : S₁ S₂) (n : ) :
            (SimplicialObject.Split.nondegComplexFunctor.map Φ).f n = Φ.f n
            @[simp]
            theorem SimplicialObject.Split.nondegComplexFunctor_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S : SimplicialObject.Split C) :
            SimplicialObject.Split.nondegComplexFunctor.obj S = S.s.nondegComplex
            noncomputable def SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
            SimplicialObject.Split.nondegComplexFunctor.comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex C )) (SimplicialObject.Split.forget C).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.

            Equations
            Instances For
              @[simp]
              @[simp]
              theorem SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : SimplicialObject.Split C) (n : ) :
              (SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.hom.app X).f.f n = CategoryTheory.CategoryStruct.comp ((X.s.cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))) (AlgebraicTopology.DoldKan.PInfty.f n)