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.
Real forms of a complex vector space correspond exactly to conjugations
Statement
Let be a complex vector space. Call a real subspace a real form of when the map , , is a complex-linear isomorphism. Then the assignments
where is the conjugation on transported from the canonical conjugation of along , are inverse bijections between the conjugations of and the real forms of . The canonical conjugation of Conjugations and real structures on a complex vector space is .
Facts & Assumptions
Given: A complex vector space .
The fixed points of a conjugation form a real subspace whose complexification recovers the ambient complex space (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).
A conjugation is additive, conjugate-linear, and an involution; on the complexification of a real space the canonical conjugation is (Conjugations and real structures on a complex vector space).
The fixed real form of a conjugation is the real subspace of its fixed points (The fixed real form of a conjugation).
Every element of the complexification is uniquely with (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).
Proof
For a conjugation , the subspace is a real form of : by [L1] the complexification of recovers through the multiplication map, which is exactly the defining condition.
The fixed points of on are the embedded copy of : by [L4] an element is uniquely , and by [L2], which equals itself exactly when , hence .
For a real form with isomorphism , define . It is additive and conjugate-linear because is complex-linear and has these properties by [L2], and it is an involution because .
If came from a conjugation , then : for with , step 1.3 gives , while by [L2].
If came from a real form , then : the fixed points of in are the -images of the fixed points of , which step 1.2 identifies with the embedded copy of , and by the real-form condition.
Steps 1.1, 2.1 and 2.2 show that the two assignments compose to the identity in both orders, so they are inverse bijections.
Depends on
- The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space
- Conjugations and real structures on a complex vector space
- The fixed real form of a conjugation
- The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic
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
- Mikhail Troshkin, Real-complex linear algebra and abelian varieties (standard reference, not scraped)