Singular homology: 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 mathlib4Upstreamed into Mathlib.fully proved5Proved, and every prerequisite is fully proved too.

graph LR n0["The singular chain complex"]:::mathlib n1["Singular homology"]:::mathlib n2["Relative singular chains and homology"]:::fully_proved n3("The long exact sequence of a pair"):::fully_proved n4["Reduced and ordinary homology agree in positive degrees"]:::fully_proved n5["Zeroth homology is free on path components"]:::mathlib n6("Higher homology vanishes for totally disconnected spaces"):::mathlib n7("Homology of a point"):::fully_proved n8["A homotopy equivalence induces homology isomorphisms"]:::fully_proved n2 --> n3 n0 --> n1 n1 --> n8 n1 --> n7 n1 --> n3 n1 --> n4 n1 --> n2 n1 --> n6 n1 --> n5 n6 -.-> n7 n5 -.-> n7 click n0 "../../../../roadmap/homology/simplicial-and-singular/index.html#singular-chain-complex" "The singular chain complex — 1 item · 1 in mathlib" class n1 focus 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/relative-homology/index.html#relative-singular-homology" "Relative singular chains and homology — 1 item · 1 fully proved" click n3 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pair-long-exact-sequence" "The long exact sequence of a pair — 1 item · 1 fully proved" click n4 "../../../../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 n5 "../../../../roadmap/homology/simplicial-and-singular/index.html#zeroth-homology-components" "Zeroth homology is free on path components — 1 item · 1 in mathlib" click n6 "../../../../roadmap/homology/simplicial-and-singular/index.html#totally-disconnected-higher-homology" "Higher homology vanishes for totally disconnected spaces — 1 item · 1 in mathlib" click n7 "../../../../roadmap/homology/simplicial-and-singular/index.html#point-homology" "Homology of a point — 1 item · 1 fully proved" click n8 "../../../../roadmap/homology/simplicial-and-singular/index.html#homotopy-equivalence-homology-iso" "A homotopy equivalence induces homology isomorphisms — 1 item · 1 fully proved"