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.)
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₁ : SimplexCategory.len Δ' ≠ n)
(h₂ : ¬AlgebraicTopology.DoldKan.Isδ₀ i)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (X.map i.op) = 0
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}
{Δ' : SimplexCategory}
(i : Δ ⟶ Δ')
[CategoryTheory.Mono i]
{Z : C}
(h : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) (SimplexCategory.len Δ) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i)
(CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len Δ)) h) = CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len Δ'))
(CategoryTheory.CategoryStruct.comp (X.map i.op) h)
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}
{Δ' : SimplexCategory}
(i : Δ ⟶ Δ')
[CategoryTheory.Mono i]
:
CategoryTheory.CategoryStruct.comp
(AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i)
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len Δ)) = CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len Δ')) (X.map i.op)
@[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ᵒᵖ)
:
(AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X).f.app Δ = SimplicialObject.Splitting.desc
(AlgebraicTopology.DoldKan.Γ₀.splitting (AlgebraicTopology.AlternatingFaceMapComplex.obj X)) Δ fun A =>
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len A.fst.unop))
(X.map (SimplicialObject.Splitting.IndexSet.e A).op)
@[irreducible]
def
AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂ ⟶ CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)
The natural transformation N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C).
Instances For
@[irreducible]
def
AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C))
(CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂
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]
def
AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂ ⟶ CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
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₂
instance
AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectInstCategorySimplicialObjectInstCategoryKaroubiCategoryCompChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownN₂Γ₂IdNatTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
instance
AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectInstCategorySimplicialObjectKaroubiInstCategoryKaroubiCategoryCompChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownN₁Γ₂ToKaroubiNatTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
CategoryTheory.IsIso 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
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)) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂
The unit isomorphism of the Dold-Kan equivalence.
Instances For
@[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
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) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂
The natural isomorphism toKaroubi (SimplicialObject C) ≅ N₁ ⋙ Γ₂.