Mayer–Vietoris transport, sphere homology, and Brouwer 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 mathlib4Upstreamed into Mathlib.fully proved31Proved, and every prerequisite is fully proved too.
graph LR
n0("Brouwer's fixed-point theorem for disks"):::fully_proved
n1["A closed ball strongly deformation retracts from Euclidean space"]:::fully_proved
n2("Reduced homology of a contractible space vanishes"):::fully_proved
n3("The boundary sphere is not a retract of the disk"):::fully_proved
n4("A fixed-point-free disk map produces a boundary retraction"):::fully_proved
n5["A homotopy equivalence induces reduced-homology isomorphisms"]:::fully_proved
n6("The ordinary neighborhood-retract Mayer–Vietoris sequence"):::fully_proved
n7["A sphere strongly deformation retracts from punctured Euclidean space"]:::fully_proved
n8("Homotopic maps induce the same reduced-homology map"):::fully_proved
n9("The reduced neighborhood-retract Mayer–Vietoris sequence"):::fully_proved
n10["The hemispheres have compatible neighborhood deformation retractions"]:::fully_proved
n11["Stereographic models for hemispheres and the equator"]:::fully_proved
n12("The reduced homology of spheres satisfies the suspension recurrence"):::fully_proved
n13("Reduced homology of spheres"):::fully_proved
n14("Reduced homology of the zero-sphere"):::fully_proved
n15["The zero-sphere is a two-point space"]:::fully_proved
n16["External chapter: The fundamental group<br/><small>1 item · 1 fully proved</small>"]:::boundary
n17["External chapter: Homology<br/><small>18 items · 4 in mathlib · 14 fully proved</small>"]:::boundary
n16 --> n6
n17 --> n2
n17 -.-> n2
n17 --> n5
n17 -->|2| n6
n17 -.-> n6
n17 --> n8
n17 -. 2 .-> n8
n17 --> n9
n17 --> n13
n17 --> n12
n17 --> n14
n17 -. 4 .-> n14
n1 -.-> n10
n2 -. 4 .-> n17
n2 -.-> n3
n2 -.-> n12
n3 -.-> n0
n4 -.-> n0
n5 -.-> n17
n5 -.-> n2
n5 -.-> n9
n6 --> n1
n6 --> n7
n6 --> n9
n6 --> n10
n7 -.-> n17
n7 -.-> n10
n8 -.-> n5
n9 -.-> n12
n10 -.-> n12
n11 -.-> n17
n11 --> n10
n11 -.-> n12
n13 -.-> n17
n13 -.-> n3
n12 -.-> n13
n14 -.-> n13
n15 -.-> n14
click n0 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#brouwer-fixed-point-disk" "Brouwer's fixed-point theorem for disks — 1 item · 1 fully proved"
click n1 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#closed-ball-radial-deformation-retract" "A closed ball strongly deformation retracts from Euclidean space — 1 item · 1 fully proved"
click n2 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#contractible-space-reduced-homology" "Reduced homology of a contractible space vanishes — 1 item · 1 fully proved"
click n3 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#disk-boundary-no-retraction" "The boundary sphere is not a retract of the disk — 1 item · 1 fully proved"
click n4 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#fixed-point-free-disk-map-retraction" "A fixed-point-free disk map produces a boundary retraction — 1 item · 1 fully proved"
click n5 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#homotopy-equivalence-reduced-homology-iso" "A homotopy equivalence induces reduced-homology isomorphisms — 1 item · 1 fully proved"
click n6 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#ordinary-neighborhood-mayer-vietoris" "The ordinary neighborhood-retract Mayer–Vietoris sequence — 1 item · 1 fully proved"
click n7 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#punctured-space-radial-deformation-retract" "A sphere strongly deformation retracts from punctured Euclidean space — 1 item · 1 fully proved"
click n8 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#reduced-homology-homotopy-invariance" "Homotopic maps induce the same reduced-homology map — 1 item · 1 fully proved"
click n9 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#reduced-neighborhood-mayer-vietoris" "The reduced neighborhood-retract Mayer–Vietoris sequence — 1 item · 1 fully proved"
click n10 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-hemisphere-neighborhood-cover" "The hemispheres have compatible neighborhood deformation retractions — 1 item · 1 fully proved"
click n11 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-hemisphere-stereographic-models" "Stereographic models for hemispheres and the equator — 1 item · 1 fully proved"
click n12 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-reduced-homology-recurrence" "The reduced homology of spheres satisfies the suspension recurrence — 1 item · 1 fully proved"
click n13 "../../../../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-reduced-homology" "Reduced homology of spheres — 1 item · 1 fully proved"
click n14 "../../../../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 n15 "../../../../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"
click n16 "../../../chapters/fundamental-group.html" "The fundamental group — 1 item · 1 fully proved"
click n17 "../../../chapters/homology.html" "Homology — 18 items · 4 in mathlib · 14 fully proved"