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.
Conjugations and real structures on a complex vector space
Definition
Let be a complex vector space. A conjugation (also called a real structure) on is a map such that for all and :
- ;
- , where is complex conjugation;
- .
Thus a conjugation is additive, conjugate-linear (anti-linear) in the scalar action, and an involution. When is a real vector space, the canonical conjugation on the complexification of Complexification as with its canonical real-linear embedding is
its well-definedness on the tensor product follows from Universal property of the tensor product for balanced maps into abelian groups, applied to the -bilinear map .
Remarks
On a nonzero complex vector space, a conjugation is not complex-linear: if it were, then for every one would have both and , forcing because is an involution. On the zero space the unique conjugation is also complex-linear. Every conjugation is -linear, because for every .
Depends on
Used by
- Real forms of a complex vector space correspond exactly to conjugations Corollary
- The fixed real form of a conjugation Definition
- A complex-linear operator comes from a real operator exactly when it commutes with the chosen conjugation Theorem
- For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs Theorem
- The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space Theorem
Dependency tree · two levels
11 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
- Mikhail Troshkin, Real-complex linear algebra and abelian varieties (standard reference, not scraped)