A simply-connected cover maps uniquely to every pointed connected cover: 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 proved4Proved, and every prerequisite is fully proved too.

graph LR n0["Pointed connected covering spaces"]:::fully_proved n1("A lift is determined by one point"):::mathlib n2("A map lifts exactly when its fundamental group lands in the covering subgroup"):::fully_proved n3("Local path-connectedness ascends along a covering"):::fully_proved n4("A simply-connected cover maps uniquely to every pointed connected cover"):::fully_proved n0 --> n4 n2 -.-> n4 n3 -.-> n4 n1 -.-> n4 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#unique-lifting" "A lift is determined by one point — 1 item · 1 in mathlib" click n2 "../../../../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 n3 "../../../../roadmap/fundamental-group/covering-spaces/index.html#locally-path-connected-total-space" "Local path-connectedness ascends along a covering — 1 item · 1 fully proved" class n4 focus click n4 "../../../../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"