Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27
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.

Conjugating loop classes by a path is an isomorphism of fundamental groups

Statement

Let X be a topological space, let x0,x1∈X and let c:I→X be a path in X from x0 to x1 (Paths, path-connected spaces and path components). Write cˉ(s):=c(1−s) for the reversed path and let ∗ denote the first-then-second concatenation of composable paths of Paths, path-connected spaces and path components, so that for every based loop α:I→X at x0 (Based loops and the fundamental group) the concatenation cˉ∗α∗c is a loop at x1; the bracketing of that triple product is immaterial up to path homotopy rel endpoints by step 1.2 below, and the bracket (cˉ∗α)∗c is used throughout. Then:

  1. The assignment φc:π1(X,x0)⟶π1(X,x1),φc([α]):=[(cˉ∗α)∗c], is well defined: if α≃α′ rel endpoints (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints), then (cˉ∗α)∗c≃(cˉ∗α′)∗c rel endpoints.
  2. φc is a group isomorphism (Group isomorphisms, automorphisms and the set Aut⁡(G)), and its two-sided inverse is φcˉ:π1(X,x1)⟶π1(X,x0),φcˉ([β]):=[(c∗β)∗cˉ].

Consequently π1(X,x0)≅π1(X,x1) whenever a path from x0 to x1 exists, that is, whenever x0 and x1 lie in the same path component of X; the isomorphism depends on the chosen path, and no claim is made that it is independent of that choice.

Facts & Assumptions

Given: A topological space X, points x0,x1∈X and a path c:I→X from x0 to x1.

[F1]

A path in X from x to y is a continuous map γ:I→X with γ(0)=x and γ(1)=y; its reversal is γˉ(t)=γ(1−t) and joins y to x; composable paths concatenate by traversing each at double speed, and the constant path at a point x is continuous (Paths, path-connected spaces and path components).

[F2]

Based loops at x0 are paths α:I→X with α(0)=x0=α(1), and π1(X,x0) is their set of path-homotopy classes rel endpoints; the product [α][β]=[α∗β] traverses α first and β second, is well defined, and makes π1(X,x0) a group whose identity is the class of the constant loop cx0 and in which [α]−1=[αˉ] (Based loops and the fundamental group, Loop classes form the group π1(X,x0) under concatenation).

[L3]

A path homotopy relative to the endpoints from α to α′ is a continuous H:I×I→X with H(s,0)=α(s), H(s,1)=α′(s), H(0,t)=α(0) and H(1,t)=α(1), and this relation is an equivalence relation on paths with fixed endpoints (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Homotopy relative to a fixed subspace, and path homotopy relative to endpoints, are equivalence relations).

[L4]

A map is continuous when its restrictions to the members of a finite closed cover are continuous and agree on overlaps; composites and restrictions of continuous maps are continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L5]

A bijective group homomorphism is a group isomorphism (Group isomorphisms, automorphisms and the set Aut⁡(G)).

Proof

technique · direct
1.1

Concatenation respects path homotopy rel endpoints. Let α≃α′ rel endpoints by H and β≃β′ rel endpoints by K, where α(1)=β(0) and α′(1)=β′(0) so that both concatenations are defined. Put G(s,t):=H(2s,t) for 0≤s≤12 and G(s,t):=K(2s−1,t) for 12≤s≤1. At s=12 the two formulas give H(1,t)=α(1) and K(0,t)=β(0) by the rel-endpoints condition, and these agree because the middle endpoints agree; hence G is a well-defined function on I×I. The two closed sets [0,12]×I and [12,1]×I cover I×I, and on each of them G is a composite of H or K with the continuous affine map (s,t)↦(2s,t) or (s,t)↦(2s−1,t), so [L4] makes G continuous. Finally G(s,0)=α∗β(s), G(s,1)=α′∗β′(s), G(0,t)=α(0)=α′(0) and G(1,t)=β(1)=β′(1), so G is a path homotopy α∗β≃α′∗β′ rel endpoints. A constant homotopy on one factor is the case β=β′, K(s,t):=β(s), so the same statement applies when only one of the two factors is deformed.

F1L3L4
1.2

