THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. The unit isomorphism of the Dold-Kan equivalence
In order to construct the unit isomorphism of the Dold-Kan equivalence,
we first construct natural transformations
Γ₂N₁.nat_trans : N₁ ⋙ Γ₂ ⟶ to_karoubi (simplicial_object C) and
Γ₂N₂.nat_trans : N₂ ⋙ Γ₂ ⟶ 𝟭 (simplicial_object C).
It is then shown that Γ₂N₂.nat_trans is an isomorphism by using
that it becomes an isomorphism after the application of the functor
N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)
which reflects isomorphisms.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
theorem
algebraic_topology.dold_kan.P_infty_comp_map_mono_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{Δ' : simplex_category}
(i : Δ' ⟶ simplex_category.mk n)
[hi : category_theory.mono i]
(h₁ : Δ'.len ≠ n)
(h₂ : ¬algebraic_topology.dold_kan.is_δ₀ i) :
theorem
algebraic_topology.dold_kan.Γ₀_obj_termwise_map_mono_comp_P_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{Δ Δ' : simplex_category}
(i : Δ ⟶ Δ')
[category_theory.mono i]
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X Δ.len ⟶ X') :
theorem
algebraic_topology.dold_kan.Γ₀_obj_termwise_map_mono_comp_P_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{Δ Δ' : simplex_category}
(i : Δ ⟶ Δ')
[category_theory.mono i] :
noncomputable
def
algebraic_topology.dold_kan.Γ₂N₁.nat_trans
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The natural transformation N₁ ⋙ Γ₂ ⟶ to_karoubi (simplicial_object C).
Equations
- algebraic_topology.dold_kan.Γ₂N₁.nat_trans = {app := λ (X : category_theory.simplicial_object C), {f := {app := λ (Δ : simplex_categoryᵒᵖ), (algebraic_topology.dold_kan.Γ₀.splitting (algebraic_topology.alternating_face_map_complex.obj X)).desc Δ (λ (A : simplicial_object.splitting.index_set Δ), algebraic_topology.dold_kan.P_infty.f (opposite.unop A.fst).len ≫ X.map A.e.op), naturality' := _}, comm := _}, naturality' := _}
Instances for algebraic_topology.dold_kan.Γ₂N₁.nat_trans
@[simp]
theorem
algebraic_topology.dold_kan.Γ₂N₁.nat_trans_app_f_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : category_theory.simplicial_object C)
(Δ : simplex_categoryᵒᵖ) :
@[simp]
theorem
algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂_hom
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂.hom = category_theory.eq_to_hom algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂._proof_1
noncomputable
def
algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The compatibility isomorphism relating N₂ ⋙ Γ₂ and N₁ ⋙ Γ₂.
Equations
- algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂ = category_theory.eq_to_iso algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂._proof_1
noncomputable
def
algebraic_topology.dold_kan.Γ₂N₂.nat_trans
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The natural transformation N₂ ⋙ Γ₂ ⟶ 𝟭 (simplicial_object C).
Equations
- algebraic_topology.dold_kan.Γ₂N₂.nat_trans = ((category_theory.whiskering_left (category_theory.simplicial_object C) (category_theory.idempotents.karoubi (category_theory.simplicial_object C)) (category_theory.idempotents.karoubi (category_theory.simplicial_object C))).obj (category_theory.idempotents.to_karoubi (category_theory.simplicial_object C))).preimage (algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂.hom ≫ algebraic_topology.dold_kan.Γ₂N₁.nat_trans)
Instances for algebraic_topology.dold_kan.Γ₂N₂.nat_trans
theorem
algebraic_topology.dold_kan.identity_N₂
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts 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 unit isomorphism of the Dold-Kan equivalence.
@[simp]
theorem
algebraic_topology.dold_kan.Γ₂N₁_inv_app_f_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : category_theory.simplicial_object C)
(Δ : simplex_categoryᵒᵖ) :
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 to_karoubi (simplicial_object C) ≅ N₁ ⋙ Γ₂.