The counit isomorphism of the Dold-Kan equivalence
The purpose of this file is to construct natural isomorphisms
N₁Γ₀ : Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ)
and N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (karoubi (chain_complex C ℕ))
.
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso_inv_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(i : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso_hom_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(i : ℕ) :
noncomputable
def
algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
The isomorphism (Γ₀.splitting K).nondeg_complex ≅ K
for all K : chain_complex C ℕ
.
noncomputable
def
algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The natural isomorphism (Γ₀.splitting K).nondeg_complex ≅ K
for K : chain_complex C ℕ
.
Equations
- algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor = category_theory.nat_iso.of_components algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor._proof_1
noncomputable
def
algebraic_topology.dold_kan.N₁Γ₀
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The natural isomorphism Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ)
.
Equations
- algebraic_topology.dold_kan.N₁Γ₀ = (((algebraic_topology.dold_kan.Γ₀'.associator (simplicial_object.split.forget C) algebraic_topology.dold_kan.N₁ ≪≫ category_theory.iso_whisker_left algebraic_topology.dold_kan.Γ₀' simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁.symm) ≪≫ (algebraic_topology.dold_kan.Γ₀'.associator simplicial_object.split.nondeg_complex_functor (category_theory.idempotents.to_karoubi (chain_complex C ℕ))).symm) ≪≫ category_theory.iso_whisker_right algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor (category_theory.idempotents.to_karoubi (chain_complex C ℕ))) ≪≫ (category_theory.idempotents.to_karoubi (chain_complex C ℕ)).left_unitor
theorem
algebraic_topology.dold_kan.N₁Γ₀_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
theorem
algebraic_topology.dold_kan.N₁Γ₀_hom_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
theorem
algebraic_topology.dold_kan.N₁Γ₀_inv_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.N₁Γ₀_hom_app_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.N₁Γ₀_inv_app_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(n : ℕ) :
theorem
algebraic_topology.dold_kan.N₂Γ₂_to_karoubi
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
noncomputable
def
algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
Compatibility isomorphism between to_karoubi _ ⋙ Γ₂ ⋙ N₂
and Γ₀ ⋙ N₁
which
are functors chain_complex C ℕ ⥤ karoubi (chain_complex C ℕ)
.
@[simp]
noncomputable
def
algebraic_topology.dold_kan.N₂Γ₂
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The counit isomorphism of the Dold-Kan equivalence for additive categories.
Equations
- algebraic_topology.dold_kan.N₂Γ₂ = ((category_theory.whiskering_left (chain_complex C ℕ) (category_theory.idempotents.karoubi (chain_complex C ℕ)) (category_theory.idempotents.karoubi (chain_complex C ℕ))).obj (category_theory.idempotents.to_karoubi (chain_complex C ℕ))).preimage_iso (algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso ≪≫ algebraic_topology.dold_kan.N₁Γ₀)
theorem
algebraic_topology.dold_kan.N₂Γ₂_compatible_with_N₁Γ₀
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.N₂Γ₂_inv_app_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : category_theory.idempotents.karoubi (chain_complex C ℕ))
(n : ℕ) :