Alphabeta Math
Pipeline-generated
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.

✓ 12 results · all verified · 5 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Complexification, Realification and Real Structures

1 · Prerequisites

2 · Summary

Tensor products over a commutative ring, their universal property, uniqueness up to unique isomorphism, functoriality, and basis formulas supply the construction machinery; the complex numbers with conjugation and their algebraic laws, vector spaces, linear maps, kernels, images, rank-nullity, exact sequences, and the published minimal-polynomial and generalised-eigenspace infrastructure supply the rest.

The page introduces the two directions of scalar change between the real and complex worlds. Complexification sends a real vector space V to the tensor product C⊗RV with its canonical embedding and its concrete model V⊕iV; realification forgets the complex structure by restricting scalars to R. The page proves the universal property and uniqueness of complexification, that the tensor and direct-sum models agree, functoriality, and the preservation of kernels, images, rank, nullity, and short exact sequences; it records the opposite dimension behaviour of the two constructions. Conjugations are then introduced as conjugate-linear involutions, and their fixed points are shown to be real forms whose complexification recovers the ambient complex space, giving a bijection between conjugations and real forms. The page closes with the operator consequences: a complex-linear operator descends to a chosen real form exactly when it commutes with the conjugation; characteristic and minimal polynomials survive complexification; nonreal generalised eigenspaces occur in conjugate pairs; and one nonreal eigenvector produces the standard invariant real two-plane and rotation-scaling block.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Realification of a complex vector space by restriction of scalars

Definition

Let W be a vector space over the field C (The complex numbers as R[x]/(x2+1), with the real embedding and imaginary unit i). Its realification, written WR, is the real vector space whose underlying set and addition are those of W, and whose scalar multiplication is the restriction of the complex scalar multiplication to the canonical real embedding R⊆C:

r⋅w:=rw(r∈R, w∈W).

The axioms of a real vector space are the restriction of the corresponding complex axioms: complex scalar multiplication is already an R-scalar multiplication, since R is a subfield of C through the constant-class map of The complex numbers as R[x]/(x2+1), with the real embedding and imaginary unit i.

Remarks

Realification forgets the chosen complex structure: different complex structures on the same abelian group can have the same realification. The definition is the prototype of restriction of scalars along R⊆C; no basis and no choice of coordinates is involved.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Complexification as C⊗RV with its canonical real-linear embedding

Definition

Let V be a real vector space (Vector space over a field) and regard C as a real vector space through the constant-class map of The complex numbers as R[x]/(x2+1), with the real embedding and imaginary unit i. The complexification of V is the real tensor product

VC:=C⊗RV.

It becomes a complex vector space through the scalar action

z⋅(w⊗v):=(zw)⊗v(z,w∈C, v∈V),

and it carries the canonical real-linear embedding

ι:V⟶VC,ιv:=1⊗v.

The scalar action is well defined. For fixed z∈C the map (w,v)↦(zw)⊗v from C×V to VC is additive in each variable and R-balanced, so by Universal property of the tensor product for balanced maps into abelian groups it induces a unique R-linear map μz:VC→VC with μz(w⊗v)=(zw)⊗v. The identities μz+z′=μz+μz′, μzz′=μz∘μz′ and μ1=id⁡ hold on every elementary tensor and hence everywhere, so the action makes VC a complex vector space.

Remarks

The tensor product is over R, and the construction is basis-independent. Every element of VC is a finite sum ∑jzj⊗vj with zj∈C and vj∈V; after writing zj=aj+ibj each summand is aj(1⊗vj)+bj(i⊗vj).

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The direct-sum model V⊕iV of a complexification

Definition

Let V be a real vector space. The direct-sum model of the complexification of V is the complex vector space V⊕iV whose underlying set is V×V, with componentwise addition

(v,w)+(v′,w′):=(v+v′,w+w′)

and complex scalar multiplication

(a+bi)⋅(v,w):=(av−bw, aw+bv)(a,b∈R, v,w∈V).

An element is written v+iw for the pair (v,w), so that i(v+iw)=−w+iv; the distinguished copy of V is the real subspace of pairs (v,0). This is the concrete model compared with the tensor model VC of Complexification as C⊗RV with its canonical real-linear embedding.

Remarks

The axioms of a complex vector space are checked directly from the displayed formulas; for instance i(i(v+iw))=i(−w+iv)=−v−iw=−(v+iw), matching i2=−1. Writing v+iw is a notation for the pair, not a claim that iV is already a subspace of anything.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Complexification of a real-linear map

Definition

