# 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 (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} [] {n : } {Δ' : SimplexCategory} (i : ) [hi : ] (h₁ : Δ'.len n) (h₂ : ) :
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (X.map i.op) = 0
theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc {C : Type u_1} [] {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ Δ') {Z : C} (h : Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ.len) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ'.len) (CategoryTheory.CategoryStruct.comp (X.map i.op) h)
theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty {C : Type u_1} [] {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ Δ') :
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ.len) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ'.len) (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 Δ = Δ fun (A : ) => CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f A.fst.unop.len) (X.map A.e.op)
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₁.natTrans {C : Type u_1} [] :
AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso {C : Type u_1} [] :
(AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂) AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom.app X = AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X)
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.inv.app X = AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X)
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₂.natTrans {C : Type u_1} [] :
AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂).map P.decompId_i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app P.X) P.decompId_p)
theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.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 (AlgebraicTopology.DoldKan.N₂.associator 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.instIsIsoFunctorKaroubiSimplicialObjectNatTrans {C : Type u_1} [] :
CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
Equations
• =
instance AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans {C : Type u_1} [] :
CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
Equations
• =
@[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} [] :
AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂

The unit isomorphism of the Dold-Kan equivalence.

Equations
• AlgebraicTopology.DoldKan.Γ₂N₂ = (CategoryTheory.asIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans).symm
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} [] :
AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂

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

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