How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The orbit map of a covering-space action is a covering, with the acting group equal to the deck group when the total space is path-connected
Statement
For a covering-space action of on , the orbit map is a covering. If is path-connected, the deck group of this covering consists exactly of the transformations supplied by .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A left action of a group on a space by homeomorphisms is a covering-space action when every has an open neighbourhood such that for every nonidentity (def-group-action, def-homeomorphism-and-open-maps). Acting by homeomorphisms means that each map is a homeomorphism of ; the underlying set action alone would not make the translates open. This condition implies freeness (def-free-group-action) and makes the translates of pairwise disjoint. (Covering-space actions by disjoint translates of neighbourhoods).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
The quotient topology. Let be a topological space (def-topological-space), let be a set and let be a surjection (def-injection-surjection-bijection). The quotient topology on induced by is the final topology of the one-element family (def-initial-and-final-topology): That this is a topology is discharged in def-initial-and-final-topology, where every final topology is verified to satisfy (T1), (T2) and (T3). Dually, is closed in exactly when is closed in , because . (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).
For a covering , a deck transformation is an isomorphism over , so (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group under composition, and this group acts on by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).
For a covering with connected total space, two deck transformations agreeing at one point are equal. Consequently the deck group acts freely on the total space. (On a connected covering space, a deck transformation is determined by one point and the deck action is free).
Let and be topological spaces and let be continuous (def-continuous-map-top). Each of the following three conditions makes a quotient map (def-quotient-topology). 1. is a surjection and an open map (def-homeomorphism-and-open-maps). 2. is a surjection and a closed map. 3. admits a continuous section: a continuous with . (Surjectivity of is then automatic and need not be assumed.) Neither clause 1 nor clause 2 is necessary: a quotient map need be neither open nor closed. A witness that is a quotient map by clause 3 while failing clauses 1 and 2 is worked on the companion page, and is named in the remarks below. (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps).
Proof
Let be a neighbourhood whose nonidentity translates are disjoint. Each acts by a homeomorphism of by [F1], so every translate is open, and the full preimage of the orbit image of is , a disjoint union of open sets. That preimage being open makes the orbit image open in the quotient topology of [F3], and the orbit map is then an open continuous surjection, so [F6] applies to it.
Each translate maps homeomorphically onto that quotient neighbourhood.
The action is free automatically, and when is nonempty this embeds the acting group in the deck group: freeness makes force , so distinct group elements give distinct translates. The nonemptiness is needed — on every translate is the identity, so a nontrivial does not embed.
If the total space is path-connected, compare any deck transformation at one point with the unique group translate taking that point to its image; one-point determination then proves equality with that translate.
The preceding construction and implications establish the assertion.
Depends on
- Covering-space actions by disjoint translates of neighbourhoods
- Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
- Deck transformations and the deck-transformation group of a covering
- On a connected covering space, a deck transformation is determined by one point and the deck action is free
- A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 35 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Allen Hatcher, Algebraic Topology, §1.3 (standard reference, not scraped)
- J. Peter May, A Concise Course in Algebraic Topology, Ch. 3 (standard reference, not scraped)
- Marco Gualtieri, MAT1300 Week 4 Term 2, §1.6 (standard reference, not scraped)