mathlib3documentation

algebraic_topology.dold_kan.n_comp_gamma

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} {n : } {Δ' : simplex_category} (i : Δ' ) [hi : category_theory.mono i] (h₁ : Δ'.len n)  :
= 0
theorem algebraic_topology.dold_kan.Γ₀_obj_termwise_map_mono_comp_P_infty_assoc {C : Type u_1} {Δ Δ' : simplex_category} (i : Δ Δ') {X' : C} (f' : X') :

The natural transformation N₁ ⋙ Γ₂ ⟶ to_karoubi (simplicial_object C).

Equations
Instances for algebraic_topology.dold_kan.Γ₂N₁.nat_trans
@[simp]
@[simp]

The compatibility isomorphism relating N₂ ⋙ Γ₂ and N₁ ⋙ Γ₂.

Equations

The natural transformation N₂ ⋙ Γ₂ ⟶ 𝟭 (simplicial_object C).

Equations
Instances for algebraic_topology.dold_kan.Γ₂N₂.nat_trans
@[protected, instance]
@[protected, instance]
@[simp]

The unit isomorphism of the Dold-Kan equivalence.

Equations
@[simp]
@[simp]

The natural isomorphism to_karoubi (simplicial_object C) ≅ N₁ ⋙ Γ₂.

Equations