The normalized Moore complex and the alternating face map complex are homotopy equivalent #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, when the category A is abelian, we obtain the homotopy equivalence
homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex between the
normalized Moore complex and the alternating face map complex of a simplicial object in A.
noncomputable
def
algebraic_topology.dold_kan.homotopy_P_to_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
(q : ℕ) :
Inductive construction of homotopies from P q to 𝟙 _
Equations
- algebraic_topology.dold_kan.homotopy_P_to_id X (q + 1) = (homotopy.of_eq _).trans (((algebraic_topology.dold_kan.homotopy_P_to_id X q).add ((algebraic_topology.dold_kan.homotopy_Hσ_to_zero q).comp_left (algebraic_topology.dold_kan.P q))).trans (homotopy.of_eq _))
- algebraic_topology.dold_kan.homotopy_P_to_id X 0 = homotopy.refl (algebraic_topology.dold_kan.P 0)
noncomputable
def
algebraic_topology.dold_kan.homotopy_Q_to_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
(q : ℕ) :
The complement projection Q q to P q is homotopic to zero.
theorem
algebraic_topology.dold_kan.homotopy_P_to_id_eventually_constant
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{q n : ℕ}
(hqn : n < q) :
(algebraic_topology.dold_kan.homotopy_P_to_id X (q + 1)).hom n (n + 1) = (algebraic_topology.dold_kan.homotopy_P_to_id X q).hom n (n + 1)
noncomputable
def
algebraic_topology.dold_kan.homotopy_P_infty_to_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C) :
Construction of the homotopy from P_infty to the identity using eventually
(termwise) constant homotopies from P q to the identity for all q
Equations
- algebraic_topology.dold_kan.homotopy_P_infty_to_id X = {hom := λ (i j : ℕ), (algebraic_topology.dold_kan.homotopy_P_to_id X (j + 1)).hom i j, zero' := _, comm := _}
@[simp]
theorem
algebraic_topology.dold_kan.homotopy_P_infty_to_id_hom
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
(i j : ℕ) :
(algebraic_topology.dold_kan.homotopy_P_infty_to_id X).hom i j = (algebraic_topology.dold_kan.homotopy_P_to_id X (j + 1)).hom i j
@[simp]
theorem
algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex_homotopy_hom_inv_id
{A : Type u_1}
[category_theory.category A]
[category_theory.abelian A]
{Y : category_theory.simplicial_object A} :
algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex.homotopy_hom_inv_id = homotopy.of_eq algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex._proof_1
noncomputable
def
algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex
{A : Type u_1}
[category_theory.category A]
[category_theory.abelian A]
{Y : category_theory.simplicial_object A} :
The inclusion of the Moore complex in the alternating face map complex is an homotopy equivalence
Equations
- algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex = {hom := algebraic_topology.inclusion_of_Moore_complex_map Y, inv := algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex Y, homotopy_hom_inv_id := homotopy.of_eq algebraic_topology.dold_kan.homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex._proof_1, homotopy_inv_hom_id := (homotopy.of_eq _).trans (algebraic_topology.dold_kan.homotopy_P_infty_to_id Y)}
@[simp]
@[simp]