Alphabeta Math
Session-authored (Fable 5 assisted)
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.

13 results · all verified · 10 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 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Seifert–van Kampen Theorem

1 · Prerequisites

2 · Summary

Based loops and induced homomorphisms turn continuous maps into group maps (Based loops and the fundamental group, The homomorphism on fundamental groups induced by a pointed continuous map). The arbitrary-map pushout of Pushouts of group homomorphisms combines homomorphisms with a common source without assuming injectivity. Compactness and the Lebesgue-number theorem (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover) supply finite subdivisions subordinate to open covers, while Deg:π1(R/Z,[0])(Z,+) is an isomorphism supplies the basic nontrivial calculation.

Loop subdivision gives Loops over a two-set path-connected open cover factor through the covering sets, and a subordinate homotopy grid makes its pushout value invariant in Homotopic-loop factorizations have the same value in the group pushout. These results yield Seifert–van Kampen identifies the fundamental group with a group pushout and its quotient and free-product consequences. Explicit wedge neighbourhoods lead to The fundamental group of a finite wedge of circles is free of that rank, while componentwise loops give π1(X×Y,(x0,y0))π1(X,x0)×π1(Y,y0). The same machinery proves simple connectedness of higher-dimensional spheres and computes the fundamental group of The two-dimensional torus T2=(R/Z)2.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Loops over a two-set path-connected open cover factor through the covering sets

Statement

Let X=UV, where U and V are open path-connected subsets of X, let UV be path-connected, and fix x0UV. If jU:UX and jV:VX are the inclusions, then every element of π1(X,x0) is a finite product of elements in the images of

(jU):π1(U,x0)π1(X,x0),(jV):π1(V,x0)π1(X,x0).

Equivalently, these two images generate π1(X,x0) (Based loops and the fundamental group, The homomorphism on fundamental groups induced by a pointed continuous map).

Facts & Assumptions

Given: The cover, basepoint, and inclusion maps in the Statement, and a based loop α:IX at x0.

[F1]

If an open cover of a compact metric space has Lebesgue number δ>0, every nonempty subset of diameter less than δ lies in one cover member (Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover).

[F2]

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

[F3]

Loop concatenation is well defined on path-homotopy classes and makes π1(X,x0) a group, with constant-loop identity and path-reversal inverses (Loop classes form the group π1(X,x0) under concatenation).

[F4]

A natural-number-indexed finite family of nonempty sets has a choice function, without any choice axiom (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[F7]

For every real η>0 there is a natural q1 with 1/q<η (For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε).

Proof

technique · direct
1.1

By [F5], α1(U) and α1(V) form an open cover of the compact metric interval I. Choose a Lebesgue number δ>0 by [F1], then choose q1 with 1/q<δ by [F7] and use the subdivision ti=i/q. Each restricted path αi:=α[ti1,ti], reparametrized to I, is continuous by [F8] and lies wholly in U or wholly in V; assign it to U if its image lies in U, and to V otherwise. Merge adjacent pieces assigned to the same set. After merging, every interior subdivision value α(ti) lies in UV; the construction also admits the constant loop and the case of one retained piece.

F1F5F6F7F8
2.1

Put λ0=λm=cx0. For each remaining interior vertex, [F2] makes the family of paths in UV from x0 to α(ti) nonempty, so [F4] supplies paths λi for the finitely many vertices. If αi lies in Ai{U,V}, then βi:=λi1αiλˉi is a based loop in Ai.

step 1.1F2F4choose
3.1

In the product [β1][βm], every adjacent pair λˉiλi cancels up to endpoint-fixed path homotopy, and the outside connectors are constant. Thus [F3] gives [α]=(jA1)[β1](jAm)[βm]. For m=1 this is the single factor [α], and for a constant loop it is the identity, so every loop class has the asserted factorization.

step 2.1F3algebra
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Antipodal complements cover Sn by simply connected sets with path-connected overlap for n2

Statement

Let n2 and write SnRn+1 for the unit sphere (Euclidean spheres and closed balls as subspaces of Rn). For any coordinate unit vector ej, put

Uj=Sn{ej},Vj=Sn{ej}.

Then Uj and Vj are open, simply connected subsets of Sn, they cover Sn, and their intersection is path-connected. More precisely, stereographic projection gives homeomorphisms UjRn, VjRn, and UjVjRn{0}.

Facts & Assumptions

Given: A natural n2, a coordinate index j<n+1, the unit vector ej, and the unit sphere SnRn+1.

[F1]

The unit sphere Sn is the set of zRn+1 with z2=1 (Euclidean spheres and closed balls as subspaces of Rn).

[F2]

Sums and products of continuous real 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).

