A homotopy equivalence induces homology isomorphisms: local context

Project map · Chapter map · Full theorem DAG · Open textbook statement

This local map shows one dependency hop in either direction. The highlighted item is the current focus. What the colours mean

in mathlib3Upstreamed into Mathlib.fully proved6Proved, and every prerequisite is fully proved too.

graph LR n0["A chain map induces a map on homology"]:::mathlib n1["Singular homology"]:::mathlib n2("Homotopic maps induce the same singular-homology map"):::mathlib n3["A homotopy equivalence induces homology isomorphisms"]:::fully_proved n4["Enlarging to the chosen neighborhood preserves relative homology"]:::fully_proved n5["Enlarging the quotient point preserves relative homology"]:::fully_proved n6("The ordinary neighborhood-retract Mayer–Vietoris sequence"):::fully_proved n7("Excision holds for a union of CW subcomplexes"):::fully_proved n8["The mapping-cone cover has the relative homology of the original pair"]:::fully_proved n0 -.-> n3 n0 --> n2 n3 -.-> n7 n3 -.-> n8 n3 -.-> n6 n3 -.-> n4 n3 -.-> n5 n1 --> n3 n2 -.-> n3 click n0 "../../../../roadmap/homology/simplicial-and-singular/index.html#chain-map-homology" "A chain map induces a map on homology — 1 item · 1 in mathlib" click n1 "../../../../roadmap/homology/simplicial-and-singular/index.html#singular-homology" "Singular homology — 1 item · 1 in mathlib" click n2 "../../../../roadmap/homology/simplicial-and-singular/index.html#singular-homology-homotopy-invariance" "Homotopic maps induce the same singular-homology map — 1 item · 1 in mathlib" class n3 focus click n3 "../../../../roadmap/homology/simplicial-and-singular/index.html#homotopy-equivalence-homology-iso" "A homotopy equivalence induces homology isomorphisms — 1 item · 1 fully proved" click n4 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-neighborhood-relative-homology" "Enlarging to the chosen neighborhood preserves relative homology — 1 item · 1 fully proved" click n5 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-neighborhood-relative-homology" "Enlarging the quotient point preserves relative homology — 1 item · 1 fully proved" click n6 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#ordinary-neighborhood-mayer-vietoris" "The ordinary neighborhood-retract Mayer–Vietoris sequence — 1 item · 1 fully proved" click n7 "../../../../roadmap/homology/computations-and-applications/post-excision-applications/index.html#cw-subcomplex-excision" "Excision holds for a union of CW subcomplexes — 1 item · 1 fully proved" click n8 "../../../../roadmap/homology/computations-and-applications/post-excision-applications/index.html#mapping-cone-cover-relative-homology" "The mapping-cone cover has the relative homology of the original pair — 1 item · 1 fully proved"