algebraic_topology.dold_kan.equivalence_additive

@[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))

source

@[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 : ℕ) :

(category_theory.preadditive.dold_kan.N.map f).f.f i = algebraic_topology.dold_kan.P_infty.f i ≫ f.f.app (opposite.op (simplex_category.mk i))

source

noncomputable def category_theory.preadditive.dold_kan.N {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :

category_theory.idempotents.karoubi (category_theory.simplicial_object C) ⥤ category_theory.idempotents.karoubi (chain_complex C ℕ)

The functor karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) of the Dold-Kan equivalence for additive categories.

Equations

category_theory.preadditive.dold_kan.N = algebraic_topology.dold_kan.N₂

source

@[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 : ℕ) :

(category_theory.preadditive.dold_kan.N.obj P).X.d i j = dite (i = j + 1) (λ (h : i = j + 1), category_theory.eq_to_hom _ ≫ finset.univ.sum (λ (i : fin (j + 2)), (-1) ^ ↑i • P.X.δ i)) (λ (h : ¬i = j + 1), 0)

source

@[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 : ℕ) :

(category_theory.preadditive.dold_kan.N.obj P).p.f i = algebraic_topology.dold_kan.P_infty.f i ≫ P.p.app (opposite.op (simplex_category.mk i))

source

@[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 ᵒᵖ) (θ : Δ ⟶ Δ') :

(category_theory.preadditive.dold_kan.Γ.obj P).X.map θ = algebraic_topology.dold_kan.Γ₀.obj.map P.X θ

source

@[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)

source

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] :

category_theory.idempotents.karoubi (chain_complex C ℕ) ⥤ category_theory.idempotents.karoubi (category_theory.simplicial_object C)

The inverse functor karoubi (chain_complex C ℕ) ⥤ karoubi (simplicial_object C) of the Dold-Kan equivalence for additive categories.

Equations

category_theory.preadditive.dold_kan.Γ = algebraic_topology.dold_kan.Γ₂

source

@[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 ᵒᵖ) :

(category_theory.preadditive.dold_kan.Γ.obj P).X.obj Δ = algebraic_topology.dold_kan.Γ₀.obj.obj₂ P.X Δ

source

@[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)

source

@[simp]

theorem category_theory.preadditive.dold_kan.equivalence_unit_iso {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :

category_theory.preadditive.dold_kan.equivalence.unit_iso = algebraic_topology.dold_kan.Γ₂N₂

source

@[simp]

theorem category_theory.preadditive.dold_kan.equivalence_counit_iso {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :

category_theory.preadditive.dold_kan.equivalence.counit_iso = algebraic_topology.dold_kan.N₂Γ₂

source

@[simp]

theorem category_theory.preadditive.dold_kan.equivalence_functor {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :

category_theory.preadditive.dold_kan.equivalence.functor = category_theory.preadditive.dold_kan.N

source

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] :

category_theory.idempotents.karoubi (category_theory.simplicial_object C) ≌ category_theory.idempotents.karoubi (chain_complex 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' := _}

source

@[simp]

theorem category_theory.preadditive.dold_kan.equivalence_inverse {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_coproducts C] :

category_theory.preadditive.dold_kan.equivalence.inverse = category_theory.preadditive.dold_kan.Γ