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 θ:VC→W 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:W→W commutes with σ if and only if T=θ∘SC∘θ−1 for a real-linear operator S:V→V; in that case S is unique and is the restriction S=T∣V.

Facts & Assumptions

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

[L1]

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

[L2]

A conjugation is conjugate-linear and an involution; the canonical conjugation on VC is σcan⁡(z⊗v)=z‾⊗v, 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 θ(z⊗v)=zv is a complex-linear isomorphism, and θ(1⊗v)=v (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).

Proof

technique · direct
1.1L1L2L4algebra

If T=θ∘SC∘θ−1 for a real-linear S, then T commutes with σ: for w=θ(z⊗v), one has Tσw=θSCθ−1θσcan⁡(z⊗v)=θSC(z‾⊗v)=θ(z‾⊗Sv), while σTw=θσcan⁡θ−1θ(z⊗Sv)=θ(z‾⊗Sv) by [L1] and [L2].

1.2L2L3

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

2.1step 1.2L1L4algebra

With this S, one has θ∘SC∘θ−1=T: for w=θ(z⊗v), θSC(z⊗v)=θ(z⊗Sv)=z⋅Sv=T(z v)=T(θ(z⊗v))=Tw, using [L1], the complex-linearity of T, and the identity θ(1⊗v)=v of [L4].

3.1step 2.1L1L4

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

4.1step 1.1step 2.1step 3.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.

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