Let T:V→W be a real-linear map between real vector spaces (Linear map between vector spaces over the same field). Its complexification is the R-linear map

TC:=id⁡C⊗T:C⊗RV⟶C⊗RW,TC(z⊗v):=z⊗T(v).

Existence. The map (z,v)↦z⊗T(v) from C×V to C⊗RW is additive in each variable and R-balanced because T is real-linear, so Universal property of the tensor product for balanced maps into abelian groups supplies the unique R-linear map with the displayed value on elementary tensors.

Remarks

The map TC is complex-linear on the complexifications of Complexification as C⊗RV with its canonical real-linear embedding: for z,z′∈C and v∈V,

TC(z′⋅(z⊗v))=TC((z′z)⊗v)=(z′z)⊗T(v)=z′⋅(z⊗T(v))=z′⋅TC(z⊗v),

so the identities extend from elementary tensors to all of C⊗RV by additivity.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Conjugations and real structures on a complex vector space

Definition

Let W be a complex vector space. A conjugation (also called a real structure) on W is a map σ:W→W such that for all w,w′∈W and z∈C:

  1. σ(w+w′)=σ(w)+σ(w′);
  2. σ(zw)=z‾ σ(w), where z‾ is complex conjugation;
  3. σ(σ(w))=w.

Thus a conjugation is additive, conjugate-linear (anti-linear) in the scalar action, and an involution. When V is a real vector space, the canonical conjugation on the complexification VC of Complexification as C⊗RV with its canonical real-linear embedding is

σcan⁡(z⊗v):=z‾⊗v;

its well-definedness on the tensor product follows from Universal property of the tensor product for balanced maps into abelian groups, applied to the R-bilinear map (z,v)↦z‾⊗v.

Remarks

On a nonzero complex vector space, a conjugation is not complex-linear: if it were, then for every w one would have both σ(iw)=−iσ(w) and σ(iw)=iσ(w), forcing w=0 because σ is an involution. On the zero space the unique conjugation is also complex-linear. Every conjugation is R-linear, because r‾=r for every r∈R.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The fixed real form of a conjugation

Definition

Let σ be a conjugation on the complex vector space W (Conjugations and real structures on a complex vector space). Its fixed real form is the real subspace

Wσ:={ w∈W:σ(w)=w }⊆WR,

where WR is the realification of W. That Wσ is a real subspace is immediate: it contains 0, is closed under addition because σ is additive, and is closed under real scalars because σ(rw)=r‾ σ(w)=rw for r∈R.

Remarks

The same complex vector space can carry different conjugations with different fixed real forms; a fixed real form is extra structure attached to the choice of σ, not canonical data of W alone.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic

Statement

Let V be a real vector space. The map

Φ:C⊗RV⟶V⊕iV,Φ(z⊗v):=z(v,0),

is a complex-linear isomorphism between the tensor model of Complexification as C⊗RV with its canonical real-linear embedding and the direct-sum model of The direct-sum model V⊕iV of a complexification. Its inverse is

Ψ:V⊕iV⟶C⊗RV,Ψ(v+iw):=1⊗v+i⊗w.

Facts & Assumptions

Given: A real vector space V, with C regarded as a real vector space through R⊆C.

[L1]

The complexification VC=C⊗RV carries the complex scalar action z′⋅(z⊗v)=(z′z)⊗v and the real-linear embedding ιv=1⊗v (Complexification as C⊗RV with its canonical real-linear embedding).

[L2]

The direct-sum model is V⊕iV with (a+bi)⋅(v,w)=(av−bw, aw+bv), written v+iw=(v,w) (The direct-sum model V⊕iV of a complexification).

[L3]

Every R-balanced map b:C×V→A into a real vector space A extends uniquely to an R-linear map C⊗RV→A sending z⊗v to b(z,v) (Universal property of the tensor product for balanced maps into abelian groups).

Proof

technique · direct
1.1givenL2algebra

The map b:C×V→V⊕iV, b(z,v)=z(v,0), is R-bilinear: it is additive in each variable because the addition in V⊕iV is componentwise, and for r∈R one has b(zr,v)=(zr)(v,0)=z(r(v,0))=z(rv,0)=b(z,rv) by [L2].

2.1step 1.1L3

By [L3] there is a unique R-linear map Φ:C⊗RV→V⊕iV with Φ(z⊗v)=z(v,0).

3.1step 2.1L1L2algebra