[F3]

Continuity of maps into a finite-dimensional Euclidean space is equivalent to continuity of every coordinate map (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).

[F5]

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

[F6]

For n2, Rn{0} is polygonally connected, hence path-connected (For n2, the punctured space Rn{0} is polygonally connected).

[F7]

Pointed homeomorphisms induce mutually inverse fundamental-group homomorphisms (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F8]

A space is simply connected when it is nonempty and path-connected and its fundamental group has one element at every basepoint (Simply connected topological spaces).

Proof

technique · direct
1.1

Delete the j-th coordinate to identify ej with Rn, and write z=u+tej. Projection from ej is σ+(z)=u/(1t) on Uj, with inverse τ+(y)=2yy22+1+y221y22+1ej. Projection from ej is σ(z)=u/(1+t) on Vj, with inverse τ(y)=2yy22+1+1y22y22+1ej. Since y220, the inverse denominator y22+1 is positive. The sphere equation u22+t2=1 and deletion of the relevant pole give 1t0 on Uj and 1+t0 on Vj. The same equation shows that both inverse formulas land on Sn, and direct substitution gives σ±τ±=id and τ±σ±=id.

F1algebra
2.1

The coordinate t is continuous, so Uj={zSn:t<1} and Vj={zSn:t>1} are open by [F4]. They cover the sphere because no point has both t=1 and t=1. The formulas in step 1.1 are continuous by [F2] and [F3], so they are the asserted homeomorphisms. Moreover σ+ sends the deleted point ej to 0, hence restricts to a homeomorphism UjVjRn{0}.

step 1.1F2F3F4
3.1

The space Rn is nonempty and convex, so [F5] makes it simply connected. Each homeomorphism in step 2.1 transports paths, and [F7] applied to it and its inverse transports the one-element fundamental group at every basepoint. Thus [F8] makes both Uj and Vj simply connected.

step 2.1F5F7F8
4.1

By [F6] and the last homeomorphism in step 2.1, UjVj is path-connected. This proves every assertion.

step 2.1F6
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Sn is simply connected for every n2

Statement

For every natural number n2, the unit sphere SnRn+1 is simply connected (Simply connected topological spaces).

Facts & Assumptions

Given: A natural number n2 and an arbitrary basepoint x0Sn.

[L1]

For either of two distinct coordinate axes, the complements of its antipodal coordinate poles are open and simply connected, cover Sn, and have path-connected overlap (Antipodal complements cover Sn by simply connected sets with path-connected overlap for n2).

[L2]

For a two-set open cover whose two members and overlap are path-connected and contain the basepoint, the inclusion-images of the two fundamental groups generate the fundamental group of the union (Loops over a two-set path-connected open cover factor through the covering sets).

[F1]

A space is simply connected when it is nonempty and path-connected and has a one-element fundamental group at every basepoint (Simply connected topological spaces).

Proof

technique · direct
1.1

The point x0 cannot be a pole on both the first and second coordinate axes. Choose the first axis unless x0 is one of its two poles, and choose the second axis otherwise. For that axis, [L1] supplies an antipodal open cover Sn=UV with x0UV, with U and V simply connected and UV path-connected. Any two points of Sn can be joined by going inside their respective cover members to a point of the nonempty overlap and then inside the overlap, so Sn is path-connected.

