mathlib3 documentation

algebraic_topology.dold_kan.gamma_comp_n

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 ℕ)).

(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

source
@[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 : ℕ) :
(algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso K).inv.f i = 𝟙 ((algebraic_topology.dold_kan.Γ₀.splitting K).N i)
source
@[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 : ℕ) :
(algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso K).hom.f i = 𝟙 ((algebraic_topology.dold_kan.Γ₀.splitting K).N i)
source
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 ℕ) :
(algebraic_topology.dold_kan.Γ₀.splitting K).nondeg_complex ≅ K

The isomorphism (Γ₀.splitting K).nondeg_complex ≅ K for all K : chain_complex C ℕ.

Equations
source
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] :
algebraic_topology.dold_kan.Γ₀' ⋙ simplicial_object.split.nondeg_complex_functor ≅ 𝟭 (chain_complex C ℕ)

The natural isomorphism (Γ₀.splitting K).nondeg_complex ≅ K for K : chain_complex C ℕ.

Equations
source
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] :
algebraic_topology.dold_kan.Γ₀ ⋙ algebraic_topology.dold_kan.N₁ ≅ category_theory.idempotents.to_karoubi (chain_complex C ℕ)

The natural isomorphism Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ).

Equations
source
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 ℕ) :
algebraic_topology.dold_kan.N₁Γ₀.app K = (algebraic_topology.dold_kan.Γ₀.splitting K).to_karoubi_nondeg_complex_iso_N₁.symm ≪≫ (category_theory.idempotents.to_karoubi (chain_complex C ℕ)).map_iso (algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso K)
source
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 ℕ) :
algebraic_topology.dold_kan.N₁Γ₀.hom.app K = (algebraic_topology.dold_kan.Γ₀.splitting K).to_karoubi_nondeg_complex_iso_N₁.inv ≫ (category_theory.idempotents.to_karoubi (chain_complex C ℕ)).map (algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso K).hom
source
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 ℕ) :
algebraic_topology.dold_kan.N₁Γ₀.inv.app K = (category_theory.idempotents.to_karoubi (chain_complex C ℕ)).map (algebraic_topology.dold_kan.Γ₀_nondeg_complex_iso K).inv ≫ (algebraic_topology.dold_kan.Γ₀.splitting K).to_karoubi_nondeg_complex_iso_N₁.hom
source
@[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 : ℕ) :
(algebraic_topology.dold_kan.N₁Γ₀.hom.app K).f.f n = (algebraic_topology.dold_kan.Γ₀.splitting K).to_karoubi_nondeg_complex_iso_N₁.inv.f.f n
source
@[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 : ℕ) :
(algebraic_topology.dold_kan.N₁Γ₀.inv.app K).f.f n = (algebraic_topology.dold_kan.Γ₀.splitting K).to_karoubi_nondeg_complex_iso_N₁.hom.f.f n
source
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] :
category_theory.idempotents.to_karoubi (chain_complex C ℕ) ⋙ algebraic_topology.dold_kan.Γ₂ ⋙ algebraic_topology.dold_kan.N₂ = algebraic_topology.dold_kan.Γ₀ ⋙ algebraic_topology.dold_kan.N₁
source
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] :
category_theory.idempotents.to_karoubi (chain_complex C ℕ) ⋙ algebraic_topology.dold_kan.Γ₂ ⋙ algebraic_topology.dold_kan.N₂ ≅ algebraic_topology.dold_kan.Γ₀ ⋙ algebraic_topology.dold_kan.N₁

Compatibility isomorphism between to_karoubi _ ⋙ Γ₂ ⋙ N₂ and Γ₀ ⋙ N₁ which are functors chain_complex C ℕ ⥤ karoubi (chain_complex C ℕ).

Equations
source
@[simp]
theorem algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :
algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso.inv = category_theory.eq_to_hom _
source
@[simp]
theorem algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :
algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso.hom = category_theory.eq_to_hom algebraic_topology.dold_kan.N₂Γ₂_to_karoubi
source
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] :
algebraic_topology.dold_kan.Γ₂ ⋙ algebraic_topology.dold_kan.N₂ ≅ 𝟭 (category_theory.idempotents.karoubi (chain_complex C ℕ))

The counit isomorphism of the Dold-Kan equivalence for additive categories.

Equations
source
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 ℕ) :
algebraic_topology.dold_kan.N₂Γ₂.hom.app ((category_theory.idempotents.to_karoubi (chain_complex C ℕ)).obj K) = algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso.hom.app K ≫ algebraic_topology.dold_kan.N₁Γ₀.hom.app K
source
@[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 : ℕ) :
(algebraic_topology.dold_kan.N₂Γ₂.inv.app X).f.f n = X.p.f n ≫ (algebraic_topology.dold_kan.Γ₀.splitting X.X).ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n)))