Reduced homology of the zero-sphere: 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 mathlib2Upstreamed into Mathlib.fully proved6Proved, and every prerequisite is fully proved too.

graph LR n0["Reduced singular homology"]:::fully_proved n1["Reduced and ordinary homology agree in positive degrees"]:::fully_proved n2["Zeroth homology splits into reduced homology and the coefficient object"]:::fully_proved n3["Zeroth homology is free on path components"]:::mathlib n4("Higher homology vanishes for totally disconnected spaces"):::mathlib n5["The zero-sphere is a two-point space"]:::fully_proved n6("Reduced homology of the zero-sphere"):::fully_proved n7("Reduced homology of spheres"):::fully_proved n6 -.-> n7 n5 -.-> n6 n2 -.-> n6 n1 -.-> n6 n0 --> n7 n0 --> n6 n0 --> n2 n0 --> n1 n4 -.-> n6 n3 -.-> n6 click n0 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-singular-homology" "Reduced singular homology — 1 item · 1 fully proved" click n1 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-positive-degree-comparison" "Reduced and ordinary homology agree in positive degrees — 1 item · 1 fully proved" click n2 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pointed-zeroth-homology-splitting" "Zeroth homology splits into reduced homology and the coefficient object — 1 item · 1 fully proved" click n3 "../../../../../roadmap/homology/simplicial-and-singular/index.html#zeroth-homology-components" "Zeroth homology is free on path components — 1 item · 1 in mathlib" click n4 "../../../../../roadmap/homology/simplicial-and-singular/index.html#totally-disconnected-higher-homology" "Higher homology vanishes for totally disconnected spaces — 1 item · 1 in mathlib" click n5 "../../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#zero-sphere-two-point-homeomorphism" "The zero-sphere is a two-point space — 1 item · 1 fully proved" class n6 focus click n6 "../../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#zero-sphere-reduced-homology" "Reduced homology of the zero-sphere — 1 item · 1 fully proved" click n7 "../../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-reduced-homology" "Reduced homology of spheres — 1 item · 1 fully proved"