L1
2.1

By [L2], every element of π1(Sn,x0) is a product of classes induced from π1(U,x0) and π1(V,x0). Both groups have one element by [L1], so every factor, and hence every such product, is the identity. Thus π1(Sn,x0) has one element.

step 1.1L1L2
3.1

The sphere is nonempty, step 1.1 makes it path-connected, and step 2.1 applies to the arbitrary basepoint x0. Therefore every basepoint has a one-element fundamental group, so [F1] makes Sn simply connected.

step 1.1step 2.1F1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

A path homotopy over a two-set open cover admits a finite subordinate grid

Statement

Let X=UV with U and V open, and let H:I×IX be a path homotopy. Suppose finite subdivisions of the bottom and top edges are prescribed. Then there are finite partitions

0=s0<s1<<sm=1,0=t0<t1<<tr=1

such that the horizontal partition contains every prescribed bottom and top cut, and every closed grid rectangle [si1,si]×[tk1,tk] is mapped by H wholly into U or wholly into V.

Facts & Assumptions

Proof

technique · constructive
1.1

By [F4], H1(U) and H1(V) form an open cover of the compact metric square I2. By [F1] and [F2], choose a Lebesgue number δ>0 for this cover in d.

F1F2F3F4
2.1

Take q1 with 1/q<δ, using [F5]. Start with the uniform cuts k/q in each coordinate, adjoin the finitely many prescribed bottom and top cuts to the horizontal list, and sort each resulting finite set after removing repetitions. Every gap in either partition is at most 1/q<δ, and both lists contain 0 and 1.

step 1.1F5construct
3.1

Each closed grid rectangle is nonempty and has d-diameter at most 1/q<δ, so [F2] places it inside H1(U) or H1(V). Its image therefore lies in the corresponding cover member, and the constructed horizontal partition refines both prescribed boundary subdivisions.

step 1.1step 2.1F2discharge-construct
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Homotopic-loop factorizations have the same value in the group pushout

Statement

Assume the hypotheses of Loops over a two-set path-connected open cover factor through the covering sets, and let P be a pushout of

π1(UV,x0)π1(U,x0),π1(UV,x0)π1(V,x0).

A subordinate factorization is one obtained from a finite subdivision and connector paths in UV as in Loops over a two-set path-connected open cover factor through the covering sets; it writes the loop class as a product of inclusion-images of based loops lying in U or V. Replace each factor by its image under the corresponding canonical map to P and multiply in the same order. If two based loops are path-homotopic relative to their endpoints, then every subordinate factorization of the first and every subordinate factorization of the second have the same value in P.

Facts & Assumptions

Given: The two-set cover and basepoint, the pushout P with factor maps iU,iV, endpoint-homotopic based loops α,β, and subordinate factorizations of both loops.

[L1]

Every based loop over the cover has a finite subordinate factorization by loops in U and V (Loops over a two-set path-connected open cover factor through the covering sets).

[L2]

A path homotopy over the cover has a finite subordinate grid refining any prescribed bottom and top subdivisions (A path homotopy over a two-set open cover admits a finite subordinate grid).

[F1]

In the pushout, the factor maps satisfy iUkU=iVkV on π1(UV,x0) (Pushouts of group homomorphisms).

[F2]

