LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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, e_{0}) \to (B, b_{0})$ be a connected covering of a path-connected locally path-connected base, and put

$G = π_{1} (B, b_{0}), H = p_{*} π_{1} (E, e_{0}) .$

For $g \in G$ , let $e_{g} = e_{0} \cdot g$ under right monodromy. A deck transformation $τ_{g}$ satisfying $τ_{g} (e_{0}) = e_{g}$ exists exactly when $g \in N_{G} (H)$ , and it is then unique. The assignment

$Θ : N_{G} (H) ⟶ Deck (E / B), g ⟼ τ_{g}$

is a surjective homomorphism. Two elements have the same image exactly when they determine the same coset $H g$ , 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 $e_{g}$ of the lift of a loop representing $g$ , the induced subgroup is $g^{- 1} H g$ (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 $N_{G} (H) = {g \in G : g H g^{- 1} = H}$ (The normalizer $N_{G} (H) = {g \in G : g H g^{- 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 \cdot 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, x_{0})$ under concatenation).

[F5]

The normalizer of a subgroup is itself a subgroup ( $C_{G} (x)$ and $N_{G} (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.1

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

F6given

2.1

By [L1], now licensed by step 1.1, the same covering based at $e_{g}$ has induced subgroup $g^{- 1} H g$ .

step 1.1L1F3

3.1

A deck transformation taking $e_{0}$ to $e_{g}$ is exactly a based isomorphism from $(E, e_{0})$ to $(E, e_{g})$ . By [L2], it exists exactly when $H = g^{- 1} H g$ , which by [F1] is exactly $g \in N_{G} (H)$ ; uniqueness follows from [F2].

step 2.1L2F1F2

4.1

For $g, g^{'} \in N_{G} (H)$ , [F2] gives $τ_{g} = τ_{g^{'}}$ exactly when $e_{0} \cdot g = e_{0} \cdot g^{'}$ . Applying the action by $g^{' - 1}$ reduces this to $e_{0} \cdot (g g^{' - 1}) = e_{0}$ , which holds exactly when the lifted loop closes at $e_{0}$ , equivalently when $g g^{' - 1} \in p_{*} π_{1} (E, e_{0}) = H$ . Thus $τ_{g} = τ_{g^{'}}$ exactly when $H g = H g^{'}$ . By step 1.1, given any point $e$ in the fibre, choose a path from $e_{0}$ to $e$ ; its projection is a loop at $b_{0}$ , and uniqueness in [F7] makes the lifted endpoint $e_{0} \cdot g$ equal to $e$ . Hence the monodromy orbit is the whole fibre, so step 3.1 and [F2] make $Θ$ surjective.

step 1.1step 3.1F2F3F7choose

5.1

By [F5], $N_{G} (H)$ is a group. Deck transformations commute with lifted endpoints: $τ_{g} (e_{0} \cdot h) = τ_{g} (e_{0}) \cdot h$ . Hence $(τ_{g} \circ τ_{h}) (e_{0}) = τ_{g} (e_{0} \cdot h) = (e_{0} \cdot g) \cdot h = e_{0} \cdot (g h) = τ_{g h} (e_{0}),$ so [F2] gives $τ_{g} τ_{h} = τ_{g h}$ and $Θ$ is a homomorphism. Its kernel consists of the $g$ with $e_{0} \cdot g = e_{0}$ . If $g = p_{*} [λ] \in H$ , the lift of a representative projected loop is the closed loop $λ$ , so it fixes $e_{0}$ ; conversely, if the lift of a representative of $g$ closes at $e_{0}$ , that lifted loop projects to $g$ and puts $g$ in $H$ . Thus $\ker Θ = H$ .

step 4.1F2F3F4F5∎

Depends on

Used by

Dependency tree · two levels

43 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

Allen Hatcher, Algebraic Topology, proof of Proposition 1.39 (standard reference, not scraped)