Documentation

Mathlib.AlgebraicTopology.DoldKan.NCompGamma

The unit isomorphism of the Dold-Kan equivalence

In order to construct the unit isomorphism of the Dold-Kan equivalence, we first construct natural transformations Γ₂N₁.natTrans : N₁ ⋙ Γ₂ ⟶ toKaroubi (simplicial_object C) and Γ₂N₂.natTrans : N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C). It is then shown that Γ₂N₂.natTrans is an isomorphism by using that it becomes an isomorphism after the application of the functor N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) which reflects isomorphisms.

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

@[irreducible]

The natural transformation N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C).

Instances For
    @[irreducible]

    The compatibility isomorphism relating N₂ ⋙ Γ₂ and N₁ ⋙ Γ₂.

    Instances For
      theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
      AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.hom.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)) (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂)).obj X = (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂).obj X)
      theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
      AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.inv.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂).obj X = (CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)) (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂)).obj X)
      @[irreducible]

      The natural transformation N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C).

      Instances For
        theorem AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) :
        AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂).map (CategoryTheory.Idempotents.Karoubi.decompId_i P)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.hom AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app P.X) (CategoryTheory.Idempotents.Karoubi.decompId_p P))
        theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
        AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.app X).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app ((CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).obj X))
        theorem AlgebraicTopology.DoldKan.identity_N₂_objectwise {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) :
        CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.N₂Γ₂.inv.app (AlgebraicTopology.DoldKan.N₂.obj P)) (AlgebraicTopology.DoldKan.N₂.map (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P)) = CategoryTheory.CategoryStruct.id (AlgebraicTopology.DoldKan.N₂.obj P)
        theorem AlgebraicTopology.DoldKan.identity_N₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.N₂Γ₂.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.N₂).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂)) = CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂
        @[simp]
        theorem AlgebraicTopology.DoldKan.Γ₂N₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        AlgebraicTopology.DoldKan.Γ₂N₂.inv = AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
        @[simp]
        theorem AlgebraicTopology.DoldKan.Γ₂N₁_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        AlgebraicTopology.DoldKan.Γ₂N₁.inv = AlgebraicTopology.DoldKan.Γ₂N₁.natTrans

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

        Instances For