Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

Deck transformations of a connected covering correspond to cosets in the subgroup normalizer

Statement

Let p:(E,e0)→(B,b0) be a connected covering of a path-connected locally path-connected base, and put

G=π1(B,b0),H=p∗π1(E,e0).

For g∈G, let eg=e0⋅g under right monodromy. A deck transformation τg satisfying τg(e0)=eg exists exactly when g∈NG(H), and it is then unique. The assignment

Θ:NG(H)⟶Deck⁡(E/B),g⟼τg

is a surjective homomorphism. Two elements have the same image exactly when they determine the same coset Hg, and ker⁡Θ=H.

Facts & Assumptions

Given: The based connected covering and groups G,H in the Statement.

[L1]

For a covering with path-connected total space, at the endpoint eg of the lift of a loop representing g, the induced subgroup is g−1Hg (Changing the point over a fixed basepoint conjugates the induced covering subgroup).

[L2]

Two based connected coverings are based-isomorphic exactly when their induced subgroups are equal (Based connected coverings are isomorphic exactly when their induced subgroups are equal).

[F1]

The normalizer is NG(H)={g∈G:gHg−1=H} (The normalizer NG(H)={g∈G:gHg−1=H} of a subgroup).

[F2]

Two deck transformations of a connected covering 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).

[F3]

Right monodromy sends (e,g) to the endpoint e⋅g of the lift of a representative loop (The monodromy right action on a covering fibre and its equivalent left-action convention).

[F4]

Traversal-order concatenation gives multiplication in the fundamental group (Loop classes form the group π1(X,x0) under concatenation).

[F5]

The normalizer of a subgroup is itself a subgroup (CG(x) and NG(H) are subgroups of G).

[F6]

Local path-connectedness lifts along a covering, and a connected locally path-connected space is path-connected (Local path-connectedness lifts and descends along covering maps, A connected, locally path-connected space is path-connected, because its path components are open).

[F7]

Every path in the base has a unique lift from a prescribed point in the fibre (Existence and uniqueness of path lifts through a covering map).

Proof

technique · direct
1.1F6given

Local path-connectedness of the base lifts to E, and connectedness then makes E path-connected by [F6].

2.1step 1.1L1F3

By [L1], now licensed by step 1.1, the same covering based at eg has induced subgroup g−1Hg.

3.1step 2.1L2F1F2

A deck transformation taking e0 to eg is exactly a based isomorphism from (E,e0) to (E,eg). By [L2], it exists exactly when H=g−1Hg, which by [F1] is exactly g∈NG(H); uniqueness follows from [F2].

4.1step 1.1step 3.1F2F3F7choose

For g,g′∈NG(H), [F2] gives τg=τg′ exactly when e0⋅g=e0⋅g′. Applying the action by g′−1 reduces this to e0⋅(gg′−1)=e0, which holds exactly when the lifted loop closes at e0, equivalently when gg′−1∈p∗π1(E,e0)=H. Thus τg=τg′ exactly when Hg=Hg′. By step 1.1, given any point e in the fibre, choose a path from e0 to e; its projection is a loop at b0, and uniqueness in [F7] makes the lifted endpoint e0⋅g equal to e. Hence the monodromy orbit is the whole fibre, so step 3.1 and [F2] make Θ surjective.

5.1step 4.1F2F3F4F5∎

By [F5], NG(H) is a group. Deck transformations commute with lifted endpoints: τg(e0⋅h)=τg(e0)⋅h. Hence (τg∘τh)(e0)=τg(e0⋅h)=(e0⋅g)⋅h=e0⋅(gh)=τgh(e0), so [F2] gives τgτh=τgh and Θ is a homomorphism. Its kernel consists of the g with e0⋅g=e0. If g=p∗[λ]∈H, the lift of a representative projected loop is the closed loop λ, so it fixes e0; conversely, if the lift of a representative of g closes at e0, that lifted loop projects to g and puts g in H. Thus ker⁡Θ=H.

Depends on

Used by

Dependency tree · two levels

46 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