Construction of the inverse functor of the Dold-Kan equivalence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we construct the functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C
which shall be the inverse functor of the Dold-Kan equivalence in the case of abelian categories,
and more generally pseudoabelian categories.
By definition, when K is a chain_complex, Γ₀.obj K is a simplicial object which
sends Δ : simplex_categoryᵒᵖ to a certain coproduct indexed by the set
splitting.index_set Δ whose elements consists of epimorphisms e : Δ.unop ⟶ Δ'.unop
(with Δ' : simplex_categoryᵒᵖ); the summand attached to such an e is K.X Δ'.unop.len.
By construction, Γ₀.obj K is a split simplicial object whose splitting is Γ₀.splitting K.
We also construct Γ₂ : karoubi (chain_complex C ℕ) ⥤ karoubi (simplicial_object C)
which shall be an equivalence for any additive category C.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
@[nolint]
def
algebraic_topology.dold_kan.is_δ₀
{Δ Δ' : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i] :
Prop
is_δ₀ i is a simple condition used to check whether a monomorphism i in
simplex_category identifies to the coface map δ 0.
Equations
- algebraic_topology.dold_kan.is_δ₀ i = (Δ.len = Δ'.len + 1 ∧ ⇑(simplex_category.hom.to_order_hom i) 0 ≠ 0)
theorem
algebraic_topology.dold_kan.is_δ₀.eq_δ₀
{n : ℕ}
{i : simplex_category.mk n ⟶ simplex_category.mk (n + 1)}
[category_theory.mono i]
(hi : algebraic_topology.dold_kan.is_δ₀ i) :
i = simplex_category.δ 0
def
algebraic_topology.dold_kan.Γ₀.obj.summand
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
(Δ : simplex_categoryᵒᵖ)
(A : simplicial_object.splitting.index_set Δ) :
C
In the definition of (Γ₀.obj K).obj Δ as a direct sum indexed by A : splitting.index_set Δ,
the summand summand K Δ A is K.X A.1.len.
Equations
- algebraic_topology.dold_kan.Γ₀.obj.summand K Δ A = K.X (opposite.unop A.fst).len
noncomputable
def
algebraic_topology.dold_kan.Γ₀.obj.obj₂
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
(Δ : simplex_categoryᵒᵖ)
[category_theory.limits.has_finite_coproducts C] :
C
The functor Γ₀ sends a chain complex K to the simplicial object which
sends Δ to the direct sum of the objects summand K Δ A for all A : splitting.index_set Δ
Equations
noncomputable
def
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i] :
A monomorphism i : Δ' ⟶ Δ induces a morphism K.X Δ.len ⟶ K.X Δ'.len which
is the identity if Δ = Δ', the differential on the complex K if i = δ 0, and
zero otherwise.
Equations
- algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i = dite (Δ = Δ') (λ (h : Δ = Δ'), category_theory.eq_to_hom _) (λ (h : ¬Δ = Δ'), dite (algebraic_topology.dold_kan.is_δ₀ i) (λ (h : algebraic_topology.dold_kan.is_δ₀ i), K.d Δ.len Δ'.len) (λ (h : ¬algebraic_topology.dold_kan.is_δ₀ i), 0))
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
(Δ : simplex_category) :
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_δ₀'
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i]
(hi : algebraic_topology.dold_kan.is_δ₀ i) :
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i = K.d Δ.len Δ'.len
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_δ₀
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{n : ℕ} :
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K (simplex_category.δ 0) = K.d (n + 1) n
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i]
(h₁ : Δ ≠ Δ')
(h₂ : ¬algebraic_topology.dold_kan.is_δ₀ i) :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{K K' : chain_complex C ℕ}
(f : K ⟶ K')
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i] :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{K K' : chain_complex C ℕ}
(f : K ⟶ K')
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i]
{X' : C}
(f' : K'.X Δ'.len ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_comp_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{Δ'' Δ' Δ : simplex_category}
(i' : Δ'' ⟶ Δ')
[category_theory.mono i']
(i : Δ' ⟶ Δ)
[category_theory.mono i]
{X' : C}
(f' : K.X Δ''.len ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_comp
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
{Δ'' Δ' Δ : simplex_category}
(i' : Δ'' ⟶ Δ')
[category_theory.mono i']
(i : Δ' ⟶ Δ)
[category_theory.mono i] :
noncomputable
def
algebraic_topology.dold_kan.Γ₀.obj.map
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
{Δ' Δ : simplex_categoryᵒᵖ}
(θ : Δ ⟶ Δ') :
The simplicial morphism on the simplicial object Γ₀.obj K induced by
a morphism Δ' → Δ in simplex_category is defined on each summand
associated to an A : Γ_index_set Δ in terms of the epi-mono factorisation
of θ ≫ A.e.
Equations
- algebraic_topology.dold_kan.Γ₀.obj.map K θ = category_theory.limits.sigma.desc (λ (A : simplicial_object.splitting.index_set Δ), algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K (category_theory.limits.image.ι (θ.unop ≫ A.e)) ≫ category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ') (A.pull θ))
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{θ : Δ ⟶ Δ'}
{Δ'' : simplex_category}
{e : opposite.unop Δ' ⟶ Δ''}
{i : Δ'' ⟶ opposite.unop A.fst}
[category_theory.epi e]
[category_theory.mono i]
(fac : e ≫ i = θ.unop ≫ A.e)
{X' : C}
(f' : algebraic_topology.dold_kan.Γ₀.obj.obj₂ K Δ' ⟶ X') :
category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ) A ≫ algebraic_topology.dold_kan.Γ₀.obj.map K θ ≫ f' = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i ≫ category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ') (simplicial_object.splitting.index_set.mk e) ≫ f'
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{θ : Δ ⟶ Δ'}
{Δ'' : simplex_category}
{e : opposite.unop Δ' ⟶ Δ''}
{i : Δ'' ⟶ opposite.unop A.fst}
[category_theory.epi e]
[category_theory.mono i]
(fac : e ≫ i = θ.unop ≫ A.e) :
category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ) A ≫ algebraic_topology.dold_kan.Γ₀.obj.map K θ = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i ≫ category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ') (simplicial_object.splitting.index_set.mk e)
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀'
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ') :
category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ) A ≫ algebraic_topology.dold_kan.Γ₀.obj.map K θ = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K (category_theory.limits.image.ι (θ.unop ≫ A.e)) ≫ category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ') (A.pull θ)
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀'_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ')
{X' : C}
(f' : algebraic_topology.dold_kan.Γ₀.obj.obj₂ K Δ' ⟶ X') :
category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ) A ≫ algebraic_topology.dold_kan.Γ₀.obj.map K θ ≫ f' = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K (category_theory.limits.image.ι (θ.unop ≫ A.e)) ≫ category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K Δ') (A.pull θ) ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj_map
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(Δ Δ' : simplex_categoryᵒᵖ)
(θ : Δ ⟶ Δ') :
noncomputable
def
algebraic_topology.dold_kan.Γ₀.obj
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
The functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, on objects.
Equations
- algebraic_topology.dold_kan.Γ₀.obj K = {obj := λ (Δ : simplex_categoryᵒᵖ), algebraic_topology.dold_kan.Γ₀.obj.obj₂ K Δ, map := λ (Δ Δ' : simplex_categoryᵒᵖ) (θ : Δ ⟶ Δ'), algebraic_topology.dold_kan.Γ₀.obj.map K θ, map_id' := _, map_comp' := _}
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.obj_obj
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
(Δ : simplex_categoryᵒᵖ) :
theorem
algebraic_topology.dold_kan.Γ₀.splitting_map_eq_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
(Δ : simplex_categoryᵒᵖ) :
simplicial_object.splitting.map (algebraic_topology.dold_kan.Γ₀.obj K) (λ (n : ℕ), category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K (opposite.op (simplex_category.mk n))) (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n)))) Δ = 𝟙 (simplicial_object.splitting.coprod (λ (n : ℕ), algebraic_topology.dold_kan.Γ₀.obj.summand K (opposite.op (simplex_category.mk n)) (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n)))) Δ)
noncomputable
def
algebraic_topology.dold_kan.Γ₀.splitting
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
By construction, the simplicial Γ₀.obj K is equipped with a splitting.
Equations
- algebraic_topology.dold_kan.Γ₀.splitting K = {N := λ (n : ℕ), K.X n, ι := λ (n : ℕ), category_theory.limits.sigma.ι (algebraic_topology.dold_kan.Γ₀.obj.summand K (opposite.op (simplex_category.mk n))) (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))), map_is_iso' := _}
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.splitting_iso_hom_eq_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
(Δ : simplex_categoryᵒᵖ) :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ')
{Δ'' : simplex_category}
{e : opposite.unop Δ' ⟶ Δ''}
{i : Δ'' ⟶ opposite.unop A.fst}
[category_theory.epi e]
[category_theory.mono i]
(fac : e ≫ i = θ.unop ≫ A.e) :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ')
{Δ'' : simplex_category}
{e : opposite.unop Δ' ⟶ Δ''}
{i : Δ'' ⟶ opposite.unop A.fst}
[category_theory.epi e]
[category_theory.mono i]
(fac : e ≫ i = θ.unop ≫ A.e)
{X' : C}
(f' : (algebraic_topology.dold_kan.Γ₀.obj K).obj Δ' ⟶ X') :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand'
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ') :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_on_summand'_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ')
{X' : C}
(f' : (algebraic_topology.dold_kan.Γ₀.obj K).obj Δ' ⟶ X') :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_mono_on_summand_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i] :
(algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op Δ)) ≫ (algebraic_topology.dold_kan.Γ₀.obj K).map i.op = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i ≫ (algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op Δ'))
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_mono_on_summand_id_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_category}
(i : Δ' ⟶ Δ)
[category_theory.mono i]
{X' : C}
(f' : (algebraic_topology.dold_kan.Γ₀.obj K).obj (opposite.op Δ') ⟶ X') :
(algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op Δ)) ≫ (algebraic_topology.dold_kan.Γ₀.obj K).map i.op ≫ f' = algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono K i ≫ (algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op Δ')) ≫ f'
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_epi_on_summand_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_category}
(e : Δ' ⟶ Δ)
[category_theory.epi e] :
theorem
algebraic_topology.dold_kan.Γ₀.obj.map_epi_on_summand_id_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(K : chain_complex C ℕ)
[category_theory.limits.has_finite_coproducts C]
{Δ Δ' : simplex_category}
(e : Δ' ⟶ Δ)
[category_theory.epi e]
{X' : C}
(f' : (algebraic_topology.dold_kan.Γ₀.obj K).obj (opposite.op Δ') ⟶ X') :
noncomputable
def
algebraic_topology.dold_kan.Γ₀.map
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
{K K' : chain_complex C ℕ}
(f : K ⟶ K') :
The functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, on morphisms.
Equations
- algebraic_topology.dold_kan.Γ₀.map f = {app := λ (Δ : simplex_categoryᵒᵖ), (algebraic_topology.dold_kan.Γ₀.splitting K).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), f.f (opposite.unop A.fst).len ≫ (algebraic_topology.dold_kan.Γ₀.splitting K').ι_summand A), naturality' := _}
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀.map_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
{K K' : chain_complex C ℕ}
(f : K ⟶ K')
(Δ : simplex_categoryᵒᵖ) :
(algebraic_topology.dold_kan.Γ₀.map f).app Δ = (algebraic_topology.dold_kan.Γ₀.splitting K).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), f.f (opposite.unop A.fst).len ≫ (algebraic_topology.dold_kan.Γ₀.splitting K').ι_summand A)
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀'_map_F
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K K' : chain_complex C ℕ)
(f : K ⟶ K') :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀'_obj
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ) :
noncomputable
def
algebraic_topology.dold_kan.Γ₀'
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The functor Γ₀' : chain_complex C ℕ ⥤ simplicial_object.split C
that induces Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, which
shall be the inverse functor of the Dold-Kan equivalence for
abelian or pseudo-abelian categories.
Equations
- algebraic_topology.dold_kan.Γ₀' = {obj := λ (K : chain_complex C ℕ), simplicial_object.split.mk' (algebraic_topology.dold_kan.Γ₀.splitting K), map := λ (K K' : chain_complex C ℕ) (f : K ⟶ K'), {F := algebraic_topology.dold_kan.Γ₀.map f, f := f.f, comm' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀'_map_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K K' : chain_complex C ℕ)
(f : K ⟶ K')
(i : ℕ) :
(algebraic_topology.dold_kan.Γ₀'.map f).f i = f.f i
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀_obj_map
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : chain_complex C ℕ)
(Δ Δ' : simplex_categoryᵒᵖ)
(θ : Δ ⟶ Δ') :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀_obj_obj
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : chain_complex C ℕ)
(Δ : simplex_categoryᵒᵖ) :
@[simp]
theorem
algebraic_topology.dold_kan.Γ₀_map_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(_x _x_1 : chain_complex C ℕ)
(f : _x ⟶ _x_1)
(Δ : simplex_categoryᵒᵖ) :
(algebraic_topology.dold_kan.Γ₀.map f).app Δ = (algebraic_topology.dold_kan.Γ₀.splitting _x).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), f.f (opposite.unop A.fst).len ≫ (algebraic_topology.dold_kan.Γ₀.splitting _x_1).ι_summand A)
noncomputable
def
algebraic_topology.dold_kan.Γ₀
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, which is
the inverse functor of the Dold-Kan equivalence when C is an abelian
category, or more generally a pseudoabelian category.
@[simp]
theorem
algebraic_topology.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ᵒᵖ) :
(algebraic_topology.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)
noncomputable
def
algebraic_topology.dold_kan.Γ₂
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The extension of Γ₀ : chain_complex C ℕ ⥤ simplicial_object C
on the idempotent completions. It shall be an equivalence of categories
for any additive category C.
@[simp]
theorem
algebraic_topology.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ᵒᵖ) :
(algebraic_topology.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)
@[simp]
theorem
algebraic_topology.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
algebraic_topology.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ᵒᵖ) :
theorem
algebraic_topology.dold_kan.higher_faces_vanish.on_Γ₀_summand_id
{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.P_infty_on_Γ₀_splitting_summand_eq_self
{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.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))) ≫ algebraic_topology.dold_kan.P_infty.f n = (algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n)))
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_on_Γ₀_splitting_summand_eq_self_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(K : chain_complex C ℕ)
{n : ℕ}
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj (algebraic_topology.dold_kan.Γ₀.obj K)).X n ⟶ X') :
(algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))) ≫ algebraic_topology.dold_kan.P_infty.f n ≫ f' = (algebraic_topology.dold_kan.Γ₀.splitting K).ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))) ≫ f'