The map Ψ(v+iw)=1⊗v+i⊗w satisfies Ψ∘Φ=id⁡ on elementary tensors: writing z=a+bi, one has Ψ(Φ(z⊗v))=Ψ(av+ibv)=1⊗(av)+i⊗(bv)=a(1⊗v)+b(i⊗v)=(a+bi)(1⊗v)=z⊗v by the scalar action of [L1].

3.2step 2.1L1L2algebra

Conversely Φ∘Ψ=id⁡: Φ(1⊗v+i⊗w)=(v,0)+i(w,0)=(v,0)+(0,w)=(v,w)=v+iw by [L2].

3.3step 2.1L1L2algebra

The map Φ is complex-linear: for z,z′∈C, Φ(z′⋅(z⊗v))=Φ((z′z)⊗v)=(z′z)(v,0)=z′(z(v,0))=z′Φ(z⊗v) by [L1] and [L2], and the identity extends from elementary tensors by additivity.

4.1step 3.1step 3.2step 3.3∎

Steps 3.1 and 3.2 make Φ bijective with inverse Ψ, and step 3.3 makes it complex-linear, so Φ is the claimed canonical complex-linear isomorphism.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Complexification is initial for real-linear maps into complex vector spaces, and is unique up to unique isomorphism

Statement

Let V be a real vector space and let ι:V→VC be the canonical real-linear embedding of Complexification as C⊗RV with its canonical real-linear embedding. For every complex vector space W and every real-linear map f:V→W there is a unique complex-linear map F:VC→W with F∘ι=f, namely F(z⊗v)=z f(v).

Moreover, if U is a complex vector space and ι′:V→U is a real-linear map with the same property, then there is a unique complex-linear isomorphism u:VC→U with u∘ι=ι′.

Facts & Assumptions

Given: A real vector space V with canonical embedding ι:V→VC, and a real-linear map f:V→W into a complex vector space W.

[L1]

The complexification carries the scalar action z′⋅(z⊗v)=(z′z)⊗v and ιv=1⊗v (Complexification as C⊗RV with its canonical real-linear embedding).

[L2]

Every R-balanced map b:C×V→A extends uniquely to an R-linear map out of C⊗RV (Universal property of the tensor product for balanced maps into abelian groups).

[L3]

Two pairs representing the same class of balanced maps are related by a unique isomorphism commuting with the structure maps, obtained by applying each universal property to the other pair (Tensor products are unique up to a unique isomorphism carrying elementary tensors to elementary tensors).

Proof

technique · direct
1.1givenL2algebra

The map b:C×V→W given by b(z,v)=z f(v) is R-bilinear and R-balanced: additivity follows from the linearity of f in v and the distributivity of complex scalar multiplication, and b(zr,v)=(zr)f(v)=z(r f(v))=z f(rv)=b(z,rv) for r∈R.

1.2L1givenalgebra

Uniqueness of any extension: if G:VC→W is complex-linear with G∘ι=f, then G(z⊗v)=G(z⋅(1⊗v))=z G(1⊗v)=z f(v) on every elementary tensor by [L1], so its values are already determined, and elementary tensors generate VC.

2.1step 1.1L2

By [L2] there is a unique R-linear map F:VC→W with F(z⊗v)=z f(v).

3.1step 2.1L1algebra

The map F is complex-linear: by the scalar action of [L1], F(z′⋅(z⊗v))=F((z′z)⊗v)=(z′z)f(v)=z′(z f(v))=z′F(z⊗v), and additivity extends the identity to all of VC.

3.2step 2.1L1

The map F satisfies F∘ι=f because F(ιv)=F(1⊗v)=f(v) by [L1].

3.3step 1.2step 2.1

Uniqueness: steps 1.2 and 2.1 show that any complex-linear extension G with G∘ι=f agrees with F on every elementary tensor, hence everywhere, so G=F.

4.1step 3.3L3

For the uniqueness up to unique isomorphism, apply the universal property of (VC,ι) to ι′ to get a unique complex-linear u:VC→U with u∘ι=ι′, and the universal property of (U,ι′) to ι to get v:U→VC with v∘ι′=ι. Both v∘u and id⁡ carry ι to itself, and both u∘v and id⁡ carry ι′ to itself, so step 3.3 forces both composites to be identities; this is the two-application argument recorded in [L3].

5.1step 3.1step 3.2step 3.3step 4.1∎

Steps 3.1 and 3.2 prove the universal property, step 3.3 its uniqueness clause, and step 4.1 the uniqueness of the representing pair up to unique isomorphism.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Complexification is a functor on real vector spaces and real-linear maps

Statement

