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 be a real vector space. The map
is a complex-linear isomorphism between the tensor model of Complexification as with its canonical real-linear embedding and the direct-sum model of The direct-sum model of a complexification. Its inverse is
Facts & Assumptions
Given: A real vector space , with regarded as a real vector space through .
The complexification carries the complex scalar action and the real-linear embedding (Complexification as with its canonical real-linear embedding).
The direct-sum model is with , written (The direct-sum model of a complexification).
Every -balanced map into a real vector space extends uniquely to an -linear map sending to (Universal property of the tensor product for balanced maps into abelian groups).
Proof
The map , , is -bilinear: it is additive in each variable because the addition in is componentwise, and for one has by [L2].
By [L3] there is a unique -linear map with .
The map satisfies on elementary tensors: writing , one has by the scalar action of [L1].
Conversely : by [L2].
The map is complex-linear: for , by [L1] and [L2], and the identity extends from elementary tensors by additivity.
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.
Depends on
Used by
- Real forms of a complex vector space correspond exactly to conjugations Corollary
- Complexifying a real polynomial space gives the same degree bound with complex coefficients Example
- The standard embedding ℝⁿ↪ℂⁿ is the canonical complexification map Example
- A real basis becomes a complex basis after complexification, so dim_ℂ(ℂ⊗_ℝV)=dim_ℝV Theorem
- Complexification is initial for real-linear maps into complex vector spaces, and is unique up to unique isomorphism Theorem
- Complexification preserves kernels, images, finite rank, nullity, and short exact sequences Theorem
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
- Keith Conrad, Complexification (notes) (standard reference, not scraped)
- Mikhail Troshkin, Real-complex linear algebra and abelian varieties (standard reference, not scraped)