Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29
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 tensor and direct-sum models of complexification are canonically complex-linearly isomorphic

Statement

Let V be a real vector space. The map

Φ:CRVViV,Φ(zv):=z(v,0),

is a complex-linear isomorphism between the tensor model of Complexification as CRV with its canonical real-linear embedding and the direct-sum model of The direct-sum model ViV of a complexification. Its inverse is

Ψ:ViVCRV,Ψ(v+iw):=1v+iw.

Facts & Assumptions

Given: A real vector space V, with C regarded as a real vector space through RC.

[L1]

The complexification VC=CRV carries the complex scalar action z(zv)=(zz)v and the real-linear embedding ιv=1v (Complexification as CRV with its canonical real-linear embedding).

[L2]

The direct-sum model is ViV with (a+bi)(v,w)=(avbw,aw+bv), written v+iw=(v,w) (The direct-sum model ViV of a complexification).

[L3]

Every R-balanced map b:C×VA into a real vector space A extends uniquely to an R-linear map CRVA sending zv to b(z,v) (Universal property of the tensor product for balanced maps into abelian groups).

Proof

technique · direct
1.1

The map b:C×VViV, b(z,v)=z(v,0), is R-bilinear: it is additive in each variable because the addition in ViV is componentwise, and for rR one has b(zr,v)=(zr)(v,0)=z(r(v,0))=z(rv,0)=b(z,rv) by [L2].

givenL2algebra
2.1

By [L3] there is a unique R-linear map Φ:CRVViV with Φ(zv)=z(v,0).

step 1.1L3
3.1

The map Ψ(v+iw)=1v+iw satisfies ΨΦ=id on elementary tensors: writing z=a+bi, one has Ψ(Φ(zv))=Ψ(av+ibv)=1(av)+i(bv)=a(1v)+b(iv)=(a+bi)(1v)=zv by the scalar action of [L1].

step 2.1L1L2algebra
3.2

Conversely ΦΨ=id: Φ(1v+iw)=(v,0)+i(w,0)=(v,0)+(0,w)=(v,w)=v+iw by [L2].

step 2.1L1L2algebra
3.3

The map Φ is complex-linear: for z,zC, Φ(z(zv))=Φ((zz)v)=(zz)(v,0)=z(z(v,0))=zΦ(zv) by [L1] and [L2], and the identity extends from elementary tensors by additivity.

step 2.1L1L2algebra
4.1

Steps 3.1 and 3.2 make Φ bijective with inverse Ψ, and step 3.3 makes it complex-linear, so Φ is the claimed canonical complex-linear isomorphism.

step 3.1step 3.2step 3.3

Depends on

Used by

Dependency tree · two levels

10 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