THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. The Dold-Kan equivalence for additive categories.
This file defines preadditive.dold_kan.equivalence which is the equivalence
of categories karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ).
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
@[simp]
theorem
category_theory.preadditive.dold_kan.N_obj_X_X
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(P : category_theory.idempotents.karoubi (category_theory.simplicial_object C))
(n : ℕ) :
(category_theory.preadditive.dold_kan.N.obj P).X.X n = P.X.obj (opposite.op (simplex_category.mk n))
@[simp]
theorem
category_theory.preadditive.dold_kan.N_map_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(P Q : category_theory.idempotents.karoubi (category_theory.simplicial_object C))
(f : P ⟶ Q)
(i : ℕ) :
noncomputable
def
category_theory.preadditive.dold_kan.N
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C] :
The functor karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) of
the Dold-Kan equivalence for additive categories.
@[simp]
theorem
category_theory.preadditive.dold_kan.N_obj_X_d
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(P : category_theory.idempotents.karoubi (category_theory.simplicial_object C))
(i j : ℕ) :
@[simp]
theorem
category_theory.preadditive.dold_kan.N_obj_p_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(P : category_theory.idempotents.karoubi (category_theory.simplicial_object C))
(i : ℕ) :
@[simp]
theorem
category_theory.preadditive.dold_kan.Γ_obj_X_map
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(P : category_theory.idempotents.karoubi (chain_complex C ℕ))
(Δ Δ' : simplex_categoryᵒᵖ)
(θ : Δ ⟶ Δ') :
@[simp]
theorem
category_theory.preadditive.dold_kan.Γ_obj_p_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(P : category_theory.idempotents.karoubi (chain_complex C ℕ))
(Δ : simplex_categoryᵒᵖ) :
(category_theory.preadditive.dold_kan.Γ.obj P).p.app Δ = (algebraic_topology.dold_kan.Γ₀.splitting P.X).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), P.p.f (opposite.unop A.fst).len ≫ (algebraic_topology.dold_kan.Γ₀.splitting P.X).ι_summand A)
noncomputable
def
category_theory.preadditive.dold_kan.Γ
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The inverse functor karoubi (chain_complex C ℕ) ⥤ karoubi (simplicial_object C) of
the Dold-Kan equivalence for additive categories.
@[simp]
theorem
category_theory.preadditive.dold_kan.Γ_obj_X_obj
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(P : category_theory.idempotents.karoubi (chain_complex C ℕ))
(Δ : simplex_categoryᵒᵖ) :
@[simp]
theorem
category_theory.preadditive.dold_kan.Γ_map_f_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(P Q : category_theory.idempotents.karoubi (chain_complex C ℕ))
(f : P ⟶ Q)
(Δ : simplex_categoryᵒᵖ) :
(category_theory.preadditive.dold_kan.Γ.map f).f.app Δ = (algebraic_topology.dold_kan.Γ₀.splitting P.X).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), f.f.f (opposite.unop A.fst).len ≫ (algebraic_topology.dold_kan.Γ₀.splitting Q.X).ι_summand A)
@[simp]
@[simp]
@[simp]
noncomputable
def
category_theory.preadditive.dold_kan.equivalence
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The Dold-Kan equivalence karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)
for additive categories.
Equations
- category_theory.preadditive.dold_kan.equivalence = {functor := category_theory.preadditive.dold_kan.N _inst_2, inverse := category_theory.preadditive.dold_kan.Γ _inst_3, unit_iso := algebraic_topology.dold_kan.Γ₂N₂ _inst_3, counit_iso := algebraic_topology.dold_kan.N₂Γ₂ _inst_3, functor_unit_iso_comp' := _}
@[simp]