For real vector spaces V,W,U and real-linear maps T:V→W and S:W→U, the complexification of Complexification of a real-linear map satisfies

(id⁡V)C=id⁡VC,(S∘T)C=SC∘TC.

Thus V↦VC, T↦TC is a functor from real vector spaces to complex vector spaces.

Facts & Assumptions

Given: Real-linear maps T:V→W and S:W→U.

[L1]

The complexification of a real-linear map is TC=id⁡C⊗T, with TC(z⊗v)=z⊗T(v) (Complexification of a real-linear map).

[L2]

For homomorphisms of right and left modules, id⁡⊗id⁡=id⁡ and (f′∘f)⊗(g′∘g)=(f′⊗g′)∘(f⊗g) (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

technique · direct
1.1L1L2

By [L2] applied with f=f′=id⁡C and g=id⁡V, one has (id⁡V)C=id⁡C⊗id⁡V=id⁡VC by [L1].

1.2L1L2algebra

By [L2] applied with f=f′=id⁡C, g=T and g′=S, one has (S∘T)C=id⁡C⊗(S∘T)=(id⁡C∘id⁡C)⊗(S∘T)=(id⁡C⊗S)∘(id⁡C⊗T)=SC∘TC by [L1].

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 are exactly the identity and composition laws of a functor.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Complexification preserves kernels, images, finite rank, nullity, and short exact sequences

Statement

Let T:V→W be a real-linear map. Under the canonical isomorphism of The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic, the complexification acts componentwise: TC(v+iw)=Tv+iTw. Consequently

ker⁡(TC)=(ker⁡T)⊕i(ker⁡T),im⁡(TC)=(im⁡T)⊕i(im⁡T),

the complexifications of the real subspaces. If V and W are finite-dimensional, then rank⁡C(TC)=rank⁡R(T) and nullity⁡C(TC)=nullity⁡R(T). If 0→U→iV→pW→0 is a short exact sequence of real vector spaces, then

0⟶UC→iCVC→pCWC⟶0

is a short exact sequence of complex vector spaces.

Facts & Assumptions

Given: A real-linear map T:V→W, and in the exactness clause real-linear maps i:U→V and p:V→W with p∘i=0.

[L1]

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

[L2]

The canonical isomorphism Φ:C⊗RV→V⊕iV satisfies Φ(z⊗v)=z(v,0), with inverse Ψ(v+iw)=1⊗v+i⊗w (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

[L3]

Kernel and image of a linear map are linear subspaces, and a linear map is injective exactly when its kernel is zero (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial).

[L4]

For a linear map from a finite-dimensional space, dim⁡V=nullity⁡T+rank⁡T (Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T).

[L5]

A short exact sequence is exact at every displayed module, so im⁡i=ker⁡p at the middle term (Exact sequences and short exact sequences of modules).

[L6]

Complexification of maps respects composition: (p∘i)C=pC∘iC (Complexification is a functor on real vector spaces and real-linear maps).

Proof

technique · direct
1.1L1L2algebra

In the direct-sum model, TC(v+iw)=Tv+iTw: applying Φ to the formula of [L1], Φ(TC(1⊗v+i⊗w))=Φ(1⊗Tv+i⊗Tw)=Tv+iTw by [L2].

1.2L2algebra

If U≤V is a real subspace with real basis u1,…,um, then every element of U⊕iU is ∑j≤m(aj+ibj)uj with aj,bj∈R: the real and imaginary components are real combinations of the uj.

1.3L2algebra

The list u1,…,um is complex-linearly independent in U⊕iU: ∑j(aj+ibj)uj=0 means (∑jajuj,∑jbjuj)=(0,0) in V⊕iV, and the real independence of the uj forces every aj=bj=0.

1.4L6givenalgebra

By [L6] and the hypothesis p∘i=0, one has pC∘iC=0, hence im⁡iC⊆ker⁡pC.

2.1step 1.1L2L3

ker⁡(TC)={v+iw:Tv=Tw=0}=(ker⁡T)⊕i(ker⁡T): the equality of the two descriptions is step 1.1, and by [L3] the kernel of the componentwise map is the complexification of ker⁡T.

2.2step 1.1L2

im⁡(TC)={Tv+iTw}=(im⁡T)⊕i(im⁡T), again directly from step 1.1.

2.3step 1.2step 1.3

For a finite-dimensional real subspace U, steps 1.2 and 1.3 exhibit u1,…,um as a complex basis of U⊕iU, so dim⁡C(U⊕iU)=dim⁡RU.

3.1step 2.1step 2.2step 2.3L4

Combining steps 2.1, 2.2 and 2.3 gives nullity⁡C(TC)=dim⁡Cker⁡(TC)=dim⁡Rker⁡T=nullity⁡R(T) and the matching rank identity, with rank and nullity as in [L4].

3.2step 2.1step 2.2L5

At the middle term, ker⁡pC=(ker⁡p)⊕i(ker⁡p)=(im⁡i)⊕i(im⁡i)=im⁡iC by [L5] and steps 2.1 and 2.2 applied to i and p.

3.3step 2.1step 2.2L3

The map iC is injective because ker⁡iC=(ker⁡i)⊕i(ker⁡i)=0 by [L3], and pC is surjective because im⁡pC=(im⁡p)⊕i(im⁡p)=WC.

4.1step 1.4step 3.2step 3.3L5

By [L5], exactness of the complexified sequence is: 0=ker⁡iC at UC, im⁡iC=ker⁡pC at VC, and im⁡pC=WC at WC; these are step 3.3, step 3.2 and step 3.3 respectively, with the containment of step 1.4 absorbed into the equality.

5.1step 3.1step 4.1∎

Steps 2.1 and 2.2 prove the kernel and image formulas, step 3.1 the rank and nullity preservation, and step 4.1 the short-exact-sequence clause.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

A real basis becomes a complex basis after complexification, so dim⁡C(C⊗RV)=dim⁡RV

Statement

Let V be a real vector space with ordered basis B=(v1,…,vn). Then (ιv1,…,ιvn) is an ordered complex basis of the complexification VC of Complexification as C⊗RV with its canonical real-linear embedding. In particular, if V is finite-dimensional then

dim⁡C(C⊗RV)=dim⁡RV.

Facts & Assumptions

Given: A real vector space V with ordered basis (v1,…,vn).

[L1]

If M and N are free with bases (ei) and (fj), then M⊗N is free with basis (ei⊗fj) (The elementary tensors of two bases form the product basis of the tensor product).

[L2]

The power basis 1,i is an R-basis of C, and C=R(i) (C/R has power basis 1,i and degree 2).

[L3]

The canonical isomorphism Φ:C⊗RV→V⊕iV sends z⊗v to z(v,0), with inverse Ψ(v+iw)=1⊗v+i⊗w (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

[L5]

The dimension of a finite-dimensional vector space is the size of any of its bases (Finite-dimensional vector space, and its dimension dim⁡FV; infinite-dimensional means having no finite basis).

Proof

technique · direct
1.1L1L2L4

By [L2], {1,i} is an R-basis of C, and by hypothesis (v1,…,vn) is an R-basis of V; hence [L1] makes {1⊗vj, i⊗vj:j≤n} an R-basis of C⊗RV.

1.2L3algebra

Transporting through the inverse isomorphism Ψ of [L3], which sends 1⊗vj to vj and i⊗vj to ivj, the set {vj, ivj:j≤n} is an R-basis of V⊕iV.

2.1step 1.2L4algebra

The vectors v1,…,vn span V⊕iV over C: every element v+iw is ∑jajvj+i∑jbjvj=∑j(aj+ibj)vj by the real basis expansion of step 1.2.

2.2step 1.2algebra

The vectors v1,…,vn are complex-linearly independent: if ∑j(aj+ibj)vj=0, then (∑jajvj,∑jbjvj)=(0,0), so the real independence in step 1.2 forces every aj=bj=0.

3.1step 2.1step 2.2L3L4

Steps 2.1 and 2.2 make (v1,…,vn) an ordered complex basis of the direct-sum model, and applying Φ of [L3] carries it to the ordered complex basis (ιv1,…,ιvn) of VC.

4.1step 3.1L5∎

Both bases have exactly n elements, so by [L5] the complex dimension of VC equals the real dimension of V.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Realification doubles finite dimension

Statement

If W is a finite-dimensional complex vector space with dim⁡CW=n, then its realification WR of Realification of a complex vector space by restriction of scalars is finite-dimensional over R with

dim⁡RWR=2n.

Facts & Assumptions

Given: A finite-dimensional complex vector space W with dim⁡CW=n.

[L1]

The realification WR is the real vector space with the same underlying set and addition, and scalar multiplication restricted to R⊆C (Realification of a complex vector space by restriction of scalars).

[L2]

In C=R[x]/(x2+1) with i=x+(x2+1), every complex number is written uniquely as a+bi with a,b∈R and i2=−1 (The complex numbers as R[x]/(x2+1), with the real embedding and imaginary unit i).

[L4]

The dimension of a finite-dimensional vector space is the size of any of its bases (Finite-dimensional vector space, and its dimension dim⁡FV; infinite-dimensional means having no finite basis).

Proof

technique · direct
1.1L4choose

Choose an ordered complex basis (e1,…,en) of W, which exists because W is finite-dimensional over C by [L4].

2.1step 1.1L1L2algebra

The list (e1,ie1,…,en,ien) spans WR: writing w=∑jzjej and zj=aj+ibj by [L2], one has w=∑jajej+∑jbj(iej) by the scalar-multiplication restriction of [L1].

2.2step 1.1L3algebra

The list is linearly independent over R: if ∑jajej+∑jbj(iej)=0 with real coefficients, then ∑j(aj+ibj)ej=0 in W, so the complex independence of (e1,…,en) forces every aj+ibj=0 and hence every aj=bj=0; in particular the displayed entries are pairwise distinct.

3.1step 2.1step 2.2L3L4∎

By [L3], steps 2.1 and 2.2 make the displayed list a real basis of WR with 2n entries, so [L4] gives dim⁡RWR=2n.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space

Statement

Let σ be a conjugation on a complex vector space W. The fixed real form Wσ of The fixed real form of a conjugation is a real subspace of WR, and the map

θ:C⊗RWσ⟶W,θ(z⊗w)=z w,

is a complex-linear isomorphism whose restriction to the canonical embedding of Wσ is the inclusion Wσ↪W. Thus the complexification of Wσ canonically recovers W.

Facts & Assumptions

Given: A complex vector space W with a conjugation σ.

[L1]

A conjugation is additive, conjugate-linear, and an involution: σ(w+w′)=σw+σw′, σ(zw)=z‾ σw, σσw=w (Conjugations and real structures on a complex vector space).

[L2]

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

[L3]

A real-linear map f:Wσ→W extends to a unique complex-linear map from the complexification of Wσ (Complexification is initial for real-linear maps into complex vector spaces, and is unique up to unique isomorphism).

[L4]

Complex conjugation satisfies z+w‾=z‾+w‾, zw‾=z‾ w‾ and z‾‾=z (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L5]

The complexification of a real space carries the scalar action z′⋅(z⊗v)=(z′z)⊗v (Complexification as C⊗RV with its canonical real-linear embedding).

Proof

technique · direct
1.1L1L2

The set Wσ is a real subspace: it contains 0, is closed under addition because σ is additive by [L1], and is closed under real scalars because σ(rw)=r‾ σw=rw for r∈R.

1.2L5L1algebra

Every element of C⊗RWσ has the form 1⊗A+i⊗B with A,B∈Wσ: a general finite sum is ∑jzj⊗wj=∑j(aj+ibj)⊗wj=∑j(aj+ibj)⋅(1⊗wj)=1⊗(∑jajwj)+i⊗(∑jbjwj) by the scalar action of [L5], and the two coefficient sums lie in the real subspace Wσ.

2.1step 1.1L3

By [L3], the real-linear inclusion Wσ↪W extends uniquely to a complex-linear map θ:C⊗RWσ→W with θ(z⊗w)=zw.

3.1step 2.1L1L2L4algebra

Surjectivity: for v∈W set A=(v+σv)/2 and B=(v−σv)/(2i). By [L1] and [L4], σA=(v+σv)/2=A, and σB=(σv−v)/(2i‾)=(v−σv)/(2i)=B because i‾=−i; hence A,B∈Wσ by [L2] and θ(1⊗A+i⊗B)=A+iB=v.

3.2step 1.2step 2.1L1algebra

Injectivity: for A,B∈Wσ one has θ(1⊗A+i⊗B)=A+iB by step 2.1. If A+iB=0, applying σ and using [L1] gives A−iB=0; subtracting the two identities gives 2iB=0, hence B=0 and then A=0, so the tensor 1⊗A+i⊗B is zero.

4.1step 2.1step 3.1step 3.2∎

Steps 2.1, 3.1 and 3.2 make θ a complex-linear isomorphism, and its restriction to ιWσ is the inclusion because θ(1⊗A)=A.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Real forms of a complex vector space correspond exactly to conjugations

Statement

Let W be a complex vector space. Call a real subspace V≤WR a real form of W when the map θ:VC→W, θ(z⊗v)=zv, is a complex-linear isomorphism. Then the assignments

σ⟼WσandV⟼σV,

where σV is the conjugation on W transported from the canonical conjugation of VC along θ, are inverse bijections between the conjugations of W and the real forms of W. The canonical conjugation of Conjugations and real structures on a complex vector space is σcan⁡(z⊗v)=z‾⊗v.

Facts & Assumptions

Given: A complex vector space W.

[L1]

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).

[L2]

A conjugation is additive, conjugate-linear, and an involution; on the complexification VC of a real space the canonical conjugation is σcan⁡(z⊗v)=z‾⊗v (Conjugations and real structures on a complex vector space).

[L3]

The fixed real form of a conjugation is the real subspace of its fixed points (The fixed real form of a conjugation).

[L4]

Every element of the complexification VC is uniquely 1⊗A+i⊗B with A,B∈V (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

Proof

technique · direct
1.1L1

For a conjugation σ, the subspace Wσ is a real form of W: by [L1] the complexification of Wσ recovers W through the multiplication map, which is exactly the defining condition.

1.2L2L4algebra

The fixed points of σcan⁡ on VC are the embedded copy of V: by [L4] an element is uniquely 1⊗A+i⊗B, and σcan⁡(1⊗A+i⊗B)=1⊗A−i⊗B by [L2], which equals itself exactly when i⊗B=−i⊗B, hence B=0.

1.3L2givenalgebra

For a real form V with isomorphism θ:VC→W, define σV(w)=θ(σcan⁡(θ−1w)). It is additive and conjugate-linear because θ is complex-linear and σcan⁡ has these properties by [L2], and it is an involution because σcan⁡2=id⁡.

2.1step 1.3L1L2

If V=Wσ came from a conjugation σ, then σV=σ: for w=A+iB with A,B∈Wσ, step 1.3 gives σV(w)=θ(1⊗A−i⊗B)=A−iB, while σ(A+iB)=A+i‾B=A−iB by [L2].

2.2step 1.2step 1.3L3

If σV came from a real form V, then WσV=θ({1⊗A:A∈V})=V: the fixed points of σV in W are the θ-images of the fixed points of σcan⁡, which step 1.2 identifies with the embedded copy of V, and θ(1⊗A)=A by the real-form condition.

3.1step 1.1step 2.1step 2.2∎

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Complexification preserves the characteristic and minimal polynomials of a finite-dimensional real operator

Statement

Let T:V→V be an endomorphism of a finite-dimensional real vector space and let TC be its complexification. Then

χTC=χT,μTC=μT,

where the minimal polynomial of T is regarded as an element of R[x]⊆C[x].

Facts & Assumptions

Given: An endomorphism T of a finite-dimensional real vector space V.

[L1]

A real ordered basis becomes an ordered complex basis after complexification (A real basis becomes a complex basis after complexification, so dim⁡C(C⊗RV)=dim⁡RV).

[L2]

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

[L3]

The characteristic polynomial of an operator is the characteristic polynomial of its matrix in any ordered basis, independent of the choice (The basis-independent characteristic polynomial χT of an endomorphism of a finite-dimensional space, including χT=1 in dimension zero).

[L4]

An operator and its matrix in an ordered basis have the same minimal polynomial (The minimal polynomial is unchanged by choosing a matrix representation or replacing a matrix by a similar one).

[L5]

For a field extension K/F, a matrix A∈Mn(F) has the same minimal polynomial over F and over K (For a matrix over a field, extending the scalar field does not change its minimal polynomial).

Proof

technique · direct
1.1L1L2

Choose an ordered real basis B=(v1,…,vn) of V; by [L1], (ιv1,…,ιvn) is an ordered complex basis of VC, and by [L2] the matrix of TC in it equals the matrix A=[T]B, because TC(ιvj)=ιTvj.

2.1step 1.1L3

By [L3], χT is the characteristic polynomial of A over R and χTC is the characteristic polynomial of the same matrix A over C; the two polynomials have the same coefficients, so χTC=χT.

2.2step 1.1L4

By [L4], μT is the minimal polynomial of A over R and μTC is the minimal polynomial of A over C.

3.1step 2.2L5

By [L5] with K=C and F=R, the minimal polynomial of A is the same element of R[x]⊆C[x] in both readings, so step 2.2 gives μTC=μT.

4.1step 2.1step 3.1∎

Steps 2.1 and 3.1 prove both claimed equalities.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs

Statement

Let T:V→V be an endomorphism of a real vector space, let σ=σcan⁡ be the canonical conjugation of VC, and let λ∈C and e≥1. Then

σ(Gλ(e)(TC))=Gλ‾(e)(TC).

Thus for nonreal λ the generalised eigenspaces of TC for λ and for λ‾ are interchanged by the real-linear involution σ, and they have the same real dimension.

Facts & Assumptions

Given: A real vector space V, an endomorphism T:V→V, a complex scalar λ, and an exponent e≥1.

[L1]

A conjugation is conjugate-linear and an involution (Conjugations and real structures on a complex vector space).

[L2]

The complexification of a real operator commutes with the canonical conjugation, because it comes from a real operator (A complex-linear operator comes from a real operator exactly when it commutes with the chosen conjugation).

[L3]

The generalised eigenspace of exponent e is Gλ(e)(TC)=ker⁡(TC−λI)e (Primary components ker⁡q(T)e and generalised eigenspaces Gλ(e)(T)=ker⁡(T−λI)e).

Proof

technique · direct
1.1L1L2

The operator TC commutes with σ by [L2], and σ is an R-linear involution, hence a bijection, with σ(zw)=z‾ σw by [L1].

2.1step 1.1L1algebra

The powers commute with σ up to conjugation of the scalar: for w∈VC, σ(TCw−λw)=TCσw−λ‾ σw by step 1.1 and [L1]; iterating this e times gives σ(TC−λI)e=(TC−λ‾I)eσ.

3.1step 2.1L3

If w∈ker⁡(TC−λI)e, then (TC−λ‾I)eσw=σ(TC−λI)ew=σ(0)=0, so σw∈Gλ‾(e)(TC) by [L3].

3.2step 2.1L1L3

Conversely, if w′∈Gλ‾(e)(TC), then w:=σw′ satisfies (TC−λI)ew=σ(TC−λ‾I)ew′=0, so w∈Gλ(e)(TC); since σ is an involution, the two inclusions combine to the equality σ(Gλ(e)(TC))=Gλ‾(e)(TC).

4.1step 1.1step 3.2∎

Because σ is real-linear and bijective by step 1.1, the two generalised eigenspaces have the same real dimension; for nonreal λ they form the conjugate pair interchanged by σ.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

A nonreal eigenvector yields an invariant real two-plane and the standard rotation-scaling block

Statement

Let T:V→V be an endomorphism of a real vector space, identify V with the fixed real form of the canonical conjugation on VC, and suppose w=u+iv with u,v∈V is an eigenvector of TC with eigenvalue λ=a+bi, where b≠0. Then u and v are R-linearly independent, span⁡R{u,v} is T-invariant, and with respect to the ordered basis (u,−v) the matrix of T restricted to that plane is

(a−bba).

Moreover σ(w)=u−iv is an eigenvector of TC with eigenvalue λ‾=a−bi.

Facts & Assumptions

Given: A real vector space V, an endomorphism T, and an eigenvector w=u+iv of TC with eigenvalue λ=a+bi, where u,v∈V and b≠0.

[L1]

Every element of VC is uniquely u+iv with u,v in the fixed real form V (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).

[L2]

The canonical conjugation interchanges the generalised eigenspaces of λ and λ‾ (For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs).

Proof

technique · direct
1.1L1givenalgebra

By [L1], the decomposition w=u+iv with u,v∈V is unique. Both u and v are nonzero: if v=0 then w lies in V and TCw=λw forces b=0; symmetrically u=0 would give the same contradiction for the coefficient of i.

2.1step 1.1algebra

Expanding TC(u+iv)=λ(u+iv) gives Tu+iTv=(au−bv)+i(bu+av); comparing the V- and iV-components, which are unique by [L1], yields Tu=au−bv and Tv=bu+av.

2.2step 1.1L2

The conjugate vector is an eigenvector for λ‾: σ(w)=u−iv lies in Gλ‾(1)(TC) by [L2] applied with e=1.

3.1step 1.1step 2.1L1algebra

The vectors u,v are R-linearly independent: if u and v were dependent, then, since both are nonzero, v=αu for a real α, so w=(1+iα)u and dividing the eigen-equation by 1+iα≠0 gives TCu=λu. But TCu=Tu lies in V, while λu=au+biu has nonzero i-component bu, contradicting uniqueness of the components in [L1].

3.2step 2.1algebra

The plane is invariant and the block appears: Tu=au−bv=au+b(−v) and T(−v)=−(bu+av)=−bu+a(−v) by step 2.1, so in the ordered basis (u,−v) the two columns are (ab) and (−ba).

4.1step 2.2step 3.1step 3.2∎

Steps 3.1 and 3.2 prove the independence, invariance and matrix claims, and step 2.2 the conjugate eigenvector claim.

5 · Examples, counterexamples and false statements

None yet.

Sources