Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

Möbius line Thom space as a projective-plane quotient

Example

For the Möbius line L→S1, Th⁡(L)=D(L)/S(L) is homeomorphic to RP2 with the center of a complementary disk as basepoint. Equivalently it is the quotient RP2/D2 for a closed disk whose complement is the interior of a Möbius band. This describes its twisting, beyond the AT mod-two Thom class example.

Facts & Assumptions

Given: D(L)=[0,1]×[−1,1]/((0,t)∼(1,−t)).

[F2]

Trivial Thom spaces as suspension smash products identifies the trivial line's Thom space over S1 with Σ(S+1).

Verification

1.1F1givenconstruct

The disk bundle D(L)=[0,1]×[−1,1]/((0,t)∼(1,−t)) is a Möbius band and its sphere bundle S(L) is its single boundary circle. Realize RP2 as the disk with antipodal boundary points identified. Removing from it a smaller concentric open disk leaves the closed annulus with its outer circle antipodally identified, which is again a Möbius band: the outer identification reverses the inward transverse direction on one traversal, which is the defining twist. Since the removed disk is complementary to that Möbius band, RP2 is obtained from D(L) by attaching a closed disk along ∂D(L), and collapsing that attached disk turns the pushout into D(L)/∂D(L), which is Th⁡(L) by [F1].

2.1F2step 1.1construct∎

On a disk pair D1⊂D2 of concentric Euclidean disks, the radial map that sends D1 to the center of D2 and rescales the annulus D2∖D1 onto D2 minus its center, while fixing the complement of D2, is continuous, injective off D1, and onto; it therefore descends to a continuous bijection D2/D1→D2 from the compact quotient to the Hausdorff disk, hence a homeomorphism. Applying this inside the projective plane to a disk containing the attached disk exhibits Th⁡(L)≅RP2/D2≅RP2 with the basepoint corresponding to the centre of the complementary disk. The trivial line over S1 instead has Thom space Σ(S+1) by [F2]: its two boundary circles are collapsed to the same basepoint, whereas the unreduced suspension ΣS1≅S2 keeps its two suspension points distinct.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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