Alphabeta Math
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.

✓ 16 results · all verified · 11 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Applications of the Fundamental Group

1 · Prerequisites

2 · Summary

Functoriality of induced fundamental-group maps, the calculation π1(S1)≅Z, and simple connectedness of higher-dimensional spheres turn geometric constructions into algebraic obstructions. Radial deformation retractions identify punctured Euclidean spaces with spheres, while path lifting for R→R/Z controls circle maps. Componentwise continuity and the algebra of continuous real maps justify the explicit disk and polynomial constructions.

Retract functoriality gives the disk no-retraction theorem and, through an explicit ray formula, Brouwer's fixed-point theorem. Normalized polynomial loops yield a fundamental-group proof of the fundamental theorem of algebra. Odd lift increments give Borsuk–Ulam and its planar consequences. The two loop products in a topological group force its fundamental group to be abelian. Punctured-space calculations distinguish R2 from Rn for n≥3, separate arguments handle n=0,1, and the Hawaiian earring is shown to be compact and path-connected.

3 · Logical flowchart

4 · Definitions, theorems and proofs

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism

Statement

Let A⊆X, let i:A↪X be the inclusion, and choose a∈A. If A is a retract of X (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise), then

i∗:π1(A,a)⟶π1(X,a)

is injective. If A is a deformation retract of X, the inclusion and retraction induce mutually inverse fundamental-group isomorphisms at every basepoint of A.

Facts & Assumptions

Given: A subspace A⊆X, its inclusion i:A↪X, a basepoint a∈A, and a retraction r:X→A; in the second clause, a deformation retraction from X onto A.

[F1]

A continuous map r:X→A is a retraction when r∘i=id⁡A; for a deformation retract, id⁡X is homotopic to i∘r through a homotopy that fixes every point of A (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

[L1]

For pointed continuous maps, id⁡∗=id⁡ and (g∘f)∗=g∗∘f∗; pointed-homotopic maps induce the same homomorphism on fundamental groups (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

Proof

technique · direct
1.1givenF1

Since a∈A, both i:(A,a)→(X,a) and r:(X,a)→(A,a) are pointed, and r∘i=id⁡A.

2.1step 1.1L1algebra

Functoriality gives r∗∘i∗=(r∘i)∗=id⁡, so i∗ has a left inverse and is injective.

3.1step 2.1F1L1∎

If A is a deformation retract, the homotopy from id⁡X to i∘r fixes a, so [L1] also gives i∗∘r∗=(i∘r)∗=id⁡; hence i∗ and r∗ are mutually inverse isomorphisms.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

There is no retraction of the closed disk onto the unit circle

Statement

Write D2=B‾2(0,1)⊆R2 and S1=S2(0,1) (Euclidean spheres and closed balls as subspaces of Rn). There is no continuous retraction from the closed unit disk D2 onto the unit circle S1.

Facts & Assumptions

Given: The closed unit disk D2, the unit circle S1, the common basepoint e0=(1,0), and the inclusion i:S1↪D2.

[L1]

If A is a retract of X, then the inclusion induces an injective homomorphism on fundamental groups at every basepoint of A (A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism).

[F1]

The closed unit disk and unit circle are respectively the Euclidean closed ball B‾2(0,1) and Euclidean sphere S2(0,1) (Euclidean spheres and closed balls as subspaces of Rn).

[L2]

Every nonempty convex subset of Rn is simply connected (Every nonempty convex subset of Rn is simply connected).

[L3]

For the geometric unit circle S1 based at (1,0), π1(S1,(1,0))≅(Z,+) (The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))≅Z).

Proof

technique · contradiction
1.1F1L2L4algebra

The disk D2 is nonempty and convex: if x,y∈D2 and 0≤t≤1, then ∥(1−t)x+ty∥2≤(1−t)∥x∥2+t∥y∥2≤1. Hence π1(D2,e0) has one element.

1.2F1L3

The unit circle has π1(S1,e0) isomorphic to the nontrivial group Z.

1.3assume-contra

Suppose a retraction r:D2→S1 existed.

2.1step 1.1step 1.2step 1.3L1discharge-contradiction∎

