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.
A complex-linear operator comes from a real operator exactly when it commutes with the chosen conjugation
Statement
Let be a complex vector space, let be a conjugation on , let be its fixed real form, and let be the canonical isomorphism of The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space. A complex-linear operator commutes with if and only if for a real-linear operator ; in that case is unique and is the restriction .
Facts & Assumptions
Given: A complex vector space , a conjugation with fixed real form , and a complex-linear operator .
The complexification of a real-linear map is (Complexification of a real-linear map).
A conjugation is conjugate-linear and an involution; the canonical conjugation on is , and (Conjugations and real structures on a complex vector space, Real forms of a complex vector space correspond exactly to conjugations).
The fixed real form is (The fixed real form of a conjugation).
The map is a complex-linear isomorphism, and (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).
Proof
If for a real-linear , then commutes with : for , one has , while by [L1] and [L2].
Conversely, if , then is invariant under : for , , so by [L3]; the restriction is therefore a well-defined real-linear operator.
With this , one has : for , , using [L1], the complex-linearity of , and the identity of [L4].
Uniqueness: if , then because is an isomorphism, and evaluating on gives , whence by the injectivity of the embedding in [L4].
Steps 1.1, 2.1 and 3.1 together prove both directions of the claimed equivalence, the concrete description of as the restriction, and its uniqueness.
Depends on
- Complexification of a real-linear map
- Conjugations and real structures on a complex vector space
- The fixed real form of a conjugation
- The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space
- Complexification is a functor on real vector spaces and real-linear maps
- Real forms of a complex vector space correspond exactly to conjugations
Used by
- A nonreal eigenvector yields an invariant real two-plane and the standard rotation-scaling block Corollary
- A complex-linear map need not preserve a chosen real form Counterexample
- FALSE: every complex-linear operator descends to every chosen real form False statement
- For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs Theorem
Dependency tree · two levels
13 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)
- Keith Conrad, Complexification (notes) (standard reference, not scraped)