ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

$π_{1} (R^{2} ∖ {0}) ≅ Z$

Example

Point $R^{2} ∖ {0}$ at $(1, 0)$ . Its fundamental group is infinite cyclic:

$π_{1} (R^{2} ∖ {0}, (1, 0)) ≅ (Z, +) .$

Facts & Assumptions

Given: The punctured plane $P = R^{2} ∖ {0}$ , its unit circle $C$ , and the basepoint $(1, 0) \in C$ .

[F1]

Radial normalization is a deformation retraction of $R^{n} ∖ {0}$ onto its unit sphere for every $n \geq 1$ (For $n \geq 1$ , radial normalisation is a deformation retraction of $R^{n} ∖ {0}$ onto $S^{n - 1}$ ).

[F2]

Induced fundamental-group maps respect identities, composition, and pointed homotopies (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F3]

The map $[t] \mapsto (\cos 2 π t, \sin 2 π t)$ is a homeomorphism from $R / Z$ to $C$ sending $[0]$ to $(1, 0)$ ( $[t] \mapsto (\cos 2 π t, \sin 2 π t)$ is a homeomorphism from $R / Z$ to the unit circle).

[F4]

The degree map is an isomorphism $π_{1} (R / Z, [0]) ≅ (Z, +)$ ( $Deg : π_{1} (R / Z, [0]) \to (Z, +)$ is an isomorphism).

Verification

technique · direct

1.1F1

Specializing [F1] to $n = 2$ gives a retraction $r : P \to C$ and an endpoint-fixed homotopy from ${id}_{P}$ to the composite of $r$ with the inclusion $i : C ↪ P$ , fixing $(1, 0)$ .

2.1step 1.1F2

Functoriality gives $r_{*} i_{*} = id$ and the pointed homotopy in step 1.1 gives $i_{*} r_{*} = id$ , so $i_{*}$ is an isomorphism $π_{1} (C, (1, 0)) ≅ π_{1} (P, (1, 0))$ .

3.1step 2.1F2F3F4∎

The pointed homeomorphism of [F3] induces an isomorphism from the quotient-circle fundamental group to $π_{1} (C, (1, 0))$ . Composing it with [F4] and the isomorphism of step 2.1 gives $π_{1} (P, (1, 0)) ≅ Z$ .

Depends on

Used by

The once-punctured two-sphere has trivial fundamental group and the twice-punctured two-sphere has fundamental group ℤ Example

Dependency tree · two levels

39 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, Chapter 1 (standard reference, not scraped)

π1(R2∖{0})≅Zπ1​(R2∖{0})≅Z