Covering spaces 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 proved28Proved, and every prerequisite is fully proved too.
graph LR
n0["Pointed connected covering spaces"]:::fully_proved
n1("The induced subgroup consists of loops with closed lifts"):::fully_proved
n2("Changing the lifted basepoint conjugates the image subgroup"):::fully_proved
n3("Covering maps inject path-homotopy classes"):::mathlib
n4["Deck transformations and quotient actions<br/><small>8 items · 1 in mathlib · 7 fully proved</small>"]:::scope
n5("Homotopies lift uniquely through a covering map"):::fully_proved
n6("A map lifts exactly when its fundamental group lands in the covering subgroup"):::fully_proved
n7("Local path-connectedness ascends along a covering"):::fully_proved
n8["The fundamental group acts on a covering fiber"]:::mathlib
n9["Pointed connected covers are classified by subgroups"]:::fully_proved
n10("Equal image subgroups characterize pointed cover isomorphism"):::fully_proved
n11["Sheets are cosets of the induced subgroup"]:::fully_proved
n12("The subgroup cover realizes the chosen subgroup"):::fully_proved
n13("The subgroup projection is a path-connected covering"):::fully_proved
n14["The covering space associated to a subgroup"]:::fully_proved
n15("A lift is determined by one point"):::mathlib
n16("A simply-connected cover maps uniquely to every pointed connected cover"):::fully_proved
n17["The path-class universal cover<br/><small>7 items · 7 fully proved</small>"]:::scope
n18["Connected covers are classified by conjugacy classes"]:::fully_proved
n0 --> n9
n0 --> n10
n0 --> n16
n0 --> n18
n0 -->|3| n4
n1 -.-> n2
n1 -.-> n11
n1 -.-> n12
n1 -.-> n4
n1 -.-> n17
n2 -.-> n18
n2 -.-> n4
n3 -.-> n17
n6 -.-> n10
n6 -.-> n16
n7 -.-> n10
n7 -.-> n16
n8 --> n1
n8 -.-> n2
n8 -.-> n11
n8 --> n4
n8 -.-> n4
n9 -.-> n18
n10 -.-> n9
n10 -.-> n4
n12 -.-> n9
n13 -.-> n12
n14 -.-> n9
n14 --> n12
n14 --> n13
n15 -.-> n10
n15 -.-> n16
n15 -. 3 .-> n4
n17 --> n9
n17 -. 3 .-> n13
n17 --> n14
n17 --> n18
click n0 "../../../roadmap/fundamental-group/covering-spaces/index.html#based-connected-cover" "Pointed connected covering spaces — 1 item · 1 fully proved"
click n1 "../../../roadmap/fundamental-group/covering-spaces/index.html#closed-lift-image" "The induced subgroup consists of loops with closed lifts — 1 item · 1 fully proved"
click n2 "../../../roadmap/fundamental-group/covering-spaces/index.html#cover-basepoint-conjugacy" "Changing the lifted basepoint conjugates the image subgroup — 1 item · 1 fully proved"
click n3 "../../../roadmap/fundamental-group/covering-spaces/index.html#covering-injective-path-classes" "Covering maps inject path-homotopy classes — 1 item · 1 in mathlib"
click n4 "covering-spaces/deck-transformations.html" "Deck transformations and quotient actions — 8 items · 1 in mathlib · 7 fully proved"
click n5 "../../../roadmap/fundamental-group/covering-spaces/index.html#homotopy-lifting" "Homotopies lift uniquely through a covering map — 1 item · 1 fully proved"
click n6 "../../../roadmap/fundamental-group/covering-spaces/index.html#lifting-criterion" "A map lifts exactly when its fundamental group lands in the covering subgroup — 1 item · 1 fully proved"
click n7 "../../../roadmap/fundamental-group/covering-spaces/index.html#locally-path-connected-total-space" "Local path-connectedness ascends along a covering — 1 item · 1 fully proved"
click n8 "../../../roadmap/fundamental-group/covering-spaces/index.html#monodromy-action" "The fundamental group acts on a covering fiber — 1 item · 1 in mathlib"
click n9 "../../../roadmap/fundamental-group/covering-spaces/index.html#pointed-cover-classification" "Pointed connected covers are classified by subgroups — 1 item · 1 fully proved"
click n10 "../../../roadmap/fundamental-group/covering-spaces/index.html#pointed-cover-rigidity" "Equal image subgroups characterize pointed cover isomorphism — 1 item · 1 fully proved"
click n11 "../../../roadmap/fundamental-group/covering-spaces/index.html#sheet-index" "Sheets are cosets of the induced subgroup — 1 item · 1 fully proved"
click n12 "../../../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-image" "The subgroup cover realizes the chosen subgroup — 1 item · 1 fully proved"
click n13 "../../../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-is-covering" "The subgroup projection is a path-connected covering — 1 item · 1 fully proved"
click n14 "../../../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-space" "The covering space associated to a subgroup — 1 item · 1 fully proved"
click n15 "../../../roadmap/fundamental-group/covering-spaces/index.html#unique-lifting" "A lift is determined by one point — 1 item · 1 in mathlib"
click n16 "../../../roadmap/fundamental-group/covering-spaces/index.html#universal-cover-initial" "A simply-connected cover maps uniquely to every pointed connected cover — 1 item · 1 fully proved"
click n17 "covering-spaces/universal-cover.html" "The path-class universal cover — 7 items · 7 fully proved"
click n18 "../../../roadmap/fundamental-group/covering-spaces/index.html#unpointed-cover-classification" "Connected covers are classified by conjugacy classes — 1 item · 1 fully proved"