Simplicial and singular homology dependency map
This map shows the container's direct articles. Nested containers are collapsed and clickable; dependency edges are rolled up from their leaves. in mathlib10Upstreamed into Mathlib.fully proved82Proved, and every prerequisite is fully proved too.ready to state1Prerequisites are stated, so this can be written down.
graph LR
n0("Chain-homotopic maps induce the same homology map"):::mathlib
n1["A chain map induces a map on homology"]:::mathlib
n2["A homotopy equivalence induces homology isomorphisms"]:::fully_proved
n3("Homology of a point"):::fully_proved
n4["Relative homology and exact sequences<br/><small>45 items · 2 in mathlib · 43 fully proved</small>"]:::scope
n5["The singular chain complex"]:::mathlib
n6("Homotopic maps induce the same singular-homology map"):::mathlib
n7["Singular homology"]:::mathlib
n8["A topological homotopy gives a singular-chain homotopy"]:::mathlib
n9("Higher homology vanishes for totally disconnected spaces"):::mathlib
n10["Zeroth homology is free on path components"]:::mathlib
n11["External chapter: Homology<br/><small>38 items · 37 fully proved · 1 ready to state</small>"]:::boundary
n0 -.-> n11
n0 -.-> n6
n0 -. 2 .-> n4
n1 --> n0
n1 -.-> n2
n1 --> n6
n1 -->|2| n4
n2 -. 3 .-> n11
n2 -. 2 .-> n4
n3 -.-> n11
n3 -.-> n4
n5 --> n11
n5 --> n7
n5 --> n6
n5 --> n8
n5 -->|2| n4
n7 --> n2
n7 --> n3
n7 --> n9
n7 --> n10
n7 -->|3| n4
n6 -.-> n2
n8 -.-> n11
n8 -.-> n6
n8 -.-> n4
n9 -.-> n11
n9 -.-> n3
n10 -.-> n11
n10 -.-> n3
n4 -->|40| n11
n4 -. 24 .-> n11
click n0 "../../../roadmap/homology/simplicial-and-singular/index.html#chain-homotopy-invariance" "Chain-homotopic maps induce the same homology map — 1 item · 1 in mathlib"
click n1 "../../../roadmap/homology/simplicial-and-singular/index.html#chain-map-homology" "A chain map induces a map on homology — 1 item · 1 in mathlib"
click n2 "../../../roadmap/homology/simplicial-and-singular/index.html#homotopy-equivalence-homology-iso" "A homotopy equivalence induces homology isomorphisms — 1 item · 1 fully proved"
click n3 "../../../roadmap/homology/simplicial-and-singular/index.html#point-homology" "Homology of a point — 1 item · 1 fully proved"
click n4 "simplicial-and-singular/relative-homology.html" "Relative homology and exact sequences — 45 items · 2 in mathlib · 43 fully proved"
click n5 "../../../roadmap/homology/simplicial-and-singular/index.html#singular-chain-complex" "The singular chain complex — 1 item · 1 in mathlib"
click n6 "../../../roadmap/homology/simplicial-and-singular/index.html#singular-homology-homotopy-invariance" "Homotopic maps induce the same singular-homology map — 1 item · 1 in mathlib"
click n7 "../../../roadmap/homology/simplicial-and-singular/index.html#singular-homology" "Singular homology — 1 item · 1 in mathlib"
click n8 "../../../roadmap/homology/simplicial-and-singular/index.html#topological-homotopy-chain-homotopy" "A topological homotopy gives a singular-chain homotopy — 1 item · 1 in mathlib"
click n9 "../../../roadmap/homology/simplicial-and-singular/index.html#totally-disconnected-higher-homology" "Higher homology vanishes for totally disconnected spaces — 1 item · 1 in mathlib"
click n10 "../../../roadmap/homology/simplicial-and-singular/index.html#zeroth-homology-components" "Zeroth homology is free on path components — 1 item · 1 in mathlib"
click n11 "../../chapters/homology.html" "Homology — 38 items · 37 fully proved · 1 ready to state"