Basic constructions 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 proved27Proved, and every prerequisite is fully proved too.
graph LR
n0["Straight-line homotopy between paths"]:::fully_proved
n1("Borsuk–Ulam for the two-sphere"):::fully_proved
n2("Brouwer's fixed point theorem for the disc"):::fully_proved
n3["A path induces change of basepoint"]:::mathlib
n4("The real line covers the circle"):::fully_proved
n5("Convex sets have trivial fundamental group"):::mathlib
n6("Euclidean two-space is distinguished by dimension"):::fully_proved
n7("The fundamental group of the circle"):::fully_proved
n8("Path concatenation gives the fundamental-group law"):::fully_proved
n9("The fundamental theorem of algebra"):::fully_proved
n10("Homotopic maps differ by basepoint change"):::fully_proved
n11["A homotopy equivalence induces a fundamental-group isomorphism"]:::fully_proved
n12("A loop splits across an open cover"):::fully_proved
n13("The circle is not a retract of the disc"):::fully_proved
n14("Path homotopy is an equivalence relation"):::mathlib
n15["The fundamental group of a product"]:::fully_proved
n16("Retractions and deformation retracts on the fundamental group"):::fully_proved
n17("Simply connected spaces have unique path-homotopy classes"):::mathlib
n18("Higher spheres are simply connected"):::fully_proved
n19("Three closed sets covering the sphere contain an antipodal pair"):::fully_proved
n20["The fundamental group of the torus"]:::fully_proved
n21["Winding number of a loop in the circle"]:::fully_proved
n22["External chapter: The fundamental group<br/><small>9 items · 9 fully proved</small>"]:::boundary
n1 --> n19
n4 -.-> n7
n4 --> n21
n7 -->|5| n22
n7 -.-> n22
n7 --> n1
n7 --> n6
n7 --> n9
n7 --> n13
n7 --> n20
n8 --> n3
n12 -.-> n22
n12 --> n18
n13 --> n2
n14 --> n8
n14 --> n17
n15 --> n20
n16 --> n22
n16 -.-> n22
n17 -.-> n5
n18 -.-> n22
n18 --> n1
n18 --> n6
n21 --> n7
click n0 "../../../roadmap/fundamental-group/basic-constructions/index.html#affine-path-homotopy" "Straight-line homotopy between paths — 1 item · 1 fully proved"
click n1 "../../../roadmap/fundamental-group/basic-constructions/index.html#borsuk-ulam-sphere" "Borsuk–Ulam for the two-sphere — 1 item · 1 fully proved"
click n2 "../../../roadmap/fundamental-group/basic-constructions/index.html#brouwer-disc" "Brouwer's fixed point theorem for the disc — 1 item · 1 fully proved"
click n3 "../../../roadmap/fundamental-group/basic-constructions/index.html#change-of-basepoint" "A path induces change of basepoint — 1 item · 1 in mathlib"
click n4 "../../../roadmap/fundamental-group/basic-constructions/index.html#circle-covering" "The real line covers the circle — 1 item · 1 fully proved"
click n5 "../../../roadmap/fundamental-group/basic-constructions/index.html#convex-trivial-fundamental-group" "Convex sets have trivial fundamental group — 1 item · 1 in mathlib"
click n6 "../../../roadmap/fundamental-group/basic-constructions/index.html#euclidean-two-not-homeomorphic" "Euclidean two-space is distinguished by dimension — 1 item · 1 fully proved"
click n7 "../../../roadmap/fundamental-group/basic-constructions/index.html#fundamental-group-circle" "The fundamental group of the circle — 1 item · 1 fully proved"
click n8 "../../../roadmap/fundamental-group/basic-constructions/index.html#fundamental-group-law" "Path concatenation gives the fundamental-group law — 1 item · 1 fully proved"
click n9 "../../../roadmap/fundamental-group/basic-constructions/index.html#fundamental-theorem-algebra" "The fundamental theorem of algebra — 1 item · 1 fully proved"
click n10 "../../../roadmap/fundamental-group/basic-constructions/index.html#homotopic-maps-fundamental-group" "Homotopic maps differ by basepoint change — 1 item · 1 fully proved"
click n11 "../../../roadmap/fundamental-group/basic-constructions/index.html#homotopy-equivalence-fundamental-group" "A homotopy equivalence induces a fundamental-group isomorphism — 1 item · 1 fully proved"
click n12 "../../../roadmap/fundamental-group/basic-constructions/index.html#loop-in-open-cover" "A loop splits across an open cover — 1 item · 1 fully proved"
click n13 "../../../roadmap/fundamental-group/basic-constructions/index.html#no-retraction-disc" "The circle is not a retract of the disc — 1 item · 1 fully proved"
click n14 "../../../roadmap/fundamental-group/basic-constructions/index.html#path-homotopy-equivalence" "Path homotopy is an equivalence relation — 1 item · 1 in mathlib"
click n15 "../../../roadmap/fundamental-group/basic-constructions/index.html#product-fundamental-group" "The fundamental group of a product — 1 item · 1 fully proved"
click n16 "../../../roadmap/fundamental-group/basic-constructions/index.html#retractions-fundamental-group" "Retractions and deformation retracts on the fundamental group — 1 item · 1 fully proved"
click n17 "../../../roadmap/fundamental-group/basic-constructions/index.html#simply-connected-unique-path-classes" "Simply connected spaces have unique path-homotopy classes — 1 item · 1 in mathlib"
click n18 "../../../roadmap/fundamental-group/basic-constructions/index.html#sphere-simply-connected" "Higher spheres are simply connected — 1 item · 1 fully proved"
click n19 "../../../roadmap/fundamental-group/basic-constructions/index.html#three-closed-sets-antipodal" "Three closed sets covering the sphere contain an antipodal pair — 1 item · 1 fully proved"
click n20 "../../../roadmap/fundamental-group/basic-constructions/index.html#torus-fundamental-group" "The fundamental group of the torus — 1 item · 1 fully proved"
click n21 "../../../roadmap/fundamental-group/basic-constructions/index.html#winding-number" "Winding number of a loop in the circle — 1 item · 1 fully proved"
click n22 "../../chapters/fundamental-group.html" "The fundamental group — 9 items · 9 fully proved"