Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Twisted duality for a nonorientable surface

Statement

Let Ng be the closed connected nonorientable surface of genus g≥1 and let O be its integral orientation system. Then H2(Ng;O)≅Z, and cap with its canonical twisted fundamental class gives Hk(Ng;Z)≅H2−k(Ng;O),Hk(Ng;O)≅H2−k(Ng;Z) for every integer k.

Facts & Assumptions

Given: The polygon CW structure on Ng with one vertex, one two-cell, and one-cells a1,…,ag, attached by a12⋯ag2.

[F1]

The orientation system is a local system gives monodromy ai↦−1 for every crosscap loop.

[F2]

Cellular chains compute local homology computes the twisted complex from its group-ring incidence matrix.

[F3]

Poincare duality with the orientation local system gives twisted duality on the closed surface.

Proof

technique · direct
1.1F1F2

The lifted boundary of the two-cell has ai-coefficient a12⋯ai−12(1+ai), obtained by differentiating the attaching word one letter at a time, or equivalently by grouping its two successive lifted incidences along ai. Under the orientation action in [F1], each preceding square acts as 1 and 1+ai acts as 1−1=0. Thus the twisted d2:Z→Zg is zero.

2.1F2step 1.1

Each lifted one-cell has endpoint incidence ai−1, which evaluates to −2. Hence d1:Zg→Z is (x1,…,xg)↦−2∑ixi. In particular H2(Ng;O)=ker⁡d2=Z; also H1(Ng;O)≅Zg−1 and H0(Ng;O)≅Z/2. These include g=1, where the middle group is zero.

3.1F3step 2.1∎

There is a canonical pairing O⊗O→Z‾: after choosing either generator ox, send ox⊗ox to 1 and extend bilinearly. Replacing ox by −ox changes both factors, so the map is independent of the choice; the two monodromy signs cancel, so it commutes with transport. Apply [F3] first with the constant system and then with L=O. The first target is O, and the second is O⊗O≅Z‾, giving the two displayed families. Step 2.1 verifies the top group directly. Degrees outside 0,1,2 vanish, and no AC beyond that already assumed by [F3] is introduced.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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