Reparametrisation does not change the class. Let λ:I→X be a path and let φ:I→I be continuous with φ(0)=0 and φ(1)=1. Then H(s,t):=λ((1−t)φ(s)+ts) is continuous because the argument is obtained from the continuous maps s↦φ(s), s↦s and t↦t by products, sums and the continuous inclusion of I in R, and it satisfies H(s,0)=λ(φ(s)), H(s,1)=λ(s), H(0,t)=λ(0) and H(1,t)=λ(1): the last two because φ(0)=0 and φ(1)=1. So λ∘φ≃λ rel endpoints. Consequently the two bracketings of a triple concatenation of composable paths are reparametrisations of one another, so they are path-homotopic rel endpoints, and for a path λ from x to y the concatenations λ∗cy and cx∗λ with the constant paths at the endpoints are reparametrisations of λ, so both are path-homotopic to λ rel endpoints. Hence constant factors may be inserted and deleted inside a larger concatenation up to path homotopy rel endpoints.

F1L3L4
1.3

A path cancels its reversal. Let λ:I→X be a path from x to y and put H(s,t):=λ(2s(1−t)) for 0≤s≤12 and H(s,t):=λ(2(1−s)(1−t)) for 12≤s≤1. At s=12 both formulas give λ(1−t), and the two closed pieces cover I×I, so [L4] makes H continuous. One has H(s,0)=λ∗λˉ(s), H(s,1)=λ(0)=x, and H(0,t)=λ(0)=x=H(1,t), so H is a path homotopy λ∗λˉ≃cx rel endpoints, where cx is the constant path at the initial point. Applying the same statement to the reversed path λˉ, whose reversal is λ, gives λˉ∗λ≃cy rel endpoints.

F1L3L4
2.1

Well-definedness of φc. By [F1] the path cˉ joins x1 to x0 and the concatenation (cˉ∗α)∗c is a loop at x1 for every based loop α at x0, so the formula of the statement defines a function on the set of based loops. Let α≃α′ rel endpoints. Step 1.1 applied to the pair α≃α′ and the constant homotopy of cˉ gives cˉ∗α≃cˉ∗α′ rel endpoints, and step 1.1 applied again to that homotopy and the constant homotopy of c gives (cˉ∗α)∗c≃(cˉ∗α′)∗c rel endpoints. Both are loops at x1, so their classes in π1(X,x1) coincide by [F2], and φc is independent of the representative of [α].

step 1.1F1F2L3
2.2

φc is a homomorphism. Let α,β be based loops at x0. Then, using the product formula of [F2] and the bracketing freedom of step 1.2, φc([α])φc([β])=[(cˉ∗α∗c)∗(cˉ∗β∗c)]≃[(cˉ∗α)∗(c∗cˉ)∗(β∗c)]≃[(cˉ∗α)∗(β∗c)]≃[cˉ∗(α∗β)∗c]=φc([α][β]), where the second reduction replaces the loop c∗cˉ at x0 by a constant path using step 1.3 and deletes that constant factor using step 1.2, and where each replacement is licensed inside the ambient concatenation by step 1.1. Hence φc is a group homomorphism.

step 1.1step 1.2step 1.3F2
3.1

φcˉ is a two-sided inverse. The assignment φcˉ([β]):=[(c∗β)∗cˉ] is well defined by the argument of step 2.1 with c replaced by cˉ, and it maps π1(X,x1) to π1(X,x0). For a based loop α at x0 one has φcˉ(φc([α]))=[c∗((cˉ∗α)∗c)∗cˉ]; reassociating by step 1.2 and applying step 1.1 to insert the pairs, this class equals [(c∗cˉ)∗α∗(c∗cˉ)], and since c∗cˉ is homotopic to the constant path at x0 by step 1.3, deleting both constant factors with step 1.2 gives [α]. Symmetrically, for a based loop β at x1 one has φc(φcˉ([β]))=[cˉ∗((c∗β)∗cˉ)∗c]≃[(cˉ∗c)∗β∗(cˉ∗c)]=[β] by the same two steps, because cˉ∗c is homotopic to the constant path at x1 by step 1.3. So the two composites are the identities.

step 1.1step 1.2step 1.3step 2.1F2
4.1

Conclusion. Steps 2.1, 2.2 and 3.1 exhibit φc as a well-defined group homomorphism with a two-sided inverse, hence a bijection, and [L5] makes it a group isomorphism. The final assertion follows because a path from x0 to x1 exists exactly when the two points lie in the same path component of X by [F1].

step 2.1step 2.2step 3.1F1L5∎

Depends on

Used by

Dependency tree · two levels

27 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