Documentation

Mathlib.AlgebraicTopology.DoldKan.FunctorN

Construction of functors N for the Dold-Kan correspondence #

In this file, we construct functors N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) for any preadditive category C. (The indices of these functors are the number of occurrences of Karoubi at the source or the target.)

In the case C is additive, the functor N₂ shall be the functor of the equivalence CategoryTheory.Preadditive.DoldKan.equivalence defined in EquivalenceAdditive.lean.

In the case the category C is pseudoabelian, the composition of N₁ with the inverse of the equivalence ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ) will be the functor CategoryTheory.Idempotents.DoldKan.N of the equivalence of categories CategoryTheory.Idempotents.DoldKan.equivalence : SimplicialObject C ≌ ChainComplex C ℕ defined in EquivalencePseudoabelian.lean.

When the category C is abelian, a relation between N₁ and the normalized Moore complex functor shall be obtained in Normalized.lean.

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

source
@[simp]
theorem AlgebraicTopology.DoldKan.N₁_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.DoldKan.N₁.toPrefunctor.map f).f = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (AlgebraicTopology.AlternatingFaceMapComplex.map f)
source
@[simp]
theorem AlgebraicTopology.DoldKan.N₁_obj_p {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) :
(AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj X).p = AlgebraicTopology.DoldKan.PInfty
source
@[simp]
theorem AlgebraicTopology.DoldKan.N₁_obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) :
(AlgebraicTopology.DoldKan.N₁.toPrefunctor.obj X).X = AlgebraicTopology.AlternatingFaceMapComplex.obj X
source
def AlgebraicTopology.DoldKan.N₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))

The functor SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) which maps X to the formal direct factor of K[X] defined by PInfty.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.N₂_map_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
    ∀ {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (f : X ⟶ Y) (i : ℕ), (AlgebraicTopology.DoldKan.N₂.toPrefunctor.map f).f.f i = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i) (f.f.app (Opposite.op (SimplexCategory.mk i)))
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.N₂_obj_p_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (i : ℕ) :
    (AlgebraicTopology.DoldKan.N₂.toPrefunctor.obj P).p.f i = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i) (P.p.app (Opposite.op (SimplexCategory.mk i)))
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.N₂_obj_X_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (n : ℕ) :
    (AlgebraicTopology.DoldKan.N₂.toPrefunctor.obj P).X.X n = P.X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.N₂_obj_X_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (i : ℕ) (j : ℕ) :
    (AlgebraicTopology.DoldKan.N₂.toPrefunctor.obj P).X.d i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : P.X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk i)) = P.X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (j + 1))))) (Finset.sum Finset.univ fun (i : Fin (j + 2)) => (-1) ^ ↑i • CategoryTheory.SimplicialObject.δ P.X i) else 0
    source
    def AlgebraicTopology.DoldKan.N₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
    CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))

    The extension of N₁ to the Karoubi envelope of SimplicialObject C.

    Equations
    Instances For
      source
      def AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
      CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)) AlgebraicTopology.DoldKan.N₂ ≅ AlgebraicTopology.DoldKan.N₁

      The canonical isomorphism toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) :
        (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) :
        (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X).f = AlgebraicTopology.DoldKan.PInfty