LemmaStatement: 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.

Changing the point over a fixed basepoint conjugates the induced covering subgroup

Statement

Let $p : E \to B$ be a covering with path-connected total space, and let $e_{0}, e_{1} \in p^{- 1} (b_{0})$ . If $\tilde{γ}$ is a path from $e_{0}$ to $e_{1}$ and $γ = p \circ \tilde{γ}$ , then, with traversal-order multiplication,

$p_{*} π_{1} (E, e_{1}) = [γ]^{- 1} (p_{*} π_{1} (E, e_{0})) [γ] .$

Every point $e_{1}$ in the fibre arises in this way from some path $\tilde{γ}$ .

Facts & Assumptions

Given: The covering, fibre points, and connecting path in the Statement; write $H_{i} = p_{*} π_{1} (E, e_{i})$ and $g = [γ]$ .

[F1]

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

[F2]

Traversal-order concatenation gives multiplication of loop classes and reversal gives inversion (Loop classes form the group $π_{1} (X, x_{0})$ under concatenation).

[F3]

A path-connected space contains a path between every pair of its points (Paths, path-connected spaces and path components).

Proof

technique · direct

1.1F2

If $[λ] \in π_{1} (E, e_{1})$ , then $\tilde{γ} * λ * \overset{ˉ}{\tilde{γ}}$ is a loop at $e_{0}$ . Its projection represents $g p_{*} [λ] g^{- 1}$ by [F2], so $g H_{1} g^{- 1} \subseteq H_{0}$ .

2.1step 1.1F2

Apply step 1.1 to the reversed path from $e_{1}$ to $e_{0}$ . This gives $g^{- 1} H_{0} g \subseteq H_{1}$ , while conjugating the first inclusion by $g^{- 1}$ and $g$ gives the reverse containment. Hence $H_{1} = g^{- 1} H_{0} g$ , with the displayed direction fixed by traversal order.

3.1F1F3choose∎

For an arbitrary $e_{1} \in p^{- 1} (b_{0})$ , path-connectedness and [F3] supply a path from $e_{0}$ to $e_{1}$ ; its projection begins and ends at $b_{0}$ , hence is a loop. Conversely, [F1] says the endpoint of the lift of that loop from $e_{0}$ is the prescribed $e_{1}$ .

Depends on

Used by

Dependency tree · two levels

29 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 Theorem 1.38 (standard reference, not scraped)