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 be a topological space, let and let be a path in from to (Paths, path-connected spaces and path components). Write 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 at (Based loops and the fundamental group) the concatenation is a loop at ; the bracketing of that triple product is immaterial up to path homotopy rel endpoints by step 1.2 below, and the bracket is used throughout. Then:
- The assignment is well defined: if rel endpoints (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints), then rel endpoints.
- is a group isomorphism (Group isomorphisms, automorphisms and the set ), and its two-sided inverse is
Consequently whenever a path from to exists, that is, whenever and lie in the same path component of ; 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 , points and a path from to .
A path in from to is a continuous map with and ; its reversal is and joins to ; composable paths concatenate by traversing each at double speed, and the constant path at a point is continuous (Paths, path-connected spaces and path components).
Based loops at are paths with , and is their set of path-homotopy classes rel endpoints; the product traverses first and second, is well defined, and makes a group whose identity is the class of the constant loop and in which (Based loops and the fundamental group, Loop classes form the group under concatenation).
A path homotopy relative to the endpoints from to is a continuous with , , and , 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).
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).
A bijective group homomorphism is a group isomorphism (Group isomorphisms, automorphisms and the set ).
Proof
Concatenation respects path homotopy rel endpoints. Let rel endpoints by and rel endpoints by , where and so that both concatenations are defined. Put for and for . At the two formulas give and by the rel-endpoints condition, and these agree because the middle endpoints agree; hence is a well-defined function on . The two closed sets and cover , and on each of them is a composite of or with the continuous affine map or , so [L4] makes continuous. Finally , , and , so is a path homotopy rel endpoints. A constant homotopy on one factor is the case , , so the same statement applies when only one of the two factors is deformed.
Reparametrisation does not change the class. Let be a path and let be continuous with and . Then is continuous because the argument is obtained from the continuous maps , and by products, sums and the continuous inclusion of in , and it satisfies , , and : the last two because and . 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 to the concatenations and 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.
A path cancels its reversal. Let be a path from to and put for and for . At both formulas give , and the two closed pieces cover , so [L4] makes continuous. One has , , and , so is a path homotopy rel endpoints, where is the constant path at the initial point. Applying the same statement to the reversed path , whose reversal is , gives rel endpoints.
Well-definedness of . By [F1] the path joins to and the concatenation is a loop at for every based loop at , 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 gives rel endpoints, and step 1.1 applied again to that homotopy and the constant homotopy of gives rel endpoints. Both are loops at , so their classes in coincide by [F2], and is independent of the representative of .
is a homomorphism. Let be based loops at . Then, using the product formula of [F2] and the bracketing freedom of step 1.2, where the second reduction replaces the loop at 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 is a group homomorphism.
is a two-sided inverse. The assignment is well defined by the argument of step 2.1 with replaced by , and it maps to . For a based loop at one has ; reassociating by step 1.2 and applying step 1.1 to insert the pairs, this class equals , and since is homotopic to the constant path at by step 1.3, deleting both constant factors with step 1.2 gives . Symmetrically, for a based loop at one has by the same two steps, because is homotopic to the constant path at by step 1.3. So the two composites are the identities.
Conclusion. Steps 2.1, 2.2 and 3.1 exhibit 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 to exists exactly when the two points lie in the same path component of by [F1].
Depends on
- Based loops and the fundamental group
- Loop classes form the group $\pi_1(X,x_0)$ under concatenation
- Paths, path-connected spaces and path components
- 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
- Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous
- Group isomorphisms, automorphisms and the set $\operatorname{Aut}(G)$
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
- Allen Hatcher, Algebraic Topology, section 1.1, printed p. 28, Proposition 1.5 (standard reference, not scraped)