Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

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

Depends on

Used by

Dependency tree · two levels

37 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