Complexification of a real vector space (source code)

= Complexification of a real vector space
{title2=$V_\mathbb C=V\otimes_\mathbb R\mathbb C$}

The complexification of a real <vector space> $V$ allows complex scalar coefficients while preserving its real linear relations. It can be constructed as the <tensor product> $V\otimes_\mathbb R\mathbb C$, or as formal sums $u+iv$ with $u,v\in V$. A real basis of $V$ becomes a complex basis of $V_\mathbb C$, so its complex dimension equals the original real dimension. Every real <linear map> extends uniquely by complex linearity. In particular a <real representation> extends by viewing its real matrices as complex matrices. Complexifying the <realification of a complex representation> produces the original complex representation together with its complex conjugate; the coordinate change $(u,v)\mapsto(u+iv,u-iv)$ exhibits the two blocks.