LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Pointwise multiplication and concatenation of loops in a topological group agree up to homotopy

Statement

Let $G$ be a topological group with identity $e$ , and let $α, β : [0, 1] \to G$ be loops based at $e$ . Their pointwise product $(α \cdot β) (t) = α (t) β (t)$ is endpoint-fixed homotopic both to $α * β$ and to $β * α$ . Consequently pointwise multiplication descends to loop classes and agrees there with loop concatenation.

Facts & Assumptions

Given: A topological group $G$ with identity $e$ and based loops $α, β$ at $e$ .

[F1]

Multiplication $m : G \times G \to G$ , $m (x, y) = x y$ , is continuous (Topological group: multiplication and inversion are continuous).

[F2]

The product $[α] [β]$ traverses $α$ first and $β$ second, using the concatenated loop $α * β$ (Based loops and the fundamental group).

[F3]

An endpoint-fixed path homotopy is a continuous map $H : [0, 1]^{2} \to G$ that keeps the two path endpoints fixed throughout (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[L1]

A map into a product is continuous exactly when all its components 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).

[L2]

Maps continuous on the members of a finite closed cover 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).

[L3]

Finite sums, products, maxima, and minima of continuous real-valued maps are continuous, and quotients are continuous wherever their denominators do not vanish (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

Proof

technique · constructive

1.1

The map $K : [0, 1]^{2} \to G$ , $K (s, t) = α (s) β (t)$ , is continuous, and $K (0, 0) = K (1, 0) = K (0, 1) = K (1, 1) = e$ .

givenF1L1construct

2.1

For $u, t \in [0, 1]$ , put $A_{u} (t) = \min {\frac{t}{1 - u / 2}, 1}, B_{u} (t) = \max {\frac{t - u / 2}{1 - u / 2}, 0} .$ Since $1 - u / 2 \geq 1 / 2$ , [L2] and [L3] make these functions continuous on the parameter square. Hence $H_{1} (t, u) = K (A_{u} (t), B_{u} (t))$ is an endpoint-fixed homotopy: at $u = 0$ it is $α (t) β (t)$ , and at $u = 1$ it traverses $α$ first and $β$ second, so it is $α * β$ under [F2].

step 1.1F2F3L1L2L3

3.1

The formula $H_{2} (t, u) = K (B_{u} (t), A_{u} (t))$ is another endpoint-fixed homotopy. At $u = 0$ it is again $α (t) β (t)$ , while at $u = 1$ it traverses $β$ first and $α$ second, so it is $β * α$ .

step 1.1step 2.1F2F3

4.1

If $α$ or $β$ is replaced by an endpoint-fixed homotopic loop, multiplying the two homotopies pointwise gives an endpoint-fixed homotopy by [F1] and [L1]. Thus pointwise multiplication is well defined on loop classes, and steps 2.1 and 3.1 identify it with both concatenation orders.

step 2.1step 3.1F1L1discharge-construct∎

Depends on

Used by

The fundamental group of a topological group is abelian Theorem

Dependency tree · two levels

24 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

J. Peter May, A Concise Course in Algebraic Topology, Chapter 1, Problem 3 (standard reference, not scraped)