Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Euler class of zero and trivial positive-rank bundles

Example

Assume AC. For every base B in the general Thom scope and every commutative ring R:

  1. the zero bundle of rank zero with its standard unit orientation has e(0B,1)=1∈H0(B;R);
  2. every trivial bundle εBn of positive rank n≥1, with its standard product R-orientation, has e(εBn)=0∈Hn(B;R).

Facts & Assumptions

Given: AC, a base B in the general Thom scope, a commutative ring R and an integer n≥1.

[F1]

The Euler class is e(ξ)=s∗j∗(uξ); in rank zero the maps j and s are identities and e(0B,o)=o for the supplied orientation o, so the standard unit orientation gives e(0B,1)=1 (Euler class by zero-section pullback of the Thom class).

[F2]

Under AC, an R-oriented numerable real bundle of positive rank over a base in the general Thom scope has zero Euler class if it admits a nowhere-zero section; no converse is asserted (A nowhere-zero section forces the Euler class to vanish).

[F3]

Give εBn=B×Rn its product Euclidean metric. The global product chart identifies every fiber disk pair with (Dn,Sn−1) and every stalk of its R-orientation local system with Hn(Dn,Sn−1;R)≅R. The constant fiber class corresponding to 1R generates every stalk and is compatible in the single global chart, so it is an R-orientation by R-oriented vector bundle and orientation local system. For R=Z it is the coefficient orientation induced by the standard ordinary orientation of Rn in Oriented real bundles and oriented frame bundles. The formula b↦(b,e1) is a continuous section by the product topology and is nowhere zero because e1≠0.

[A1]

AC is the Axiom of Choice in the form fixed by The Axiom of Choice.

Verification

1.1F1

The rank-zero value. Give 0B the standard unit orientation. Its disk bundle is B, its sphere bundle is empty, and the zero section and relative-to-absolute map are identities; fiber normalization makes the Thom class the unit 1 in degree zero. Hence e(0B,1)=s∗j∗(1)=1∈H0(B;R) by [F1]. For another supplied rank-zero orientation o, the same calculation instead gives e(0B,o)=o.

1.2F2F3

The trivial bundle of positive rank. For n≥1 the constant section b↦(b,e1) of εBn is nowhere zero and continuous. Its global product chart, together with the constant partition of unity 1, makes the bundle numerable, while [F3] supplies its standard product R-orientation. The standing hypothesis places B in the general Thom scope. Thus every hypothesis of [F2] holds, and e(εBn)=0∈Hn(B;R).

2.1F1F2F3A1step 1.1step 1.2∎

Boundary cases. For the empty base the unique cohomology class in every degree is zero, and the standard rank-zero convention reads e(0,1)=1=0 in the zero ring; the two displayed identities remain consistent. For a point base, ε0 with unit orientation contributes e=1∈H0(∗;R)=R and εn with n≥1 contributes e=0∈Hn(∗;R)=0. For the zero ring both classes coincide with the unique element, so the identities hold. The section of step 1.2 is a specified function and no choice is made in it; AC is used only through the Thom suppliers that give the Euler class its value.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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