Commit 2022-10-08 20:02 324a7502

View on Github →

feat(algebraic_topology): extra degeneracies and homotopy equivalences (#16855) In this PR, it is shown that if an augmented simplicial object X in a preadditive category has an extra degeneracy, then the augmentation is a homotopy equivalence on the alternating face map complex.

Estimated changes

Modified src/algebra/homology/single.lean

added def chain_complex.from_single₀_equiv

added theorem chain_complex.to_single₀_ext

Modified src/algebraic_topology/alternating_face_map_complex.lean

added def algebraic_topology.alternating_face_map_complex.ε

Modified src/algebraic_topology/extra_degeneracy.lean

added def simplicial_object.augmented.extra_degeneracy.homotopy_equiv

Modified src/category_theory/preadditive/projective_resolution.lean