Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-21 16:19 d29aca84

View on Github →

feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044) This PR introduces technical lemmas about face maps and the null homotopic maps Hσ that will be used in the proof of the Dold-Kan equivalence.

Estimated changes

Modified src/algebraic_topology/alternating_face_map_complex.lean

added theorem algebraic_topology.alternating_face_map_complex.map_f

added theorem algebraic_topology.alternating_face_map_complex.obj_X

added theorem algebraic_topology.alternating_face_map_complex.obj_d_eq

added theorem algebraic_topology.alternating_face_map_complex_map_f

added theorem algebraic_topology.alternating_face_map_complex_obj_X

added theorem algebraic_topology.alternating_face_map_complex_obj_d

Created src/algebraic_topology/dold_kan/faces.lean

added theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_Hσ_eq

added theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_Hσ_eq_zero

added theorem algebraic_topology.dold_kan.higher_faces_vanish.induction

added theorem algebraic_topology.dold_kan.higher_faces_vanish.of_comp

added theorem algebraic_topology.dold_kan.higher_faces_vanish.of_succ

added def algebraic_topology.dold_kan.higher_faces_vanish

Modified src/algebraic_topology/dold_kan/homotopies.lean