Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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 W be a complex vector space, let σ be a conjugation on W, let V=Wσ be its fixed real form, and let θ:VCW 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 T:WW commutes with σ if and only if T=θSCθ1 for a real-linear operator S:VV; in that case S is unique and is the restriction S=TV.

Facts & Assumptions

Given: A complex vector space W, a conjugation σ with fixed real form V=Wσ, and a complex-linear operator T:WW.

[L1]

The complexification of a real-linear map S is SC(zv)=zS(v) (Complexification of a real-linear map).

[L2]

A conjugation is conjugate-linear and an involution; the canonical conjugation on VC is σcan(zv)=zv, and σ=θσcanθ1 (Conjugations and real structures on a complex vector space, Real forms of a complex vector space correspond exactly to conjugations).

[L3]

The fixed real form is V=Wσ={w:σw=w} (The fixed real form of a conjugation).

[L4]

The map θ(zv)=zv is a complex-linear isomorphism, and θ(1v)=v (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).

Proof

technique · direct
1.1

If T=θSCθ1 for a real-linear S, then T commutes with σ: for w=θ(zv), one has Tσw=θSCθ1θσcan(zv)=θSC(zv)=θ(zSv), while σTw=θσcanθ1θ(zSv)=θ(zSv) by [L1] and [L2].

L1L2L4algebra
1.2

Conversely, if Tσ=σT, then V is invariant under T: for vV, σ(Tv)=Tσv=Tv, so TvV by [L3]; the restriction S:=TV:VV is therefore a well-defined real-linear operator.

L2L3
2.1

With this S, one has θSCθ1=T: for w=θ(zv), θSC(zv)=θ(zSv)=zSv=T(zv)=T(θ(zv))=Tw, using [L1], the complex-linearity of T, and the identity θ(1v)=v of [L4].

step 1.2L1L4algebra
3.1

Uniqueness: if T=θSCθ1=θRCθ1, then SC=RC because θ is an isomorphism, and evaluating on 1v gives ιSv=SC(1v)=RC(1v)=ιRv, whence Sv=Rv by the injectivity of the embedding in [L4].

step 2.1L1L4
4.1

Steps 1.1, 2.1 and 3.1 together prove both directions of the claimed equivalence, the concrete description of S as the restriction, and its uniqueness.

step 1.1step 2.1step 3.1

Depends on

Used by

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