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.

Induced fundamental-group maps are well defined, functorial and invariant under based homotopy

Statement

Let $f : (X, x_{0}) \to (Y, y_{0})$ be a continuous map with $f (x_{0}) = y_{0}$ . Then

$f_{*} ([α]) = [f \circ α]$

is a well-defined group homomorphism. For pointed continuous maps,

${id}_{*} = id, (g \circ f)_{*} = g_{*} \circ f_{*} .$

If $f_{0}, f_{1} : (X, x_{0}) \to (Y, y_{0})$ are homotopic through a homotopy that keeps $x_{0}$ at $y_{0}$ , then $(f_{0})_{*} = (f_{1})_{*}$ .

Facts & Assumptions

Given: Pointed continuous maps between pointed topological spaces and based loops in their domains.

[L1]

The proposed induced map sends $[α]$ to $[f \circ α]$ (The homomorphism on fundamental groups induced by a pointed continuous map).

[L2]

Postcomposition preserves homotopies, and precomposition preserves a homotopy relative to a subspace whose image lies in the fixed subspace (Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form).

[L3]

Loop multiplication traverses the first loop and then the second, using the explicit two-piece concatenation formula (Based loops and the fundamental group).

[L4]

A map between groups is a group homomorphism exactly when it preserves products, and the loop-class operations in question are groups (Monoid homomorphism and group homomorphism, Loop classes form the group $π_{1} (X, x_{0})$ under concatenation).

Proof

technique · direct

1.1

If $α_{0}$ and $α_{1}$ are endpoint-homotopic, postcomposing their homotopy by $f$ gives an endpoint-homotopy from $f \circ α_{0}$ to $f \circ α_{1}$ by [L2]; hence the formula in [L1] is independent of the representative.

L1L2

1.2

The concatenation formulas give the literal equality $f \circ (α * β) = (f \circ α) * (f \circ β)$ , so $f_{*} ([α] [β]) = f_{*} ([α]) f_{*} ([β])$ ; thus $f_{*}$ is a group homomorphism.

L1L3L4

1.3

For every loop $α$ , $id \circ α = α$ and $(g \circ f) \circ α = g \circ (f \circ α)$ , which proves the identity and composition formulas on every loop class.

1.4

If $H$ is a homotopy from $f_{0}$ to $f_{1}$ fixing $x_{0}$ , precomposition by a based loop $α$ gives an endpoint-fixed path homotopy from $f_{0} \circ α$ to $f_{1} \circ α$ by [L2], so $(f_{0})_{*} ([α]) = (f_{1})_{*} ([α])$ .

L1L2

2.1

Steps 1.1--1.4 prove well-definedness, the homomorphism law, functoriality and based-homotopy invariance.

step 1.1step 1.2step 1.3step 1.4∎

Depends on

Used by

Cited to discharge well-definedness by The homomorphism on fundamental groups induced by a pointed continuous map.

Dependency tree · two levels

18 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, Induced Homomorphisms (standard reference, not scraped)