Deck transformations and quotient actions 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 mathlib3Upstreamed into Mathlib.fully proved11Proved, and every prerequisite is fully proved too.
graph LR
n0("Covering-space actions give quotient coverings"):::fully_proved
n1["The deck group is the normalizer quotient"]:::fully_proved
n2("A deck transformation is determined by one lifted point"):::fully_proved
n3["Deck transformations and normal covers"]:::mathlib
n4("The normalizer map is surjective with kernel the covering subgroup"):::fully_proved
n5["The normalizer acts by deck transformations"]:::fully_proved
n6["Orbit quotients are normal and have the expected deck group"]:::fully_proved
n7["The orbit-quotient fundamental group recovers the acting group"]:::fully_proved
n8["External chapter: The fundamental group<br/><small>6 items · 2 in mathlib · 4 fully proved</small>"]:::boundary
n8 -.-> n0
n8 --> n1
n8 -.-> n1
n8 --> n2
n8 -. 2 .-> n2
n8 -->|2| n5
n8 -.-> n5
n8 -.-> n4
n8 -.-> n6
n0 --> n6
n0 --> n7
n1 -.-> n7
n2 -.-> n5
n2 -.-> n4
n3 --> n0
n3 --> n1
n3 --> n2
n3 --> n5
n3 --> n6
n5 --> n4
n4 -.-> n1
n6 -.-> n7
click n0 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#covering-space-action" "Covering-space actions give quotient coverings — 1 item · 1 fully proved"
click n1 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-group-calculation" "The deck group is the normalizer quotient — 1 item · 1 fully proved"
click n2 "../../../../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 n3 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-transformation-group" "Deck transformations and normal covers — 1 item · 1 in mathlib"
click n4 "../../../../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 n5 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#normalizer-to-deck" "The normalizer acts by deck transformations — 1 item · 1 fully proved"
click n6 "../../../../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 n7 "../../../../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#orbit-quotient-fundamental-group" "The orbit-quotient fundamental group recovers the acting group — 1 item · 1 fully proved"
click n8 "../../../chapters/fundamental-group.html" "The fundamental group — 6 items · 2 in mathlib · 4 fully proved"