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

theorem AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory} (i : Δ' ⟶ SimplexCategory.mk n) [hi : CategoryTheory.Mono i] (h₁ : Δ'.len ≠ n) (h₂ : ¬Isδ₀ i) : CategoryTheory.CategoryStruct.comp (PInfty.f n) (X.map i.op) = 0

theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] : CategoryTheory.CategoryStruct.comp (Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i) (PInfty.f Δ.len) = CategoryTheory.CategoryStruct.comp (PInfty.f Δ'.len) (X.map i.op)

theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] {Z : C} (h : (AlternatingFaceMapComplex.obj X).X Δ.len ⟶ Z) : CategoryTheory.CategoryStruct.comp (Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i) (CategoryTheory.CategoryStruct.comp (PInfty.f Δ.len) h) = CategoryTheory.CategoryStruct.comp (PInfty.f Δ'.len) (CategoryTheory.CategoryStruct.comp (X.map i.op) h)

def AlgebraicTopology.DoldKan.Γ₂N₁.natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : N₁.comp Γ₂ ⟶ CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)

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

Equations

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

@[simp]

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] (X : CategoryTheory.SimplicialObject C) (Δ : SimplexCategoryᵒᵖ) : (natTrans.app X).f.app Δ = (Γ₀.splitting (AlternatingFaceMapComplex.obj X)).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (PInfty.f (Opposite.unop A.fst).len) (X.map A.e.op)

def AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).comp (N₂.comp Γ₂) ≅ N₁.comp Γ₂

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

Equations

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

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) : Γ₂N₂ToKaroubiIso.inv.app X = Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X)

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) : Γ₂N₂ToKaroubiIso.hom.app X = Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X)

def AlgebraicTopology.DoldKan.Γ₂N₂.natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : N₂.comp Γ₂ ⟶ CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))

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

Equations

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

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)) : natTrans.app P = CategoryTheory.CategoryStruct.comp ((N₂.comp Γ₂).map P.decompId_i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp Γ₂N₂ToKaroubiIso.hom Γ₂N₁.natTrans).app P.X) P.decompId_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) : Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (Γ₂N₂ToKaroubiIso.app X).inv (Γ₂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 (N₂Γ₂.inv.app (N₂.obj P)) (N₂.map (Γ₂N₂.natTrans.app P)) = CategoryTheory.CategoryStruct.id (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 N₂ ◫ N₂Γ₂.inv) (CategoryTheory.CategoryStruct.comp (N₂.associator Γ₂ N₂).inv (Γ₂N₂.natTrans ◫ CategoryTheory.CategoryStruct.id N₂)) = CategoryTheory.CategoryStruct.id N₂

instance AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.IsIso Γ₂N₂.natTrans

instance AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.IsIso Γ₂N₁.natTrans

def AlgebraicTopology.DoldKan.Γ₂N₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) ≅ N₂.comp Γ₂

The unit isomorphism of the Dold-Kan equivalence.

Equations

• AlgebraicTopology.DoldKan.Γ₂N₂ = (CategoryTheory.asIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans).symm

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₂N₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : Γ₂N₂.inv = Γ₂N₂.natTrans

def AlgebraicTopology.DoldKan.Γ₂N₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C) ≅ N₁.comp Γ₂

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

Equations

• AlgebraicTopology.DoldKan.Γ₂N₁ = (CategoryTheory.asIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).symm

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₂N₁_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : Γ₂N₁.inv = Γ₂N₁.natTrans