Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

The complex orientation of the underlying real bundle

Statement

Assume AC. Let EB be a numerable complex rank-n vector bundle over a CW complex and let ER be its underlying real bundle.

  1. ER carries a canonical integral orientation, the complex orientation: on a local complex frame (v1,,vn) the ordered real frame (v1,iv1,,vn,ivn) is positive. The orientation is independent of the complex frame used to define it, is natural under pullback, and is preserved by complex-linear bundle isomorphisms.
  2. For numerable complex bundles E,F over B, the complex orientation of (EF)R is the ordered direct-sum orientation of the complex orientations of ER and FR.
  3. Let V be a numerable real bundle of rank 2n over B with an integral orientation o, and let φ:VCVV be the canonical real-linear isomorphism v(a+ib)(av,bv). Then φ carries the complex orientation of (VC)R to (1)n times the product orientation oo; consequently e((VC)R)=(1)ne(V)2 in H4n(B;Z).

The rank-zero case is included: ER is the zero bundle with its canonical orientation and e(0B)=1.

Facts & Assumptions

[A1]

The Axiom of Choice is assumed, exactly as inherited by the numerability, Thom and Euler-class suppliers used below (The Axiom of Choice).

[F1]

The underlying real bundle ER is obtained by regarding the complex transition matrices as real-linear; the construction commutes with pullback and with direct sums (Whitney sum, tensor, dual, Hom, and exterior-power bundles). Complexification, passage to the underlying real bundle and finite direct sums use the same trivializing cover, so a partition of unity numerating that cover also numerates each resulting bundle.

[F2]

For positive rank, an orientation of a real bundle is a continuous choice of one of the two fiber orientations and is determined by positive local frames; the zero vector space and every rank-zero bundle have one canonical orientation (Oriented real bundles and oriented frame bundles).

[F3]

Bundles over a common cover are glued from their transition cocycles, and the cocycle determines the bundle up to canonical isomorphism (Vector bundles are glued from transition cocycles).

[F4]

For R-oriented numerable real bundles the Euler class is natural under orientation-preserving pullback, negates under orientation reversal over Z, and multiplies over ordered direct sums (Naturality, orientation sign, and Whitney product for Euler classes).

[F5]

Every endomorphism of a finite-dimensional complex vector space is upper triangularisable (Every finite-dimensional endomorphism over an algebraically closed field is triangularisable).

[F6]

The determinant of a block upper triangular real matrix is the product of the determinants of its diagonal blocks (The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks).

[F7]

The Euler class of a rank-zero bundle is the unit e(0B)=1 (Euler class by zero-section pullback of the Thom class).

Proof

technique · direct

Given: AC, numerable complex bundles over B as in statements 1 and 2, a numerable oriented real rank-2n bundle VB as in statement 3, and local complex frames (v1,,vn) and (w1,,wn) over a common open set.

1.1

The list (v1,iv1,,vn,ivn) is a real basis of each fiber: since the vj form a complex basis, j(ajvj+bjivj)=j(aj+ibj)vj vanishes only when all aj+ibj=0, that is, all aj=bj=0. Hence the list orients the fibers of ER over the chart, and by [F2] these local data are the candidate local orientations.

F1F2given
2.1

Compatibility on overlaps. Let AGLn(C) be the complex change-of-frame matrix wj=iAijvi. In the real bases of step 1.1 the change-of-frame matrix is the realification RA obtained by replacing every complex entry by its 2×2 real block; realification is multiplicative in the sense RAB=RARB, because it is the matrix of the same complex-linear map read in real coordinates. By [F5] choose a complex basis in which A is upper triangular; then RA is block upper triangular with diagonal blocks (ajbjbjaj) for the diagonal entries aj+ibj of A. By [F6] its determinant is the product of the block determinants j(aj2+bj2)=detCA2>0. A positive determinant means the two ordered real frames induce the same orientation, and multiplicativity of realification reduces every frame pair to this comparison.

F5F6step 1.1algebra
2.2

Complexification. Let (e1,,e2n) be an oriented real basis of a fiber of V. The vectors e1,,e2n are a complex basis of the complexification, so by step 1.1 the complex orientation of (VC)R is represented by the ordered real basis e1,ie1,e2,ie2,,e2n,ie2n. Under the isomorphism φ of statement 3 this list becomes (e1,0),(0,e1),(e2,0),(0,e2),,(e2n,0),(0,e2n), while the product orientation oo is represented by the blocked list (e1,0),,(e2n,0),(0,e1),,(0,e2n). Passing from the interleaved list to the blocked list is the shuffle of two length-2n blocks; its inversion number is 0+1++(2n1)=2n(2n1)/2=n(2n1), so the orientation sign is (1)n(2n1)=(1)n.

F1givenalgebra
3.1

Hence the local orientations of steps 1.1 and 2.1 agree on every overlap of a complex linear atlas, and [F3] glues them into a global integral orientation of ER, the complex orientation. The same determinant computation with A the transition function of a pullback chart gives naturality under pullback, and with A the matrix of a complex-linear isomorphism it gives invariance under complex-linear bundle isomorphisms.

F1F3step 2.1
3.2

For rank n=0 the frame list of step 1.1 is empty and the determinant computation of step 2.1 is vacuous, so the zero bundle carries its canonical orientation; [F7] supplies e(0B)=1 for use below.

F7step 1.1
3.3

Taking Euler classes. The numeration of V also numerates VC, (VC)R and VV by [F1], so every Euler class in this step lies in the scope of [F4]. If two orientations of a real bundle differ by a sign ε=±1 on positive frames, their Euler classes differ by the same ε by the orientation-sign clause of [F4]; for the ordered direct sum VV the Whitney product clause of [F4] gives e(VV)=e(V)e(V). Therefore e((VC)R)=(1)ne(VV)=(1)ne(V)2, which is statement 3.

F1F4step 2.2
4.1

Direct sums. A local complex frame of EF is the concatenation of a complex frame (v1,,vm) of E and a complex frame (w1,,wk) of F, so the real frame of step 1.1 is (v1,iv1,,vm,ivm,w1,iw1,,wk,iwk), exactly the ordered direct-sum frame of the complex-oriented summands ER and FR. By [F2] the two orientations coincide, so statement 2 holds, and the rank-zero case is step 3.2.

F1F2step 1.1step 3.2
5.1

Boundary cases. Rank zero is step 3.2. In statement 2, step 4.1 says that the complex orientation on 0F is the ordered sum of the canonical orientation on 0 and the complex orientation on F; only after applying the Whitney product formula [F4] and e(0)=1 from [F7] does one obtain e(0F)=1e(F). In statement 3 with n=0, both sides are the unit. For a complex line, n=1 in step 2.1 gives detCA2>0 directly, and for V of rank 2 step 2.2 has inversion number 21/2=1 and sign (1)1=1. The argument uses no choice beyond the inherited numerability data recorded in [A1].

A1F4F7step 3.2step 4.1step 2.2

Source notes

The orientation convention (v,iv) on a complex line and its determinant computation are the standard ones of Milnor-Stasheff, Lemma 14.1, and the (1)n comparison of the complex orientation of VC with the product orientation of VV is Hatcher, Vector Bundles & K-Theory section 3.2, proof of Proposition 3.15(b), printed pp. 94-96 ("n(2n-1) transpositions, so a sign (-1)^n").

Depends on

Used by

Dependency tree · two levels

33 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