The induced subgroup consists of loops with closed lifts: 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. in mathlib1Upstreamed into Mathlib.fully proved6Proved, and every prerequisite is fully proved too.
graph LR
n0["The fundamental group acts on a covering fiber"]:::mathlib
n1("The induced subgroup consists of loops with closed lifts"):::fully_proved
n2("Changing the lifted basepoint conjugates the image subgroup"):::fully_proved
n3("The normalizer map is surjective with kernel the covering subgroup"):::fully_proved
n4("The subgroup cover realizes the chosen subgroup"):::fully_proved
n5["Sheets are cosets of the induced subgroup"]:::fully_proved
n6("The path-class cover is simply-connected"):::fully_proved
n1 -.-> n2
n1 -.-> n3
n1 -.-> n5
n1 -.-> n4
n1 -.-> n6
n0 --> n1
n0 -.-> n2
n0 -.-> n5
click n0 "../../../../roadmap/fundamental-group/covering-spaces/index.html#monodromy-action" "The fundamental group acts on a covering fiber — 1 item · 1 in mathlib"
class n1 focus
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/deck-transformations/index.html#normalizer-to-deck-exactness" "The normalizer map is surjective with kernel the covering subgroup — 1 item · 1 fully proved"
click n4 "../../../../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-image" "The subgroup cover realizes the chosen subgroup — 1 item · 1 fully proved"
click n5 "../../../../roadmap/fundamental-group/covering-spaces/index.html#sheet-index" "Sheets are cosets of the induced subgroup — 1 item · 1 fully proved"
click n6 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-simply-connected" "The path-class cover is simply-connected — 1 item · 1 fully proved"