By [L1], i∗:π1(S1,e0)→π1(D2,e0) would be injective, but steps 1.1 and 1.2 make this a homomorphism from a nontrivial group to a one-element group, which cannot be injective. Thus no such retraction exists.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-24Open item page →

A fixed-point-free self-map of the disk produces a continuous retraction onto the unit circle

Statement

Let D2=B‾2(0,1) and S1=S2(0,1). Every continuous fixed-point-free map f:D2→D2 determines a continuous retraction D2→S1.

Facts & Assumptions

Given: A continuous map f:D2→D2 such that f(x)≠x for every x∈D2.

[F1]

The closed unit disk and unit circle are D2={x:∥x∥2≤1} and S1={x:∥x∥2=1} (Euclidean spheres and closed balls as subspaces of Rn).

[L1]

The Euclidean inner product is bilinear and positive definite, with ∥u∥22=⟨u,u⟩ (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

[L2]

A map into R2 is continuous exactly when its coordinate functions are continuous; finite sums, scalar multiples, inner products, and norms of continuous vector-valued functions are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L3]

Finite sums and products of continuous real-valued maps are continuous, and a quotient is continuous wherever its denominator is nonzero (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[F2]

A continuous map r:D2→S1 is a retraction when r(x)=x for every x∈S1 (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

Proof

technique · constructive
1.1givenF1L1L4construct

For x∈D2, put a=f(x), v=x−a, A=⟨v,v⟩, B=⟨a,v⟩, and C=⟨a,a⟩. Fixed-point-freeness gives v≠0 and A>0. Define λ(x)=−B+B2+A(1−C)A,r(x)=a+λ(x)v.

2.1step 1.1F1L1algebra

The equation ∥a+tv∥22=1 is At2+2Bt+C−1=0, whose discriminant is 4(B2+A(1−C))≥0 because C=∥f(x)∥22≤1; thus λ(x) is its larger root. Since the upward-opening quadratic is nonpositive at both t=0 and t=1, its larger root satisfies λ(x)≥1 and is the unique intersection parameter of the ray a+tv with S1 for t≥1.

3.1step 1.1step 2.1L2L3L4

The maps a,v,A,B,C are continuous; the radicand is nonnegative, its square root is continuous, and the denominator A never vanishes. Hence λ is continuous, and componentwise continuity makes r(x)=a+λ(x)v continuous.

4.1step 2.1step 3.1F1F2discharge-construct∎

Step 2.1 gives ∥r(x)∥2=1, so r maps D2 into S1. If x∈S1, then t=1 is a root and is the larger root because 1≥0 lies in the interval on which the quadratic is nonpositive; hence λ(x)=1 and r(x)=a+v=x. Therefore r is a continuous retraction of D2 onto S1.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Brouwer fixed-point theorem for the closed disk

Statement

Every continuous map f:D2→D2 from the closed unit disk to itself has a fixed point: there is an x∈D2 such that f(x)=x.

Facts & Assumptions

Given: A continuous map f:D2→D2.

[L1]

Every continuous fixed-point-free map f:D2→D2 determines a continuous retraction D2→S1 (A fixed-point-free self-map of the disk produces a continuous retraction onto the unit circle).

[L2]

There is no continuous retraction from the closed unit disk D2 onto its boundary circle S1 (There is no retraction of the closed disk onto the unit circle).

Proof

technique · contradiction
1.1givenassume-contra

Suppose that f has no fixed point, so f(x)≠x for every x∈D2.

2.1step 1.1L1L2discharge-contradiction∎

By [L1], the map f then determines a continuous retraction D2→S1, contradicting [L2]. Therefore f has a fixed point.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

A root-free complex polynomial gives nullhomotopic normalized circle loops

Statement

Let p be a complex polynomial with no zero in C. For each real R≥0, evaluate p on the circle of radius R, divide by its value at the basepoint R, and radially normalize to the unit circle. Transported through the homeomorphism h:R/Z→S1, this is a based circle loop αR, and every αR is nullhomotopic. In particular, every such loop has degree zero.

Facts & Assumptions

Given: A complex polynomial p such that p(z)≠0 for every z∈C, a real R≥0, and the unit-circle homeomorphism h:R/Z→S1.

[F1]

A complex polynomial is a finite coefficient list, and its evaluation at z∈C is the corresponding finite sum of powers of z (Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials).

[F2]

Under C=R2, complex continuity is continuity for the Euclidean metric (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).

[L1]

Complex modulus satisfies ∣zw∣=∣z∣∣w∣, ∣z∣=0 exactly when z=0, and ∣z+w∣≤∣z∣+∣w∣ (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L2]

The map h:R/Z→S1, h([t])=(cos⁡2πt,sin⁡2πt), is a homeomorphism and sends [0] to 1∈S1 ([t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle).

[L4]

Finite sums and products of continuous real-valued maps are continuous, as are quotients on cozero sets (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[L5]

A based circle loop is nullhomotopic exactly when its degree is zero (A based circle loop is nullhomotopic exactly when its degree is zero).

Proof

technique · constructive
1.1givenF1L1L2construct

For τ∈[0,1] and u∈R/Z, put q(τ,u)=p(τRh(u))/p(τR). Root-freeness makes numerator and denominator nonzero, so A(τ,u):=h−1(q(τ,u)∣q(τ,u)∣) is defined; moreover q(τ,[0])=1, hence A(τ,[0])=[0]. Define αR(u)=A(1,u).

2.1step 1.1F1F2L1L2L3L4

Writing complex addition and multiplication in real and imaginary coordinates shows from [F1], [L3], and [L4] that (τ,u)↦p(τRh(u)) and τ↦p(τR) are continuous. Root-freeness and [L1] make division and radial normalization continuous, and [L2] makes A continuous. At τ=0 one has q(0,u)=p(0)/p(0)=1, so A(0,u)=[0] for every u, while step 1.1 keeps the basepoint fixed for all τ. Thus A is a based homotopy on the unit interval from the constant loop to αR, including the case R=0 without division by R.

3.1step 2.1L5discharge-construct∎

Hence αR is nullhomotopic for every R≥0, and [L5] gives deg⁡(αR)=0.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The normalized large-radius loop of a monic degree-n polynomial has degree n

Statement

Let p(z)=zn+∑j<najzj be a monic complex polynomial of degree n≥1, and put S=∑j<n∣aj∣. If R>max⁡{1,S}, then the based normalized circle loop

αR(u)=h−1(p(Rh(u))/p(R)∣p(Rh(u))/p(R)∣),u∈R/Z,

is well defined and has degree n.

Facts & Assumptions

Given: A monic polynomial p(z)=zn+∑j<najzj of degree n≥1, the number S=∑j<n∣aj∣, and a real R>max⁡{1,S}.

[F1]

For a nonzero complex polynomial, degree is the final coefficient index and monic means that its leading coefficient is 1 (Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials).

[L2]

The homeomorphism h:R/Z→S1 sends [0] to 1∈S1 ([t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle).

[L4]

Path-homotopic based circle loops have the same degree (Path-homotopic based circle loops have the same degree).

[L5]

The standard loop ωm has degree m for every integer m (deg⁡(ωn)=n for every integer n).

Proof

technique · constructive
1.1givenF1L1algebra

If ∣z∣=R, then ∣∑j<najzj∣≤∑j<n∣aj∣Rj≤SRn−1<Rn=∣zn∣. The estimate includes n=1 and S=0, since R>1 and S<R.

2.1step 1.1L1L2L3construct

For s∈[0,1] put ps(z)=zn+s∑j<najzj. Step 1.1 remains strict with sS≤S, so ps never vanishes on ∣z∣=R, in particular ps(R)≠0. The formula H(s,u)=h−1(ps(Rh(u))/ps(R)∣ps(Rh(u))/ps(R)∣) is therefore a continuous based homotopy by [L2] and [L3]. At s=1 it is αR, while at s=0 it is u↦h−1(h(u)n)=ωn(u).

3.1step 2.1L4L5discharge-construct∎

Homotopy invariance and the standard-loop calculation give deg⁡(αR)=deg⁡(ωn)=n.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Fundamental theorem of algebra by the fundamental-group obstruction

Statement

Every nonconstant complex polynomial has a complex root.

Facts & Assumptions

Given: A nonconstant complex polynomial p.

[F1]

A nonzero polynomial has a degree and a nonzero leading coefficient, and it is monic exactly when its leading coefficient is 1 (Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials).

[L1]

If a complex polynomial has no zero, then every normalized circle loop obtained from it is nullhomotopic (A root-free complex polynomial gives nullhomotopic normalized circle loops).

[L2]

For a monic complex polynomial of positive degree n, every radius satisfying the strict leading-term bound gives a normalized circle loop of degree n (The normalized large-radius loop of a monic degree-n polynomial has degree n).

[L3]

A based circle loop is nullhomotopic exactly when its degree is zero (A based circle loop is nullhomotopic exactly when its degree is zero).

Proof

technique · contradiction
1.1givenF1assume-contraalgebra

Suppose p has no root. Since p is nonconstant, it is nonzero and has degree n≥1 and leading coefficient c≠0. Dividing every coefficient by c gives a monic polynomial q=c−1p of the same degree and with the same zero set, so q is also root-free.

2.1step 1.1L1L3

By [L1], every normalized radius-R loop of q is nullhomotopic, and therefore has degree zero by [L3].

2.2step 1.1L2choose

Write q(z)=zn+∑j<najzj, put S=∑j<n∣aj∣, and take R=max⁡{1,S}+1. Then R>max⁡{1,S}, so [L2] says that the normalized radius-R loop has degree n.

3.1step 2.1step 2.2algebradischarge-contradiction∎

Steps 2.1 and 2.2 assign the same loop both degree 0 and degree n, impossible because n≥1. Hence the root-free assumption is false and p has a complex root.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The fundamental-group and minimum-modulus proofs of the fundamental theorem of algebra

The theorem Fundamental theorem of algebra by the fundamental-group obstruction and the published Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root establish the same root-existence statement by genuinely different routes. The fundamental-group proof compares a root-free radial nullhomotopy with the nonzero degree forced by the leading term on a large circle. The minimum-modulus proof instead chooses a point where ∣p∣ is least and shows that a positive minimum can be decreased. The first argument spends the calculation of π1(S1); the second spends compactness and the local expansion of a polynomial.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

An antipodal circle map has odd lift increment and is not nullhomotopic

Statement

On S1=R/Z, define the antipodal involution by a([u])=[u+1/2]. If a continuous map h:S1→S1 satisfies h∘a=a∘h, then every lift h~:[0,1]→R of t↦h([t]) has

h~(1)−h~(0)=2k+1

for some integer k. Thus the lift increment is odd, possibly negative, and the loop t↦h([t]) is not nullhomotopic.

Facts & Assumptions

Given: A continuous map h:S1→S1 with h∘a=a∘h.

[F1]

For the quotient map p:R→R/Z, one has p(x)=p(y) exactly when x−y∈Z, and p(x+m)=p(x) for every integer m (The circle as S1=R/Z with basepoint [0]).

[L1]

The quotient map p:R→R/Z is a covering map (p:R→R/Z is a covering map with translated interval sheets).

[L2]

A path in the base of a covering has a unique lift after its initial lift point is fixed (Existence and uniqueness of path lifts through a covering map).

[L3]

Endpoint-fixed homotopic paths have lifts with the same endpoint whenever their lifts begin at the same point (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).

Proof

technique · contradiction
1.1F1algebra

If [u]=[v], then (u+1/2)−(v+1/2)=u−v∈Z, so a([u])=[u+1/2] is well defined by [F1]; moreover a(a([u]))=[u+1]=[u], so a is an involution.

1.2assume-contra

Suppose the loop t↦h([t]) were endpoint-fixed homotopic to the constant loop at h([0]).

2.1step 1.1givenF1L1L2

Let y∈R be arbitrary subject to p(y)=h([0]). By [L1] and [L2], the loop t↦h([t]) has a unique lift h~ with h~(0)=y. Antipodality gives p(h~(1/2))=h([1/2])=p(y+1/2), so [F1] gives a unique integer k with h~(1/2)=y+k+1/2.

3.1step 2.1F1L2algebra

For 0≤t≤1/2, the paths t↦h~(t+1/2) and t↦h~(t)+k+1/2 project to the same path because h([t+1/2])=a(h([t])), and they agree at t=0 by step 2.1. Lift uniqueness gives h~(t+1/2)=h~(t)+k+1/2, so at t=1/2 one obtains h~(1)=y+2k+1.

4.1step 3.1step 1.2L3algebradischarge-contradiction∎

The constant loop at h([0]) has the constant lift beginning at y, so [L3] and step 1.2 would force h~(1)=y. Step 3.1 instead gives h~(1)=y+2k+1≠y for every integer k, including negative k. This contradiction shows that the loop is not nullhomotopic and completes the odd-increment claim.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Borsuk–Ulam theorem in dimension two

Statement

For every continuous map f:S2→R2, there is an x∈S2 with f(x)=f(−x).

Facts & Assumptions

Given: A continuous map f:S2→R2.

[F1]

The sphere S2 is the unit sphere in R3, and its equator is the image of e:R/Z→S2, e([t])=(cos⁡2πt,sin⁡2πt,0) (Euclidean spheres and closed balls as subspaces of Rn, [t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle).

[L1]

Every continuous antipodal map S1→S1 has an odd lift increment and is not nullhomotopic (An antipodal circle map has odd lift increment and is not nullhomotopic).

[L2]

The sphere S2 is simply connected (Sn is simply connected for every n≥2).

[L3]

Radial normalization ρ:R2∖{0}→S1, ρ(y)=y/∥y∥2, is continuous (Radial normalisation x↦x/∥x∥2 is continuous on Rn∖{0}).

[L4]

Postcomposition by a continuous map preserves a homotopy relative to its fixed subspace (Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form).

[L5]

Continuity of maps into Euclidean space is componentwise, and sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

Proof

technique · contradiction
1.1givenassume-contra

Suppose f(x)≠f(−x) for every x∈S2.

2.1step 1.1L3L5constructalgebra

The difference d(x)=f(x)−f(−x) is continuous by [L5] and nonzero by step 1.1, so g(x)=ρ(d(x)) defines a continuous map g:S2→S1. Since d(−x)=−d(x), one has g(−x)=−g(x).

3.1step 2.1F1L1L5

Let h:R/Z→S1 be the homeomorphism in [F1] and put b=h−1∘g∘e. The map e is continuous componentwise by [L5]; since e([t+1/2])=−e([t]) and h([u+1/2])=−h([u]), the continuous map b is antipodal. Hence the loop t↦b([t]) is not nullhomotopic by [L1].

3.2step 2.1F1L2L4

The loop t↦e([t]) in S2 is nullhomotopic because S2 is simply connected. Postcomposing such a nullhomotopy with the continuous map h−1∘g makes t↦b([t]) nullhomotopic in R/Z.

4.1step 1.1step 3.1step 3.2discharge-contradiction∎

Steps 3.1 and 3.2 contradict one another. Therefore the assumption in step 1.1 is false, and some x∈S2 satisfies f(x)=f(−x).

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

There is no continuous injection from S2 into R2

Statement

There is no continuous injective map S2→R2.

Facts & Assumptions

Given: A continuous map f:S2→R2.

[L1]

For every continuous map f:S2→R2, there is an x∈S2 with f(x)=f(−x) (Borsuk–Ulam theorem in dimension two).

[F1]

The unit sphere S2 consists of the vectors x∈R3 with ∥x∥2=1 (Euclidean spheres and closed balls as subspaces of Rn).

[F2]

A map is injective when equality of two images forces equality of their inputs (Injection, surjection, bijection).

Proof

technique · direct
1.1givenL1choose

By [L1], choose x∈S2 with f(x)=f(−x).

2.1step 1.1F1F2algebra∎

If x=−x, then 2x=0 and hence x=0, contrary to ∥x∥2=1. Thus x and −x are distinct points with the same image, so f is not injective.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

One member of every three-set closed cover of S2 contains an antipodal pair

Statement

If three closed subsets A1,A2,A3 cover S2, then one of them contains a pair of antipodal points: there are i∈{1,2,3} and x∈S2 with x,−x∈Ai.

Facts & Assumptions

Given: Closed subsets A1,A2,A3⊆S2 with S2=A1∪A2∪A3.

[L1]

For every continuous map f:S2→R2, there is an x∈S2 with f(x)=f(−x) (Borsuk–Ulam theorem in dimension two).

[L2]

If A is a nonempty subset of a metric space, then ∣d(x,A)−d(y,A)∣≤d(x,y), so x↦d(x,A) is continuous (∣d(x,A)−d(y,A)∣≤d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz).

[L3]

For every closed subset C of a metric space there is a continuous real-valued function with zero set C; for nonempty C one may use d(x,C), and for C=∅ one may use the constant function 1 (In a metric space every closed set is a zero set and a Gδ, and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal).

[F1]

The sphere S2 carries the Euclidean subspace metric (Euclidean spheres and closed balls as subspaces of Rn).

Proof

technique · direct
1.1givenF1L2L3

For i=1,2, define δi(x)=d(x,Ai) when Ai≠∅, and define δi(x)=1 when Ai=∅. By [L2] and [L3], each δi is continuous and its zero set is exactly Ai.

2.1step 1.1L1choose

Apply [L1] to δ=(δ1,δ2):S2→R2. There is x∈S2 such that δ1(x)=δ1(−x) and δ2(x)=δ2(−x).

3.1step 1.1step 2.1L3given∎

If either common value is zero, then x and −x both lie in the corresponding Ai. If both common values are positive, neither point lies in A1∪A2, so the covering hypothesis puts both in A3. In every case one cover member contains the antipodal pair.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

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]→G be loops based at e. Their pointwise product (α⋅β)(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×G→G, m(x,y)=xy, 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→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).

[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.1givenF1L1construct

The map K:[0,1]2→G, K(s,t)=α(s)β(t), is continuous, and K(0,0)=K(1,0)=K(0,1)=K(1,1)=e.

2.1step 1.1F2F3L1L2L3

For u,t∈[0,1], put Au(t)=min⁡{t1−u/2,1},Bu(t)=max⁡{t−u/21−u/2,0}. Since 1−u/2≥1/2, [L2] and [L3] make these functions continuous on the parameter square. Hence H1(t,u)=K(Au(t),Bu(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].

3.1step 1.1step 2.1F2F3

The formula H2(t,u)=K(Bu(t),Au(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 β∗α.

4.1step 2.1step 3.1F1L1discharge-construct∎

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The fundamental group of a topological group is abelian

Statement

If G is a topological group with identity e, then π1(G,e) is an abelian group.

Facts & Assumptions

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

[L1]

Pointwise multiplication of based loops in a topological group descends to loop classes and agrees there with loop concatenation; the pointwise product loop is homotopic to both concatenation orders (Pointwise multiplication and concatenation of loops in a topological group agree up to homotopy).

[L2]

Loop concatenation makes π1(G,e) a group whose identity is the class of the constant loop at e (Loop classes form the group π1(X,x0) under concatenation).

[F1]

A group is abelian when its operation is commutative (Group and abelian group).

Proof

technique · direct
1.1givenL1L2

The classes [α] and [β] have concatenation product [α∗β], while their pointwise product is represented by t↦α(t)β(t); [L1] identifies these two classes.

2.1step 1.1L1L2

The same pointwise product is also homotopic to β∗α by [L1]. Therefore [α][β]=[α∗β]=[β∗α]=[β][α].

3.1step 2.1F1∎

Since [α] and [β] were arbitrary, multiplication in π1(G,e) is commutative, so the fundamental group is abelian.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The punctured plane has fundamental group Z, while punctured Rn is simply connected for n≥3

Statement

For n≥2, put Pn=Rn∖{0} and let e0=(1,0,…,0).

  1. The punctured plane satisfies π1(P2,e0)≅Z.
  2. For every n≥3, the space Pn is path-connected and π1(Pn,x) is trivial for every x∈Pn; hence Pn is simply connected.

Facts & Assumptions

Given: A natural number n≥2, the punctured Euclidean space Pn, its unit sphere Sn−1, and the standard point e0∈Sn−1.

[L1]

For n≥1, radial normalization r(x)=x/∥x∥2 is a retraction Pn→Sn−1, and H(x,t)=((1−t)+t/∥x∥2)x is a deformation retraction of Pn onto Sn−1 (For n≥1, radial normalisation is a deformation retraction of Rn∖{0} onto Sn−1).

[L2]

If A is a deformation retract of X, the inclusion and retraction induce mutually inverse fundamental-group isomorphisms at every basepoint of A (A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism).

[L3]

The geometric unit circle based at e0=(1,0) has fundamental group isomorphic to Z (The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))≅Z).

[L4]

For every m≥2, the sphere Sm is simply connected (Sn is simply connected for every n≥2).

[L5]

Loop concatenation makes each fundamental group a group, with constant-loop identity and path reversal representing inverses (Loop classes form the group π1(X,x0) under concatenation).

Proof

technique · direct
1.1L1L2L3F1

For n=2, [L1] and [L2] identify π1(P2,e0) with π1(S1,e0), and [L3] identifies the latter with Z.

1.2givenL1L2L4

Let n≥3 and y∈Sn−1. Since n−1≥2, [L4] says that Sn−1 is simply connected, so π1(Sn−1,y) is trivial; [L1] and [L2] therefore make π1(Pn,y) trivial.

2.1step 1.2L1L5construct

For an arbitrary x∈Pn, the path γx(t)=((1−t)+t/∥x∥2)x runs in Pn from x to r(x). Concatenating an endpoint-fixed homotopy with the fixed paths γ‾x and γx preserves it, so Φx([α])=[γ‾x∗α∗γx] is well defined. The piecewise formula K(s,t)=γx(2s(1−t)) for s≤1/2 and K(s,t)=γx(2(1−s)(1−t)) for s≥1/2 contracts γx∗γ‾x to the constant path at x; applying the same formula to γ‾x contracts γ‾x∗γx at r(x). Hence the product of Φx([α]) and Φx([β]) cancels its middle γx∗γ‾x and equals Φx([α∗β]), while [δ]↦[γx∗δ∗γ‾x] is a two-sided inverse. Thus Φx:π1(Pn,x)→π1(Pn,r(x)) is an isomorphism, and step 1.2 makes π1(Pn,x) trivial.

3.1step 2.1L1L4construct∎

Given x,z∈Pn, follow γx to r(x), a sphere path from r(x) to r(z) supplied by the path-connectedness in [L4], and the reverse of γz. This gives a path from x to z, so Pn is path-connected. Together with step 2.1, this proves simple connectedness and completes both clauses.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

R2 is not homeomorphic to Rn for n≠2

Statement

For every natural number n≠2, there is no homeomorphism R2→Rn.

Facts & Assumptions

Given: A natural number n≠2.

[L1]

At the standard basepoint, the punctured plane has fundamental group isomorphic to Z; if the given n≥3, the punctured space Rn∖{0} is simply connected (The punctured plane has fundamental group Z, while punctured Rn is simply connected for n≥3).

[L2]

For every n≥2, there is no homeomorphism R→Rn (R is not homeomorphic to Rn for any n≥2).

[L3]

Pointed continuous maps induce homomorphisms on fundamental groups, functorially; in particular a pointed homeomorphism induces an isomorphism (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[L5]

A map into Rm is continuous exactly when its component functions are continuous; sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

Proof

technique · cases
1.1L4F1assume-case zero

If n=0, then R0 is a singleton by [L4], while 0 and e0 are distinct points of R2; hence no bijection, and therefore no homeomorphism, exists.

1.2L2F1assume-case one

If n=1, a homeomorphism R2→R would have an inverse homeomorphism R→R2, contrary to [L2].

1.3givenF1L4L5assume-case high

It remains to treat n≥3. Suppose h:R2→Rn is a homeomorphism. Translating the target gives a homeomorphism h0(x)=h(x)−h(0) with h0(0)=0; its value y=h0(e0) is nonzero because h0 is injective. Choose j<n with yj≠0.

2.1step 1.3L5algebraconstruct

Let P permute coordinate j into coordinate 0, put u=P(y), and define A:Rn→Rn by A(z)0=z0/u0 and A(z)k=zk−(uk/u0)z0 for 1≤k<n. Its inverse is A−1(w)0=u0w0 and A−1(w)k=wk+ukw0, so [L5] makes A a homeomorphism fixing 0 and carrying u to e0. Thus g=A∘P∘h0 is a homeomorphism with g(0)=0 and g(e0)=e0.

3.1step 2.1L1L3

Restriction gives a pointed homeomorphism (R2∖{0},e0)→(Rn∖{0},e0), so [L3] gives an isomorphism of their fundamental groups. This contradicts [L1], because the source is isomorphic to the nontrivial group Z and the target is trivial. Hence no homeomorphism exists when n≥3.

4.1step 1.1step 1.2step 3.1cases-exhaustive∎

Since n≠2, exactly one of n=0, n=1, or n≥3 holds, and steps 1.1, 1.2, and 3.1 exclude a homeomorphism in every case.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Hawaiian earring is compact and path-connected

Statement

For every integer n≥1, let Cn be the circle of radius 1/n centred at (1/n,0), and put

H=⋃n≥1Cn⊆R2.

The Hawaiian earring H is compact and path-connected.

Facts & Assumptions

Given: The circles Cn=S2((1/n,0),1/n) for integers n≥1, and their union H.

[F1]

A Euclidean sphere S2(c,r) is the set of points x with ∥x−c∥2=r (Euclidean spheres and closed balls as subspaces of Rn).

[F2]

A space is path-connected when every pair of its points can be joined by a continuous path in it (Paths, path-connected spaces and path components).

[L2]

The circle R/Z is path-connected, and its standard map to the geometric unit circle is a homeomorphism (R/Z is compact and path-connected, [t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle).

[L3]

A map into Rm is continuous exactly when its component functions are continuous; sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L4]

The Euclidean norm satisfies the reverse triangle inequality ∣∥u∥2−∥v∥2∣≤∥u−v∥2 and is continuous (The finite and reverse triangle inequalities for a norm; and for n≥1 every norm N on Rn satisfies N(x)≤C∥x∥1 and is Lipschitz, hence continuous, for d2).

[L5]

For every real ε>0 there is an integer N≥1 with 1/N<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

Proof

technique · direct
1.1givenF1constructalgebra

Each Cn contains the origin because its centre has norm 1/n, and its radius is positive because n≥1. Thus the displayed union is nonempty and no circle of radius 1/0 occurs.

2.1step 1.1F1algebra

If x∈Cn, then ∥x∥2≤∥x−(1/n,0)∥2+1/n=2/n≤2, so H is bounded.

2.2step 1.1F1L4L5algebra

Each Cn is closed: if x∉Cn, then η=∣∥x−(1/n,0)∥2−1/n∣/2>0, and [L4] shows that the ball of radius η about x misses Cn. Now let x∉H and write d=∥x∥2>0. By [L5], choose N≥1 with 2/N<d/2. Every Cn with n≥N lies in the ball of radius d/2 about 0, while the union of the circles with 1≤n<N is a finite, possibly empty, closed union that misses x. Intersecting a neighbourhood of x disjoint from that finite union with the ball of radius d/2 about x gives a neighbourhood disjoint from all of H. Hence H is closed.

3.1step 2.1step 2.2L1

Steps 2.1 and 2.2 make H closed and bounded in R2, so it is compact by [L1].

4.1step 1.1F2L2L3construct∎

The affine map z↦(1/n,0)+(1/n)z carries the unit circle homeomorphically onto Cn, so [L2] and [L3] make each Cn path-connected. Given x∈Cm and y∈Cn, join x to the common origin inside Cm and then the origin to y inside Cn; concatenating the paths gives a path in H. Thus H is path-connected.

5 · Examples, counterexamples and false statements

None yet.

Sources