Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16
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 G on E, the orbit map EE/G is a covering. If E is path-connected, the deck group of this covering consists exactly of the transformations supplied by G.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A left action of a group G on a space E by homeomorphisms is a covering-space action when every eE has an open neighbourhood U such that gUU= for every nonidentity gG (def-group-action, def-homeomorphism-and-open-maps). Acting by homeomorphisms means that each map ege is a homeomorphism of E; the underlying set action alone would not make the translates gU open. This condition implies freeness (def-free-group-action) and makes the translates of U pairwise disjoint. (Covering-space actions by disjoint translates of neighbourhoods).

[F2]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

The quotient topology. Let (X,T) be a topological space (def-topological-space), let Y be a set and let q:XY be a surjection (def-injection-surjection-bijection). The quotient topology on Y induced by q is the final topology of the one-element family (q) (def-initial-and-final-topology): Tq  :=  {VY:q1[V]T}. 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, CY is closed in Tq exactly when q1[C] is closed in X, because q1[YV]=Xq1[V]. (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

[F4]

For a covering p:EB, a deck transformation is an isomorphism h:EE over B, so ph=p (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group Deck(p) under composition, and this group acts on E by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

[F5]

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).

[F6]

Let X and Y be topological spaces and let q:XY be continuous (def-continuous-map-top). Each of the following three conditions makes q a quotient map (def-quotient-topology). 1. q is a surjection and an open map (def-homeomorphism-and-open-maps). 2. q is a surjection and a closed map. 3. q admits a continuous section: a continuous s:YX with qs=idY. (Surjectivity of q 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

technique · direct
1.1

Let U be a neighbourhood whose nonidentity translates are disjoint. Each g acts by a homeomorphism of E by [F1], so every translate gU is open, and the full preimage of the orbit image of U is gGgU, 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.

givenF6F3F2F1
2.1

Each translate maps homeomorphically onto that quotient neighbourhood.

step 1.1F6F2F3
3.1

The action is free automatically, and when E is nonempty this embeds the acting group in the deck group: freeness makes ge=e force g=1, so distinct group elements give distinct translates. The nonemptiness is needed — on E= every translate is the identity, so a nontrivial G does not embed.

step 2.1F4F1F5
4.1

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.

step 3.1F4F5F1
5.1

The preceding construction and implications establish the assertion.

step 4.1

Depends on

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