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.
Complexification as with its canonical real-linear embedding
Definition
Let be a real vector space (Vector space over a field) and regard as a real vector space through the constant-class map of The complex numbers as , with the real embedding and imaginary unit . The complexification of is the real tensor product
It becomes a complex vector space through the scalar action
and it carries the canonical real-linear embedding
The scalar action is well defined. For fixed the map from to is additive in each variable and -balanced, so by Universal property of the tensor product for balanced maps into abelian groups it induces a unique -linear map with . The identities , and hold on every elementary tensor and hence everywhere, so the action makes a complex vector space.
Remarks
The tensor product is over , and the construction is basis-independent. Every element of is a finite sum with and ; after writing each summand is .
Depends on
Used by
- Complexification of a real-linear map Definition
- Conjugations and real structures on a complex vector space Definition
- The direct-sum model V⊕ iV of a complexification Definition
- 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
- The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space Theorem
- The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic Theorem
Dependency tree · two levels
18 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)