Relative homology and exact sequences 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 mathlib7Upstreamed 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["The augmented singular chain complex"]:::fully_proved
n1["Good pairs and quotient exact sequences<br/><small>16 items · 16 fully proved</small>"]:::scope
n2("The pair long exact sequence is natural"):::fully_proved
n3("The long exact sequence of a pair"):::fully_proved
n4["Relative homology at a basepoint is reduced homology"]:::fully_proved
n5["Zeroth homology splits into reduced homology and the coefficient object"]:::fully_proved
n6("The reduced pair long exact sequence is natural"):::fully_proved
n7("The reduced long exact sequence of a nonempty pair"):::fully_proved
n8["Reduced and ordinary homology agree in positive degrees"]:::fully_proved
n9["Reduced singular homology"]:::fully_proved
n10("Homotopic maps of pairs induce the same relative-homology map"):::fully_proved
n11["A homotopy of pairs gives a relative chain homotopy"]:::fully_proved
n12["Relative singular chains and homology"]:::fully_proved
n13("A short exact sequence gives an exact homology sequence"):::mathlib
n14["Relative homology of a simplicial-set pair"]:::mathlib
n15["The singular set of a topological pair"]:::fully_proved
n16["Small chains and excision<br/><small>10 items · 10 fully proved</small>"]:::scope
n17["Topological triples and their maps"]:::fully_proved
n18("Relative chains of a triple form a short exact sequence"):::fully_proved
n19("The triple long exact sequence is natural"):::fully_proved
n20("The long exact sequence of a triple"):::fully_proved
n21["External chapter: Homology<br/><small>45 items · 5 in mathlib · 39 fully proved · 1 ready to state</small>"]:::boundary
n21 --> n0
n21 --> n3
n21 -.-> n4
n21 --> n8
n21 -.-> n10
n21 -.-> n11
n21 --> n12
n21 --> n13
n21 --> n14
n21 -. 2 .-> n1
n21 --> n16
n21 -.-> n16
n0 -->|2| n21
n0 -.-> n6
n0 --> n9
n3 --> n2
n3 --> n7
n3 -.-> n1
n2 -.-> n6
n4 -->|2| n21
n4 -.-> n21
n4 -->|2| n1
n5 -.-> n21
n5 --> n7
n7 --> n21
n7 -.-> n21
n7 -.-> n4
n7 --> n6
n7 --> n1
n6 -. 2 .-> n1
n8 --> n21
n8 -.-> n21
n8 --> n7
n9 -->|10| n21
n9 --> n4
n9 --> n5
n9 --> n8
n10 -.-> n21
n11 -.-> n10
n12 -->|9| n21
n12 --> n3
n12 --> n2
n12 --> n4
n12 --> n10
n12 --> n11
n12 --> n18
n12 --> n1
n12 -->|3| n16
n13 -. 2 .-> n21
n13 -.-> n3
n13 -.-> n2
n13 -.-> n6
n13 -.-> n20
n13 -.-> n19
n14 -.-> n3
n14 --> n15
n14 -.-> n18
n14 --> n16
n15 --> n12
n17 --> n21
n17 --> n18
n18 --> n21
n18 --> n20
n20 -. 2 .-> n21
n20 --> n19
n1 -->|9| n21
n1 -. 9 .-> n21
n16 -->|4| n21
n16 -. 6 .-> n21
n16 --> n1
n16 -.-> n1
click n0 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#augmented-singular-chain-complex" "The augmented singular chain complex — 1 item · 1 fully proved"
click n1 "relative-homology/good-pair-quotient.html" "Good pairs and quotient exact sequences — 16 items · 16 fully proved"
click n2 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pair-long-exact-sequence-naturality" "The pair long exact sequence is natural — 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#pointed-relative-reduced-homology" "Relative homology at a basepoint is reduced homology — 1 item · 1 fully proved"
click n5 "../../../../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 n6 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-pair-long-exact-sequence-naturality" "The reduced pair long exact sequence is natural — 1 item · 1 fully proved"
click n7 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-pair-long-exact-sequence" "The reduced long exact sequence of a nonempty pair — 1 item · 1 fully proved"
click n8 "../../../../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 n9 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-singular-homology" "Reduced singular homology — 1 item · 1 fully proved"
click n10 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-homology-homotopy-invariance" "Homotopic maps of pairs induce the same relative-homology map — 1 item · 1 fully proved"
click n11 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-singular-chain-homotopy" "A homotopy of pairs gives a relative chain homotopy — 1 item · 1 fully proved"
click n12 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-singular-homology" "Relative singular chains and homology — 1 item · 1 fully proved"
click n13 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#short-exact-homology-sequence" "A short exact sequence gives an exact homology sequence — 1 item · 1 in mathlib"
click n14 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#simplicial-pair-relative-homology" "Relative homology of a simplicial-set pair — 1 item · 1 in mathlib"
click n15 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#singular-pair-functor" "The singular set of a topological pair — 1 item · 1 fully proved"
click n16 "relative-homology/small-chains-and-excision.html" "Small chains and excision — 10 items · 10 fully proved"
click n17 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#topological-triple" "Topological triples and their maps — 1 item · 1 fully proved"
click n18 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-chain-short-exact-sequence" "Relative chains of a triple form a short exact sequence — 1 item · 1 fully proved"
click n19 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-long-exact-sequence-naturality" "The triple long exact sequence is natural — 1 item · 1 fully proved"
click n20 "../../../../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-long-exact-sequence" "The long exact sequence of a triple — 1 item · 1 fully proved"
click n21 "../../../chapters/homology.html" "Homology — 45 items · 5 in mathlib · 39 fully proved · 1 ready to state"