TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

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.

Loop classes form the group $π_{1} (X, x_{0})$ under concatenation

Statement

For every pointed topological space $(X, x_{0})$ , the product

$[α] [β] = [α * β]$

is well defined and makes $π_{1} (X, x_{0})$ a group. Its identity is the class of the constant loop $c_{x_{0}}$ , and $[α]^{- 1} = [\overset{ˉ}{α}]$ .

Facts & Assumptions

Given: A topological space $X$ , a basepoint $x_{0} \in X$ , and based loops at $x_{0}$ .

[L1]

The loop-class set, concatenation order, constant loop and reversed loop are those of Based loops and the fundamental group.

[L2]

Affine real coordinate maps are continuous, and finitely many continuous pieces agreeing on closed seams paste; hence the piecewise-affine reparametrisations used below are continuous. Reversal and constant paths are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, Paths, path-connected spaces and path components).

[L3]

A path homotopy is a continuous map $I \times I \to X$ that fixes both path endpoints throughout the homotopy (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[L4]

Maps into products are continuous exactly when their components are continuous, and composites of continuous maps are continuous (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1).

[L5]

For continuous maps into the convex line $R$ , the straight-line formula is a continuous homotopy (For continuous maps into a convex subset of $R^{n}$ , the straight-line formula defines a continuous homotopy).

[L6]

Continuous maps defined on finitely many closed sets and agreeing on overlaps paste to a continuous map (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 3).

[L7]

A group operation is associative, has a two-sided identity and gives every element a two-sided inverse (Group and abelian group).

Proof

technique · direct

1.1

If $A$ is an endpoint-fixed homotopy from $α_{0}$ to $α_{1}$ and $B$ one from $β_{0}$ to $β_{1}$ , define $K (s, t) = A (2 s, t)$ for $s \leq \frac{1}{2}$ and $K (s, t) = B (2 s - 1, t)$ for $s \geq \frac{1}{2}$ ; the clauses agree because $A (1, t) = x_{0} = B (0, t)$ , and [L2], [L4], and [L6] make $K$ continuous, so $α_{0} * β_{0}$ and $α_{1} * β_{1}$ are endpoint-homotopic. Thus the proposed product is independent of representatives.

L1L2L3L4L6

1.2

If $ϕ : I \to I$ is continuous with $ϕ (0) = 0$ and $ϕ (1) = 1$ , then [L5] makes $(s, t) \mapsto (1 - t) s + t ϕ (s)$ continuous. Composing with $α$ by [L4] gives a continuous $H (s, t) : = α ((1 - t) s + t ϕ (s))$ ; it takes values in $I$ , fixes $s = 0, 1$ , and joins $α$ to $α \circ ϕ$ . Hence endpoint-fixing reparametrisation preserves a path class.

L3L4L5

1.3

The formula $H (s, t) = α (2 s (1 - t))$ for $s \leq \frac{1}{2}$ and $H (s, t) = α (2 (1 - s) (1 - t))$ for $s \geq \frac{1}{2}$ is continuous by [L2], [L4], and [L6], fixes both endpoints at $x_{0}$ , starts at $α * \overset{ˉ}{α}$ , and ends at $c_{x_{0}}$ ; applying the same construction to $\overset{ˉ}{α}$ contracts $\overset{ˉ}{α} * α$ .

L1L2L3L4L6

2.1

Put $w : = (α * β) * γ$ and define $ϕ (s) = s / 2$ for $0 \leq s \leq \frac{1}{2}$ , $ϕ (s) = s - \frac{1}{4}$ for $\frac{1}{2} \leq s \leq \frac{3}{4}$ , and $ϕ (s) = 2 s - 1$ for $\frac{3}{4} \leq s \leq 1$ ; [L2] makes this continuous, the clauses agree at the seams, $ϕ$ fixes $0, 1$ , and direct substitution gives $w \circ ϕ = α * (β * γ)$ , so step 1.2 proves associativity on classes.

step 1.2L1L2

2.2

For $ϕ_{R} (s) = \min {2 s, 1}$ one has $α \circ ϕ_{R} = α * c_{x_{0}}$ , and for $ϕ_{L} (s) = \max {2 s - 1, 0}$ one has $α \circ ϕ_{L} = c_{x_{0}} * α$ ; these continuous endpoint-fixing maps and step 1.2 show that $[c_{x_{0}}]$ is a two-sided identity.

step 1.2L1L2

3.1

Step 1.1 gives a well-defined operation, step 2.1 gives associativity, step 2.2 gives the identity, and step 1.3 gives the two-sided inverse $[\overset{ˉ}{α}]$ ; these are exactly the axioms in [L7], so $π_{1} (X, x_{0})$ is a group.

step 1.1step 1.3step 2.1step 2.2L7∎

Depends on

Used by

Cited to discharge well-definedness by Based loops and the fundamental group.

Dependency tree · two levels

47 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

A. Hatcher, Algebraic Topology, Chapter 1, Proposition 1.3 (standard reference, not scraped)

Loop classes form the group π1(X,x0)π1​(X,x0​) under concatenation