A lift is determined by one point: 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 proved5Proved, and every prerequisite is fully proved too.

graph LR n0("A lift is determined by one point"):::mathlib n1("Covering-space actions give quotient coverings"):::fully_proved n2("Equal image subgroups characterize pointed cover isomorphism"):::fully_proved n3("A deck transformation is determined by one lifted point"):::fully_proved n4["Orbit quotients are normal and have the expected deck group"]:::fully_proved n5("A simply-connected cover maps uniquely to every pointed connected cover"):::fully_proved n1 --> n4 n2 -.-> n3 n0 -.-> n1 n0 -.-> n3 n0 -.-> n4 n0 -.-> n2 n0 -.-> n5 class n0 focus click n0 "../../../../roadmap/fundamental-group/covering-spaces/index.html#unique-lifting" "A lift is determined by one point — 1 item · 1 in mathlib" click n1 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#covering-space-action" "Covering-space actions give quotient coverings — 1 item · 1 fully proved" click n2 "../../../../roadmap/fundamental-group/covering-spaces/index.html#pointed-cover-rigidity" "Equal image subgroups characterize pointed cover isomorphism — 1 item · 1 fully proved" click n3 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-realization" "A deck transformation is determined by one lifted point — 1 item · 1 fully proved" click n4 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#orbit-quotient-deck-group" "Orbit quotients are normal and have the expected deck group — 1 item · 1 fully proved" click n5 "../../../../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"