Complexification $V_\mathbf{C}$ (Ex 1.B.8)
- Complexification $V_\mathbf{C}$ (Ex 1.B.8) #Card
- 実ベクトル空間 $V$ から複素ベクトル空間を作る複素化 $V_\mathbf{C}$ の構成は？
構成. $V_\mathbf{C}=V\times V$、要素を $u+iv$ と書く。
- 加法: $(u_1+iv_1)+(u_2+iv_2)=(u_1+u_2)+i(v_1+v_2)$
- 複素スカラー倍: $(a+bi)(u+iv)=(au-bv)+i(av+bu)$
これで $V_\mathbf{C}$ は複素ベクトル空間になる（検証の実質はスカラー乗法の結合律で、複素数の積 $(ac-bd,\ ad+bc)$ がそのまま現れる）。$\mathbf{R}^n\leadsto\mathbf{C}^n$ の一般化。
射程: 実→複素の係数拡大。実ベクトル空間の文脈で複素スペクトル定理・固有値論を使うための標準的な布石（LADR 第8章で再登場）。
Mathlib の Complexification は TensorProduct ℝ ℂ V ベース。Module.complexification 周辺。