English
The matrix giving the standard-basis representation of the image under the mixed embedding is constructed by a block-diagonal pattern with a 2×2 fixed conjugation block, up to a relabeling.
Русский
Матрица, задающая представление изображения в стандартной базисной системе для смешанного вложения, строится как блочно-диагональная с фиксированным блоком сопряжения 2×2 и последующей переклассификацией.
LaTeX
$$$ \text{matrixToStdBasis} : \text{Matrix} (index K) (index K) \mathbb{C} = \text{fromBlocks}(\text{diagonal}(\lambda _\, , 1)) \;|\; \text{blockDiagonal} (2^{{-1}}) \cdot ?? $$$
Lean4
/-- The matrix that gives the representation on `stdBasis` of the image by `commMap` of an
element `x` of `(K →+* ℂ) → ℂ` fixed by the map `x_φ ↦ conj x_(conjugate φ)`,
see `stdBasis_repr_eq_matrixToStdBasis_mul`. -/
def matrixToStdBasis : Matrix (index K) (index K) ℂ :=
fromBlocks (diagonal fun _ => 1) 0 0 <|
reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal (fun _ => (2 : ℂ)⁻¹ • !![1, 1; -I, I]))
