Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Real projective space cover as a discrete fiber fibration

Example

For n≥1, define RPn=Sn/(x∼−x) with its quotient topology. The antipodal quotient q:Sn→RPn is a two-sheeted Hurewicz fibration. For n≥2, π1(RPn)≅Z/2,q∗:πk(Sn)≅πk(RPn)(k≥2). For n=1, the quotient identifies with a circle and q∗ on fundamental groups is multiplication by 2, not a quotient onto Z/2. These conclusions are choice-free.

Facts & Assumptions

[F1]

Coverings have unique HLP for all parameter spaces by finite local strips. Covering homotopies lift by finite local strips

[F2]

The fibration LES has an action on fiber components, with orbit and stabilizer descriptions. Long exact sequence of homotopy groups of a fibration

[F3]

Sn is path connected for n≥1, and π1(Sn)=0 for n≥2. Lower-dimensional sphere maps are based nullhomotopic

[F7]

The geometric circle has fundamental group Z, with the loop t↦e2πimt representing m. The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))≅Z

Verification

Given: n≥1, the antipodal quotient q, and the based fiber {x0,−x0}.

1.1F1F4

The quotient is open: for any open O⊆Sn, its saturation is q−1q(O)=O∪(−O), open. For x∈Sn let Ux={y:⟨y,x⟩>1/2}. Then Ux and −Ux are disjoint open sets, and q−1q(Ux)=Ux⊔(−Ux). Each restriction is bijective onto the open q(Ux) and is open by the same saturation argument for open subsets of Ux, hence is a homeomorphism. Such sets cover the quotient. Thus q is a two-sheeted covering and is Hurewicz by F1.

1.2F2

Its fiber is discrete with two points. Every based map of a positive-dimensional cube into this fiber is constant, since each line segment in the cube has connected image and a discrete set has no nonconstant path. All positive fiber homotopy groups vanish. F2 then gives q∗:πk(Sn)≅πk(RPn) for k≥2, because both adjacent fiber groups are zero, including π1 of the fiber at k=2.

1.3F4F5F6F7

For n=1, regard S1 as complex unit numbers. The map z↦z2 is constant on antipodal pairs and has precisely these fibers: w2=z2 implies (w−z)(w+z)=0. It is onto, since eiθ has square root eiθ/2. F4 gives a continuous bijection v:RP1→S1. The source is compact as the quotient image of the compact circle by F5–F6, and the target is Hausdorff, so F5 makes v a homeomorphism. The composite vq sends the generator loop e2πit to e4πit, so F7 gives multiplication by two on Z.

2.1F2F3step 1.1

For n≥2, F3 makes the total space path connected and simply connected. The F2 action of π1(RPn) on the two fiber components is transitive because both are in one total-space component, and its stabilizer is the image of π1(Sn)=0. Its orbit map is therefore a bijection with a two-element set, so the group has exactly two elements. Its nonidentity element squares to identity: its square cannot equal itself by cancellation, leaving only identity. This identifies the group with Z/2. A path from x0 to −x0 projects to a loop realizing the nontrivial action; its existence follows already from F3.

3.1step 1.1step 1.2step 2.1step 1.3∎

The spaces and two-point fiber are nonempty. Step 1.3 is the exceptional endpoint n=1; it is not covered by the simple-connectivity input in step 2.1. The higher-group computation in step 1.2 remains valid also for n=1. There is no claim here for n=0, whose total space is disconnected. Every chart was explicitly specified by its centre and all component assignments are unique; no AC or numerable-bundle theorem was used.

Depends on

Used by

Dependency tree · two levels

71 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