A finite natural-number-indexed family of nonempty sets has a choice function (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[F3]

Loop concatenation, constant loops, and reversed paths give the group operation, identity, and inverses in every fundamental group (Loop classes form the group π1(X,x0) under concatenation).

Proof

technique · direct
1.1

The value of a subordinate factorization [α]=(jA1)[a1](jAm)[am] is, by definition, iA1[a1]iAm[am]P. Subdividing a factor only replaces one factor by a product in the same fundamental group. If a connector at a subdivision point is changed, the two connectors differ by a loop in UV, and [F1] gives the same element whether that correction is read in the U factor or the V factor. Thus refinements and connector changes preserve the value.

L1F1F3
2.1

Choose an endpoint-fixed path homotopy H from α to β. By [L2], take a subordinate rectangular grid refining the prescribed subdivisions of both factorizations. At every grid vertex, choose a path to x0 inside U if all adjacent rectangles are assigned to U, inside V if all are assigned to V, and inside UV if both assignments occur. Each required path family is nonempty by path-connectedness, and [F2] licenses the finite selection; on the bottom and top edges use the prescribed connectors after the harmless adjustments of step 1.1.

step 1.1L2F2choose
3.1

For an oriented grid edge, concatenate its chosen endpoint connectors with the image of the edge. This gives a based loop in either adjacent cover member; if the adjacent assignments differ, both connectors lie in UV, so [F1] identifies the two readings in P. Around one grid rectangle, the four edge loops multiply to the identity because the restriction of H to that rectangle contracts its boundary inside its assigned cover member. Multiplying these boundary identities row by row cancels every interior edge with its reverse, leaving exactly the refined bottom word and the inverse of the refined top word. Hence the two words have equal value in P.

step 2.1F1F3algebra
4.1

Step 1.1 identifies the refined boundary words with the values of the original factorizations, while step 3.1 identifies those refined values with each other. Therefore every factorization of α and every factorization of β have the same value in P.

step 1.1step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Seifert–van Kampen identifies the fundamental group with a group pushout

Statement

Let X=UV, where U and V are open path-connected subsets of X, let UV be path-connected, and fix x0UV. For the inclusion-induced maps in the diagram

π1(U,x0)π1(UV,x0)π1(V,x0),

the group π1(X,x0), together with the two inclusion-induced homomorphisms, is a pushout (Pushouts of group homomorphisms). Equivalently, the canonical homomorphism from any pushout P of the displayed diagram to π1(X,x0) is an isomorphism. No injectivity of either map from the overlap group is assumed.

Facts & Assumptions

Given: The cover and basepoint in the Statement, a pushout P with factor maps iU,iV, and the inclusion-induced maps to π1(X,x0).

[L1]

Every loop class in π1(X,x0) has a finite factorization by inclusion-images of loop classes from U and V (Loops over a two-set path-connected open cover factor through the covering sets).

[L2]

All subordinate factorizations of homotopic based loops have one common value in P (Homotopic-loop factorizations have the same value in the group pushout).

[L3]

For arbitrary group homomorphisms KG and KH, the quotient of GH by the normal closure of the amalgamating relations is a pushout, so a pushout of the displayed diagram exists (A group pushout is the quotient of a free product by the amalgamating relations).

[F1]

Every compatible pair of homomorphisms out of the two factors of a group pushout factors through a unique homomorphism from the pushout (Pushouts of group homomorphisms).

[F2]

Pointed inclusions induce group homomorphisms on fundamental groups (The homomorphism on fundamental groups induced by a pointed continuous map).

Proof

technique · direct
1.1

Choose the pushout P supplied by [L3]. The two inclusion-induced homomorphisms from π1(U,x0) and π1(V,x0) to π1(X,x0) agree on π1(UV,x0), since both composites are induced by the same inclusion. By [F1], they therefore define a unique homomorphism Φ:Pπ1(X,x0) satisfying ΦiU=(jU) and ΦiV=(jV).

L3F1F2choose
1.2

For cπ1(X,x0), let Ψ(c) be the element of P that is the value of some subordinate factorization of some loop representing c. Such a factorization exists by [L1], and [L2] says that all representatives and all their factorizations give the same value. Thus exactly one such element exists for each c, so this rule defines a function without selecting factorizations globally. Concatenating two factorizations concatenates their words, hence Ψ is a homomorphism.

L1L2construct
2.1

If c is represented by a factorized loop, applying Φ to its pushout word restores the same product of inclusion-images, which is c by [L1]. Hence ΦΨ=idπ1(X,x0).

step 1.1step 1.2L1
2.2

For aπ1(U,x0), the one-factor factorization of its image gives Ψ((jU)a)=iU(a), and similarly on the V factor. Thus ΨΦ:PP agrees with the identity after composition with both factor maps. Uniqueness in [F1] makes ΨΦ=idP.

step 1.1step 1.2F1
3.1

The homomorphisms Φ and Ψ are inverse, so Φ is an isomorphism and π1(X,x0) has the asserted pushout property.

step 2.1step 2.2
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

A simply connected overlap turns the van Kampen pushout into a free product

Statement

Under the hypotheses of Seifert–van Kampen identifies the fundamental group with a group pushout, if UV is simply connected, then the inclusion-induced homomorphisms give an isomorphism

π1(U,x0)π1(V,x0)π1(X,x0).

Facts & Assumptions

Given: A two-set van Kampen cover X=UV with simply connected overlap.

[L1]

The fundamental group of X is the group pushout of the two inclusion-induced maps from π1(UV,x0) (Seifert–van Kampen identifies the fundamental group with a group pushout).

[F1]

The free product with amalgamation over the trivial group is canonically isomorphic to the ordinary free product (Amalgamation over the trivial group is the ordinary free product).

[F2]

A simply connected space has a one-element fundamental group at every basepoint (Simply connected topological spaces).

Proof

technique · direct
1.1

By [F2], π1(UV,x0) is the trivial group, so the two maps in the pushout of [L1] are the unique homomorphisms from the trivial group.

L1F2
2.1

The two maps from the trivial group are injective, so [F1] identifies their pushout with π1(U,x0)π1(V,x0). Combining this with [L1] gives the displayed isomorphism.

step 1.1L1F1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

If one set in a van Kampen cover is simply connected, the other fundamental group surjects with overlap-generated kernel

Statement

Assume the hypotheses of Seifert–van Kampen identifies the fundamental group with a group pushout and suppose that V is simply connected. Let

k:π1(UV,x0)π1(U,x0)

be induced by inclusion. Then (jU):π1(U,x0)π1(X,x0) is surjective and

ker(jU)= ⁣imk ⁣π1(U,x0).

Facts & Assumptions

Given: The van Kampen cover in the Statement, with V simply connected.

[L1]

The fundamental group of X is the pushout of the two inclusion-induced maps from the overlap group (Seifert–van Kampen identifies the fundamental group with a group pushout).

[F1]

For arbitrary homomorphisms f:KG and h:KH, the quotient of GH by the normal closure of jG(f(k))jH(h(k))1 is their pushout (A group pushout is the quotient of a free product by the amalgamating relations).

[F2]

The normal closure of a subset is the smallest normal subgroup containing it (The normal closure of a subset of a group).

[F3]

A free product is characterized by the universal property for homomorphisms from its factors (The free product of an arbitrary family of groups).

[F4]

A simply connected space has a one-element fundamental group at every basepoint (Simply connected topological spaces).

Proof

technique · direct
1.1

By [F4], π1(V,x0) is trivial. Thus [L1] identifies π1(X,x0) with the pushout of k and the unique homomorphism from π1(UV,x0) to the trivial group.

L1F4
2.1

By [F3], the free product of π1(U,x0) with the trivial group is canonically π1(U,x0). Under this identification, [F1] says that the pushout in step 1.1 is π1(U,x0)/ ⁣imk ⁣.

step 1.1F1F2F3
3.1

The canonical map from π1(U,x0) to this quotient is exactly (jU) under [L1]. A quotient map is surjective and has the quotienting normal subgroup as its kernel, so the asserted surjectivity and kernel formula follow.

step 2.1L1
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The wedge of a family of pointed spaces

Definition

Let ((Xi,xi))iI be a family of pointed topological spaces. On the tagged disjoint union iIXi (The disjoint union (coproduct) iXi with the final topology of the canonical injections: a set is open exactly when each of its traces is), define

(x,i)(y,j)(x,i)=(y,j)  or  (x=xi  and  y=xj).

This relation is reflexive and symmetric. For transitivity, the only nontrivial case has two related pairs that are not equal; then every point appearing is its summand's basepoint, so the first and third points are related as well. Thus is an equivalence relation.

For nonempty I, the wedge is the quotient space

iI(Xi,xi):=(iIXi) ⁣/

with the quotient topology (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection). The common equivalence class of the tagged basepoints is the wedge point, which makes the quotient pointed. The relation identifies no other points.

The wedge of the empty family is defined to be a one-point space, pointed at its sole element. For a pair one writes (X,x0)(Y,y0), and for rN one writes j<r(Xj,xj). In particular, the empty finite wedge is a point rather than an empty space.

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

Finite wedges of quotient circles have van Kampen covers at the wedge point

Statement

Let Q=R/Z be pointed at [0], and put Wr=j<r(Q,[0]), with W0 the one-point space. Identify Wr+1 with WrQ through the canonical homeomorphism of their tagged quotient presentations. For every rN, this successor wedge has open subsets Ar,Br such that

Wr+1=ArBr,

Ar deformation retracts onto Wr, Br deformation retracts onto the new circle, and ArBr deformation retracts onto the wedge point. The two factor inclusions induce fundamental-group isomorphisms. The sets Ar, Br, and ArBr are path-connected, and the overlap is simply connected. Thus they satisfy the hypotheses of A simply connected overlap turns the van Kampen pushout into a free product.

Facts & Assumptions

Given: A natural r, the quotient-circle wedge Wr+1, its wedge point w, and the open quotient arc O=p((1/4,1/4)) about [0] in each circle summand.

[F1]

The quotient map p:RR/Z is open, and its restriction to every interval of length below one is a homeomorphism onto its image (The quotient map is open, and every interval shorter than one embeds in R/Z).

[F3]

A deformation retraction is a retraction together with a homotopy from the identity to the inclusion-composite that fixes the retract pointwise (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

[F4]

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

[F5]

Pointed homotopy equivalences induce inverse fundamental-group homomorphisms (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F6]

A space is simply connected when it is nonempty and path-connected and has a one-element fundamental group at every basepoint (Simply connected topological spaces).

[F7]

Reversal gives inverses and concatenation gives multiplication in fundamental groups (Loop classes form the group π1(X,x0) under concatenation).

Proof

technique · constructive
1.1

The tagged quotient for WrQ differs from that for Wr+1 only by grouping the old tagged summands; the quotient maps in both directions preserve every tag and are continuous by [F2], so they are inverse homeomorphisms. Under this identification, define Ar to contain all of the old wedge Wr and the arc O in the new circle. Define Br to contain the whole new circle and the arc O in every old circle. Their inverse images under the wedge quotient are open, by [F1] and the disjoint-union topology, and each inverse image is saturated because every listed arc contains its basepoint. Hence Ar and Br are open; they cover Wr+1, and their intersection consists exactly of one copy of O in every circle, with all their basepoints identified.

F1F2construct
2.1

Use the coordinate t(1/4,1/4) supplied by [F1] and the contraction t(1s)t. On Ar, contract only the new-circle arc and fix Wr; on Br, contract every old-circle arc and fix the new circle. The formulas agree at the tagged basepoints and are jointly continuous away from the wedge point. At the wedge point, a target neighbourhood contains an arc t<εj in every incident branch; there are finitely many branches, so their minimum is positive, and the contraction never increases t. Together with the fixed trace on the retract, this gives a product neighbourhood mapped into the target neighbourhood, proving joint continuity there. Thus the formulas are deformation retractions as in [F3], and [F5] makes the two retract inclusions induce fundamental-group isomorphisms.

step 1.1F1F3F5
3.1

Apply the same contraction simultaneously on every arc of ArBr. Joint continuity away from w is coordinatewise, and at w the same finite-minimum neighbourhood argument from step 2.1 applies to all incident arcs. This gives a deformation retraction of the overlap onto w. The construction also covers r=0, when W0 is the point w, and r=1, when the old wedge has one circle.

step 1.1step 2.1F1F3
4.1

Each point of any of the three sets can be joined within its circle arc or circle to w, so [F4] makes all three path-connected. At the basepoint w, step 3.1 and [F5] identify the overlap fundamental group with that of a point, hence with the one-element group. For any other basepoint y, a path ρ from w to y gives an isomorphism from the group at w to the group at y by [α][ρˉαρ], with reverse-path inverse, using [F7]; hence its fundamental group is one-element as well. The overlap is nonempty, so [F6] makes it simply connected.

step 2.1step 3.1F4F5F6F7discharge-construct
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The fundamental group of a finite wedge of circles is free of that rank

Statement

Let Q=R/Z be pointed at [0], and for rN put

Wr:=j<r(Q,[0]).

Then π1(Wr,w) is the free group on the r standard loops, one traversing each circle summand once. In particular it has rank r (The rank of a free group admitting a finite basis). For r=0, W0 is a point and the basis is empty.

Facts & Assumptions

Given: The finite quotient-circle wedges Wr and their standard based loops.

[L1]

The successor wedge Wr+1=WrQ has a two-set van Kampen cover whose members deformation retract to Wr and Q and whose overlap is simply connected (Finite wedges of quotient circles have van Kampen covers at the wedge point).

[L2]

A two-set van Kampen cover with simply connected overlap has fundamental group the free product of the two factor fundamental groups (A simply connected overlap turns the van Kampen pushout into a free product).

[F1]

The degree map is an isomorphism π1(Q,[0])(Z,+) and sends the standard once-around loop to 1 (Deg:π1(R/Z,[0])(Z,+) is an isomorphism).

[F2]

The free product of free groups on disjoint bases is the free group on the disjoint union of those bases (Free groups on disjoint bases freely multiply to the free group on their union).

[F3]

If a property holds at 0 and passes from every natural r to r+1, then it holds for every natural number (The principle of mathematical induction).

Proof

technique · induction
1.1

The empty wedge W0 is a point by definition. Every based loop in a point is constant, so π1(W0,w) is the one-element group, which is the free group on the empty basis and has rank 0.

base
1.2

The group of one circle is infinite cyclic by [F1], so its standard loop is a one-element free basis. This is the first successor case and fixes the basis convention used below.

F1
1.3

Assume π1(Wr,w) is free on the r standard circle loops. By [L1] and [L2], the successor wedge satisfies π1(Wr+1,w)π1(Wr,w)π1(Q,[0]).

L1L2ih
2.1

The induction hypothesis and [F1] identify the two factors as free groups on disjoint bases consisting of the old r standard loops and the new standard loop. By [F2], their free product is free on the union, exactly the r+1 standard loops of Wr+1.

step 1.3F1F2
3.1

Step 1.1 is the base case and steps 1.3 and 2.1 prove the successor implication, so [F3] gives the result for every rN. The basis has r elements, hence the rank is r by definition.

step 1.1step 1.3step 2.1F3discharge-induction
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

π1(S1S1) is the free group on two generators

Statement

For the wedge of two quotient circles, the fundamental group at the wedge point is the free group F(a,b) on the two standard once-around loop classes a and b.

Facts & Assumptions

Given: The wedge W2=(R/Z)(R/Z) and its two standard loop classes a,b.

[L1]

The fundamental group of a wedge of r quotient circles is free on its r standard circle loops (The fundamental group of a finite wedge of circles is free of that rank).

Proof

technique · direct
1.1

Apply [L1] with r=2 to obtain that π1(W2,w) is free on its standard circle loops.

L1algebra
2.1

Those standard loops are precisely a and b, so π1(W2,w)F(a,b).

step 1.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

π1(X×Y,(x0,y0))π1(X,x0)×π1(Y,y0)

Statement

For pointed topological spaces (X,x0) and (Y,y0), the coordinate projections induce a natural group isomorphism

Θ:π1(X×Y,(x0,y0))π1(X,x0)×π1(Y,y0),[γ]([πXγ],[πYγ]).

Its inverse sends ([α],[β]) to the class of the paired loop s(α(s),β(s)).

Facts & Assumptions

Given: Pointed spaces (X,x0) and (Y,y0), their product, and the two coordinate projections.

[F2]

Loop concatenation is well defined on path-homotopy classes and gives the fundamental-group operation (Loop classes form the group π1(X,x0) under concatenation).

[F3]

Componentwise multiplication makes the external direct product of two groups a group (G×H is a group with identity (eG,eH), coordinatewise inverses, and homomorphic coordinate projections).

[F4]

A path homotopy relative to endpoints is a homotopy whose two endpoint tracks are constant (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[F5]

A pointed continuous map sends [α] to [fα] by a well-defined group homomorphism, and induced maps respect identities and composition (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

Proof

technique · direct
1.1

Projection sends a loop in X×Y to one loop in each factor. If two product loops are path-homotopic relative to endpoints, composing the homotopy with either projection gives a path homotopy of the coordinate loops by [F4]. Thus the displayed rule Θ is well defined.

F1F4
1.2

Conversely, [F1] makes s(α(s),β(s)) a continuous based loop. Pairing two endpoint-fixed homotopies gives a product homotopy by the same characteristic property, so the resulting class depends only on [α] and [β]. This defines a function Ξ from the direct product to π1(X×Y,(x0,y0)).

F1F4construct
2.1

Projections commute with concatenation, so [F2] and [F3] show that Θ is a group homomorphism.

step 1.1F2F3
3.1

Coordinatewise concatenation shows that Ξ is a homomorphism. By construction ΘΞ([α],[β])=([α],[β]), and uniqueness of a map with given coordinates in [F1] gives ΞΘ[γ]=[γ]. Hence Θ and Ξ are inverse group isomorphisms.

step 1.1step 2.1step 1.2F1F2F3
4.1

Let f:(X,x0)(X,x0) and g:(Y,y0)(Y,y0) be pointed continuous maps. By [F1], their product f×g is pointed and continuous. Composition with any pointed continuous map preserves endpoint-fixed homotopies and commutes with loop concatenation, so [F2], [F4], and [F5] make all three induced maps in the naturality square well-defined homomorphisms. For every product-loop class [γ], both (f×g)ΘX,Y[γ] and ΘX,Y(f×g)[γ] equal ([fπXγ],[gπYγ]). Thus the naturality square commutes for every pair (f,g), so the displayed group isomorphism is natural.

step 1.1F1F2F4F5
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The two-dimensional torus T2=(R/Z)2

Definition

Let Q=R/Z be the quotient circle of The circle as S1=R/Z with basepoint [0]. The two-dimensional torus is the product space

T2:=Q×Q

with the product topology (The product set iIXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space), pointed at ([0],[0]). This definition uses the quotient-circle model in both coordinates.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

π1(T2)Z×Z

Statement

For T2=(R/Z)2 pointed at ([0],[0]),

π1(T2,([0],[0]))(Z,+)×(Z,+).

Facts & Assumptions

Given: The pointed torus T2 of The two-dimensional torus T2=(R/Z)2.

[L1]

The fundamental group of a product is naturally the direct product of the two fundamental groups (π1(X×Y,(x0,y0))π1(X,x0)×π1(Y,y0)).

[F1]

The degree map is an isomorphism π1(R/Z,[0])(Z,+) (Deg:π1(R/Z,[0])(Z,+) is an isomorphism).

Proof

technique · direct
1.1

By the torus definition and [L1], π1(T2,([0],[0]))π1(R/Z,[0])×π1(R/Z,[0]).

L1
2.1

Applying [F1] in both coordinates gives the displayed isomorphism with Z×Z.

step 1.1F1

5 · Examples, counterexamples and false statements

None yet.

Sources