Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21
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.

Every subgroup acts on the universal cover with a connected quotient covering that realizes it

Statement

Let B be nonempty, path-connected, locally path-connected, and semilocally simply connected, fix b0∈B, and put G=π1(B,b0). For every subgroup H≤G, there is a based connected covering

pH:(EH,eH)⟶(B,b0)

such that (pH)∗π1(EH,eH)=H. It is obtained by letting H act through deck transformations on a universal cover B~ and taking EH=B~/H.

Facts & Assumptions

Given: The base B, basepoint b0, group G, and subgroup H in the Statement.

[F2]

With traversal-order multiplication, G is isomorphic to the universal deck group by the assignment taking a loop class to the deck transformation that moves a chosen fibre point to its lifted endpoint, with no path reversal (For a path-connected locally path-connected semilocally simply connected base, the deck group of a universal cover is isomorphic to the fundamental group).

[F4]

Monodromy is the right action in which e⋅[α] is the endpoint of the lift of α from e (The monodromy right action on a covering fibre and its equivalent left-action convention).

[F5]

A covering-space action is an action by homeomorphisms with neighbourhoods disjoint from every nonidentity translate (Covering-space actions by disjoint translates of neighbourhoods).

[F6]

A covering is locally a disjoint union of sheets, each mapped homeomorphically to one evenly covered neighbourhood (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F7]

On a covering with connected total space, two deck transformations that agree at one point are equal (On a connected covering space, a deck transformation is determined by one point and the deck action is free).

Proof

technique · constructive
1.1F1F2F5F6F7

Fix a universal cover p:(B~,b~0)→(B,b0) by [F1], and use [F2] to regard H as a subgroup of its deck group. Over an evenly covered neighbourhood of b∈B, choose the sheet containing a given b~. A nonidentity deck transformation sends it to a different sheet: otherwise it would send the unique point over b in that sheet to itself and hence be the identity by [F7]. Thus [F5] holds, so the restricted H-action is a covering-space action.

2.1step 1.1F3F6construct

Let q:B~→EH:=B~/H be the orbit map, which is a covering by [F3]. Since p is constant on H-orbits, it induces pH:EH→B. Over an evenly covered W⊆B, the H-orbits of the sheets of p−1(W) have disjoint images under q, and on each such image pH is identified with the homeomorphism from any representative sheet to W. Hence pH is a covering by [F6]. The path-connected space B~ maps continuously and surjectively to EH, so EH is path-connected, with basepoint eH=q(b~0).

3.1step 2.1F2F4discharge-construct∎

For a loop α at b0, its lift to EH from eH is q∘α~, where α~ is its universal lift. This lift closes exactly when the universal endpoint lies in the H-orbit of b~0, which by [F2] and [F4] holds exactly when [α]∈H. A loop class is in (pH)∗π1(EH,eH) exactly when it has a closed lift to EH, so the induced subgroup is precisely H.

Depends on

Used by

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources