Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

A connected covering is regular exactly when its induced subgroup is normal, exactly when deck transformations act transitively on a fibre

Statement

Let p:(E,e0)→(B,b0) be a covering with path-connected total space and path-connected locally path-connected base. Put

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

The following are equivalent:

  1. p is regular (Regular coverings);
  2. H⊴G;
  3. Deck⁡(E/B) acts transitively on the fibre p−1(b0).

No finiteness hypothesis is imposed on the fibre or on the index of H.

Facts & Assumptions

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

[L1]

The subgroup at the endpoint e0⋅g of a lifted loop is g−1Hg (Changing the point over a fixed basepoint conjugates the induced covering subgroup).

[L2]

A deck transformation sends e0 to e0⋅g exactly when g∈NG(H) (Deck transformations of a connected covering correspond to cosets in the subgroup normalizer).

[F1]

A subgroup is normal exactly when it is preserved under conjugation by every group element (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

[F2]

In a path-connected covering, the right-monodromy orbit through a fibre point is the whole fibre (Monodromy acts by fibre bijections, and its orbits are the intersections of path components with the fibre).

[F3]

A path has a unique lift from each prescribed point over its initial point (Existence and uniqueness of path lifts through a covering map).

Proof

technique · direct
1.1L1F2

By [F2], every point of p−1(b0) has the form e0⋅g for some g∈G, and [L1] records the subgroup at that point.

2.1step 1.1L2F1

By [L2], a deck transformation reaches e0⋅g from e0 exactly when g normalizes H. Hence the deck action on p−1(b0) is transitive exactly when NG(H)=G, which by [F1] is exactly when H⊴G. This proves the equivalence of clauses 2 and 3.

3.1step 2.1F3

For the implication from normality to regularity, clause 2 gives clause 3 by step 2.1. Let e,e′ lie over an arbitrary b∈B, choose a path from b to b0, and lift it from e,e′ to points u,u′ over b0. Clause 3 gives a deck transformation τ with τ(u)=u′. Applying τ to the reverse lift from u produces a lift from u′, so uniqueness in [F3] gives τ(e)=e′. Thus the deck group is transitive on every fibre and the covering is regular.

4.1step 2.1F1∎

For the converse implication from regularity, the definition makes the deck action transitive on p−1(b0), so clause 3 holds. Step 2.1 then gives NG(H)=G, and [F1] gives H⊴G. Thus clauses 1, 2, and 3 are equivalent.

Depends on

Used by

Dependency tree · two levels

30 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