Relative singular chains and 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 mathlib1Upstreamed into Mathlib.fully proved20Proved, and every prerequisite is fully proved too.ready to state1Prerequisites are stated, so this can be written down.

graph LR n0["The singular set of a topological pair"]:::fully_proved n1["Singular homology"]:::mathlib n2["Relative singular chains and homology"]:::fully_proved n3["The boundary and zero horn of a standard topological simplex"]:::fully_proved n4("The long exact sequence of a pair"):::fully_proved n5["Relative homology at a basepoint is reduced homology"]:::fully_proved n6("Componentwise isomorphisms imply a relative isomorphism"):::fully_proved n7("The binary-cover excision chain map is a homotopy equivalence"):::fully_proved n8["Binary-cover excision induces homology isomorphisms"]:::fully_proved n9["Deleted-subset excision induces homology isomorphisms"]:::fully_proved n10("The pair long exact sequence is natural"):::fully_proved n11("Relative chains of a triple form a short exact sequence"):::fully_proved n12["A homotopy of pairs gives a relative chain homotopy"]:::fully_proved n13("Homotopic maps of pairs induce the same relative-homology map"):::fully_proved n14["A contractible subspace identifies reduced and relative homology"]:::fully_proved n15["Relative singular chains commute with topological coproducts"]:::fully_proved n16["Relative chains commute with coproducts of arbitrary pairs"]:::can_state n17("Local homology is unchanged on an open neighborhood"):::fully_proved n18("Deleted-pair homology is local on an open neighborhood"):::fully_proved n19("Excision holds for a union of CW subcomplexes"):::fully_proved n20["The mapping-cone cover has the relative homology of the original pair"]:::fully_proved n21["Relative homology is reduced homology of the mapping cone"]:::fully_proved n17 --> n18 n14 --> n21 n20 --> n21 n15 -.-> n16 n6 -.-> n19 n6 -.-> n20 n4 -.-> n6 n4 --> n10 n12 -.-> n13 n2 --> n18 n2 --> n16 n2 --> n17 n2 --> n14 n2 --> n19 n2 --> n20 n2 --> n21 n2 --> n15 n2 --> n3 n2 --> n6 n2 --> n4 n2 --> n10 n2 --> n5 n2 --> n13 n2 --> n12 n2 --> n7 n2 --> n8 n2 --> n9 n2 --> n11 n0 --> n2 n7 --> n8 n8 -.-> n18 n8 -.-> n19 n8 -.-> n21 n8 -.-> n9 n9 -.-> n17 n1 --> n4 n1 --> n2 click n0 "../../../../../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 n1 "../../../../../roadmap/homology/simplicial-and-singular/index.html#singular-homology" "Singular homology — 1 item · 1 in mathlib" class n2 focus 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/computations-and-applications/post-excision-applications/index.html#standard-simplex-boundary-horn" "The boundary and zero horn of a standard topological simplex — 1 item · 1 fully proved" click n4 "../../../../../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 n5 "../../../../../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 n6 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#relative-homology-map-isomorphism-criterion" "Componentwise isomorphisms imply a relative isomorphism — 1 item · 1 fully proved" click n7 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#binary-cover-excision-chain-equivalence" "The binary-cover excision chain map is a homotopy equivalence — 1 item · 1 fully proved" click n8 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#binary-cover-excision-homology-isomorphism" "Binary-cover excision induces homology isomorphisms — 1 item · 1 fully proved" click n9 "../../../../../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#deleted-subset-excision-homology-isomorphism" "Deleted-subset excision induces homology isomorphisms — 1 item · 1 fully proved" click n10 "../../../../../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 n11 "../../../../../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 n12 "../../../../../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 n13 "../../../../../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 n14 "../../../../../roadmap/homology/computations-and-applications/post-excision-applications/index.html#contractible-subspace-relative-reduced-homology" "A contractible subspace identifies reduced and relative homology — 1 item · 1 fully proved" click n15 "../../../../../roadmap/homology/computations-and-applications/post-excision-applications/index.html#singular-relative-chains-coproduct" "Relative singular chains commute with topological coproducts — 1 item · 1 fully proved" click n16 "../../../../../roadmap/homology/computations-and-applications/local-degree/index.html#relative-chains-sigma-pair" "Relative chains commute with coproducts of arbitrary pairs — 1 item · 1 ready to state" click n17 "../../../../../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html#local-homology-open-neighborhood" "Local homology is unchanged on an open neighborhood — 1 item · 1 fully proved" click n18 "../../../../../roadmap/homology/computations-and-applications/local-degree/index.html#deleted-pair-open-neighborhood" "Deleted-pair homology is local on an open neighborhood — 1 item · 1 fully proved" click n19 "../../../../../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 n20 "../../../../../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" click n21 "../../../../../roadmap/homology/computations-and-applications/post-excision-applications/index.html#mapping-cone-relative-reduced-homology" "Relative homology is reduced homology of the mapping cone — 1 item · 1 fully proved"