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

theorem AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero {C : Type u_1} [] {n : } {Δ' : SimplexCategory} (i : ) [hi : ] (h₁ : ) (h₂ : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (X.map i.op) = 0
theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty {C : Type u_1} [] {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ Δ') :
CategoryTheory.CategoryStruct.comp () (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty ()) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty ()) (X.map i.op)
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app {C : Type u_1} [] (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X).f.app Δ = SimplicialObject.Splitting.desc () Δ fun A => CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty (SimplexCategory.len A.fst.unop)) (X.map )
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₁.natTrans {C : Type u_1} [] :
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂

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

Instances For
@[irreducible]
def AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂ {C : Type u_1} [] :
CategoryTheory.Functor.comp () (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} [] :
AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.hom.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp () (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} [] :
AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.inv.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂).obj X = (CategoryTheory.Functor.comp () (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂)).obj X)
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₂.natTrans {C : Type u_1} [] :
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂

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

Instances For
theorem AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂).map ()) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.hom AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app P.X) ())
theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂.app X).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app ())
theorem AlgebraicTopology.DoldKan.identity_N₂_objectwise {C : Type u_1} [] :
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.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} [] :
AlgebraicTopology.DoldKan.Γ₂N₂.inv = AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
def AlgebraicTopology.DoldKan.Γ₂N₂ {C : Type u_1} [] :
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} [] :
AlgebraicTopology.DoldKan.Γ₂N₁.inv = AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
def AlgebraicTopology.DoldKan.Γ₂N₁ {C : Type u_1} [] :
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂

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

Instances For