Documentation

Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Construction of the inverse functor of the Dold-Kan equivalence #

In this file, we construct the functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C which shall be the inverse functor of the Dold-Kan equivalence in the case of abelian categories, and more generally pseudoabelian categories.

By definition, when K is a chain_complex, Γ₀.obj K is a simplicial object which sends Δ : SimplexCategoryᵒᵖ to a certain coproduct indexed by the set Splitting.IndexSet Δ whose elements consists of epimorphisms e : Δ.unop ⟶ Δ'.unop (with Δ' : SimplexCategoryᵒᵖ); the summand attached to such an e is K.X Δ'.unop.len. By construction, Γ₀.obj K is a split simplicial object whose splitting is Γ₀.splitting K.

We also construct Γ₂ : Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C) which shall be an equivalence for any additive category C.

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

Isδ₀ i is a simple condition used to check whether a monomorphism i in SimplexCategory identifies to the coface map δ 0.

Equations
Instances For

    In the definition of (Γ₀.obj K).obj Δ as a direct sum indexed by A : Splitting.IndexSet Δ, the summand summand K Δ A is K.X A.1.len.

    Equations
    Instances For

      The functor Γ₀ sends a chain complex K to the simplicial object which sends Δ to the direct sum of the objects summand K Δ A for all A : Splitting.IndexSet Δ

      Equations
      Instances For

        A monomorphism i : Δ' ⟶ Δ induces a morphism K.X Δ.len ⟶ K.X Δ'.len which is the identity if Δ = Δ', the differential on the complex K if i = δ 0, and zero otherwise.

        Equations
        Instances For

          The simplicial morphism on the simplicial object Γ₀.obj K induced by a morphism Δ' → Δ in SimplexCategory is defined on each summand associated to an A : Splitting.IndexSet Δ in terms of the epi-mono factorisation of θ ≫ A.e.

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

            The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on objects.

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

              By construction, the simplicial Γ₀.obj K is equipped with a splitting.

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

                The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on morphisms.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem AlgebraicTopology.DoldKan.Γ₀'_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {K : ChainComplex C } {K' : ChainComplex C } (f : K K') (i : ) :
                  (AlgebraicTopology.DoldKan.Γ₀'.map f).f i = f.f i

                  The functor Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C that induces Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which shall be the inverse functor of the Dold-Kan equivalence for abelian or pseudo-abelian categories.

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

                    The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which is the inverse functor of the Dold-Kan equivalence when C is an abelian category, or more generally a pseudoabelian category.

                    Equations
                    Instances For

                      The extension of Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C on the idempotent completions. It shall be an equivalence of categories for any additive category C.

                      Equations
                      Instances For