Documentation

TauCeti.LinearAlgebra.Matrix.Realify

The realification of a matrix over an RCLike field #

An m × n matrix A over an RCLike field induces an ℝ-linear map, and splitting its entries into real and imaginary parts gives the real (m ⊕ m) × (n ⊕ n) matrix

Matrix.realify A = !![Re A, -Im A; Im A, Re A],

the realification of A. It is additive and multiplicative and turns the conjugate transpose into the transpose, so it carries Hermitian matrices to symmetric ones and *-congruence to congruence. This is what lets real quadratic-form theory be applied to Hermitian forms.

Main definitions #

Main results #

source
def TauCeti.realifyReflection (ι : Type u_5) [DecidableEq ι] :
Matrix (ι ⊕ ι) (ι ⊕ ι) ℝ

The reflection of ℝ^ι ⊕ ℝ^ι negating the second summand, which realises conjugation as a congruence of realifications.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.realifyReflection_transpose {ι : Type u_4} [DecidableEq ι] :
    (realifyReflection ι).transpose = realifyReflection ι
    source
    @[simp]
    theorem TauCeti.realifyReflection_mul_self {ι : Type u_4} [Fintype ι] [DecidableEq ι] :
    realifyReflection ι * realifyReflection ι = 1
    source
    theorem TauCeti.isUnit_det_realifyReflection {ι : Type u_4} [Fintype ι] [DecidableEq ι] :
    IsUnit (realifyReflection ι).det
    source
    def Matrix.realify {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) :
    Matrix (m ⊕ m) (n ⊕ n) ℝ

    The realification of a matrix over an RCLike field, obtained by splitting its entries into real and imaginary parts.

    Equations
    Instances For
      source
      @[simp]
      theorem Matrix.realify_apply_inl_inl {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) (i : m) (j : n) :
      A.realify (Sum.inl i) (Sum.inl j) = RCLike.re (A i j)
      source
      @[simp]
      theorem Matrix.realify_apply_inl_inr {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) (i : m) (j : n) :
      A.realify (Sum.inl i) (Sum.inr j) = -RCLike.im (A i j)
      source
      @[simp]
      theorem Matrix.realify_apply_inr_inl {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) (i : m) (j : n) :
      A.realify (Sum.inr i) (Sum.inl j) = RCLike.im (A i j)
      source
      @[simp]
      theorem Matrix.realify_apply_inr_inr {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) (i : m) (j : n) :
      A.realify (Sum.inr i) (Sum.inr j) = RCLike.re (A i j)
      source
      @[simp]
      theorem Matrix.realify_zero {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] :
      realify 0 = 0
      source
      @[simp]
      theorem Matrix.realify_add {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A B : Matrix m n 𝕜) :
      (A + B).realify = A.realify + B.realify

      Realification preserves addition.

      source
      @[simp]
      theorem Matrix.realify_neg {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) :
      (-A).realify = -A.realify
      source
      @[simp]
      theorem Matrix.realify_smul {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (r : ℝ) (A : Matrix m n 𝕜) :
      (r • A).realify = r • A.realify

      Realification commutes with real scalar multiplication.

      source
      @[simp]
      theorem Matrix.realify_map_ofReal {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (M : Matrix m n ℝ) :
      (M.map ⇑(algebraMap ℝ 𝕜)).realify = fromBlocks M 0 0 M

      A matrix with real entries realifies to two diagonal copies of itself.

      source
      @[simp]
      theorem Matrix.realify_one {ι : Type u_4} {𝕜 : Type u_5} [RCLike 𝕜] [DecidableEq ι] :
      realify 1 = 1

      Realification preserves the identity matrix.

      source
      @[simp]
      theorem Matrix.realify_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] [Fintype n] (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) :
      (A * B).realify = A.realify * B.realify

      Realification preserves matrix multiplication.

      source
      @[simp]
      theorem Matrix.realify_conjTranspose {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : Matrix m n 𝕜) :
      A.conjTranspose.realify = A.realify.transpose

      Realification turns the conjugate transpose into the transpose.

      source
      theorem Matrix.IsHermitian.isSymm_realify {ι : Type u_4} {𝕜 : Type u_5} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
      A.realify.IsSymm

      Realification carries Hermitian matrices to symmetric ones.

      source
      theorem Matrix.isUnit_det_realify {ι : Type u_4} {𝕜 : Type u_5} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} (h : IsUnit A.det) :
      IsUnit A.realify.det

      Realification preserves invertibility.

      source
      theorem Matrix.realify_map_starRingEnd {ι : Type u_4} {𝕜 : Type u_5} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι 𝕜) :
      (A.map ⇑(starRingEnd 𝕜)).realify = TauCeti.realifyReflection ι * A.realify * (TauCeti.realifyReflection ι).transpose

      Entrywise conjugation becomes congruence by the reflection negating the imaginary coordinates.