TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

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 $W_{R}$ , and the map

$θ : C \otimes_{R} W^{σ} ⟶ W, θ (z \otimes 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^{'}$ , $σ (z w) = \overline{z} σ w$ , $σ σ w = w$ (Conjugations and real structures on a complex vector space).

[L2]

The fixed real form is $W^{σ} = {w \in W : σ w = w} \subseteq W_{R}$ (The fixed real form of a conjugation).

[L3]

A real-linear map $f : W^{σ} \to 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 $\overline{z + w} = \overline{z} + \overline{w}$ , $\overline{z w} = \overline{z} \overline{w}$ and $\overline{\overline{z}} = z$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L5]

The complexification of a real space carries the scalar action $z^{'} \cdot (z \otimes v) = (z^{'} z) \otimes v$ (Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding).

Proof

technique · direct

1.1

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 $σ (r w) = \overline{r} σ w = r w$ for $r \in R$ .

L1L2

1.2

Every element of $C \otimes_{R} W^{σ}$ has the form $1 \otimes A + i \otimes B$ with $A, B \in W^{σ}$ : a general finite sum is $\sum_{j} z_{j} \otimes w_{j} = \sum_{j} (a_{j} + i b_{j}) \otimes w_{j} = \sum_{j} (a_{j} + i b_{j}) \cdot (1 \otimes w_{j}) = 1 \otimes (\sum_{j} a_{j} w_{j}) + i \otimes (\sum_{j} b_{j} w_{j})$ by the scalar action of [L5], and the two coefficient sums lie in the real subspace $W^{σ}$ .

L5L1algebra

2.1

By [L3], the real-linear inclusion $W^{σ} ↪ W$ extends uniquely to a complex-linear map $θ : C \otimes_{R} W^{σ} \to W$ with $θ (z \otimes w) = z w$ .

step 1.1L3

3.1

Surjectivity: for $v \in W$ set $A = (v + σ v) / 2$ and $B = (v - σ v) / (2 i)$ . By [L1] and [L4], $σ A = (v + σ v) / 2 = A$ , and $σ B = (σ v - v) / (2 \overline{i}) = (v - σ v) / (2 i) = B$ because $\overline{i} = - i$ ; hence $A, B \in W^{σ}$ by [L2] and $θ (1 \otimes A + i \otimes B) = A + i B = v$ .

step 2.1L1L2L4algebra

3.2

Injectivity: for $A, B \in W^{σ}$ one has $θ (1 \otimes A + i \otimes B) = A + i B$ by step 2.1. If $A + i B = 0$ , applying $σ$ and using [L1] gives $A - i B = 0$ ; subtracting the two identities gives $2 i B = 0$ , hence $B = 0$ and then $A = 0$ , so the tensor $1 \otimes A + i \otimes B$ is zero.

step 1.2step 2.1L1algebra

4.1

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

step 2.1step 3.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

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