Documentation

TauCeti.LinearAlgebra.BilinearForm.Complexification

The sesquilinear complexification of a real bilinear form #

A real bilinear form B on V has two complex extensions to the complexification ℂ ⊗[ℝ] V. Mathlib's LinearMap.BilinForm.baseChange is the complex-bilinear one, B_ℂ. Composing it in the first argument with the conjugation TauCeti.tmulConj of the complexification gives the sesquilinear one,

h (x, y) = B_ℂ (conj x, y), so h (z ⊗ v, w ⊗ u) = conj z * w * B (v, u),

which is conjugate-linear in the first argument and linear in the second, Mathlib's convention for sesquilinear forms. When B is symmetric, h is Hermitian; when B is moreover positive definite, so is h. This is the positive Hermitian form that a Euclidean metric g induces on ℂ ⊗[ℝ] V; it is a different form from the complex-bilinear g_ℂ, to which it is related by h (conj x, y) = g_ℂ (x, y). Real-linear maps preserving B complexify to maps preserving h.

Main definitions #

Main results #

The bilinear complexification and conjugation #

source
@[simp]
theorem LinearMap.BilinForm.baseChange_tmulConj_tmulConj {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) (x y : TensorProduct ℝ ℂ V) :
((BilinForm.baseChange ℂ B) ((TauCeti.tmulConj V) x)) ((TauCeti.tmulConj V) y) = (starRingEnd ℂ) (((BilinForm.baseChange ℂ B) x) y)

Conjugating both arguments of the complex-bilinear extension of a real form conjugates its value.

The sesquilinear complexification #

source
noncomputable def LinearMap.BilinForm.sesqComplexification {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) :
TensorProduct ℝ ℂ V →ₗ⋆[ℂ] TensorProduct ℝ ℂ V →ₗ[ℂ] ℂ

The sesquilinear complexification of a real bilinear form B: the form h (x, y) = B_ℂ (conj x, y) on ℂ ⊗[ℝ] V, conjugate-linear in the first argument and linear in the second, with h (z ⊗ v, w ⊗ u) = conj z * w * B (v, u) (LinearMap.BilinForm.sesqComplexification_tmul_tmul). For a Euclidean metric it is the induced positive Hermitian form on the complexification.

Instances For
    source
    theorem LinearMap.BilinForm.sesqComplexification_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) (x y : TensorProduct ℝ ℂ V) :
    (B.sesqComplexification x) y = ((BilinForm.baseChange ℂ B) ((TauCeti.tmulConj V) x)) y
    source
    @[simp]
    theorem LinearMap.BilinForm.sesqComplexification_tmul_tmul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) (z w : ℂ) (v u : V) :
    (B.sesqComplexification (z ⊗ₜ[ℝ] v)) (w ⊗ₜ[ℝ] u) = (starRingEnd ℂ) z * w * ↑((B v) u)

    The sesquilinear complexification on pure tensors.

    source
    @[simp]
    theorem LinearMap.BilinForm.sesqComplexification_tmulConj_left {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) (x y : TensorProduct ℝ ℂ V) :
    (B.sesqComplexification ((TauCeti.tmulConj V) x)) y = ((BilinForm.baseChange ℂ B) x) y

    The sesquilinear complexification evaluated at a conjugate is the complex-bilinear extension: h (conj x, y) = B_ℂ (x, y).

    source
    theorem LinearMap.BilinForm.sesqComplexification_tmulConj_tmulConj {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) (x y : TensorProduct ℝ ℂ V) :
    (B.sesqComplexification ((TauCeti.tmulConj V) x)) ((TauCeti.tmulConj V) y) = (starRingEnd ℂ) ((B.sesqComplexification x) y)

    Conjugating both arguments of the sesquilinear complexification conjugates its value.

    source
    theorem LinearMap.BilinForm.sesqComplexification_baseChange_baseChange {V : Type u_1} {V' : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup V'] [Module ℝ V'] (B : LinearMap.BilinForm ℝ V) {B' : LinearMap.BilinForm ℝ V'} {f : V →ₗ[ℝ] V'} (hf : ∀ (v w : V), (B' (f v)) (f w) = (B v) w) (x y : TensorProduct ℝ ℂ V) :
    (B'.sesqComplexification ((baseChange ℂ f) x)) ((baseChange ℂ f) y) = (B.sesqComplexification x) y

    Complexified maps preserving a real bilinear form preserve its sesquilinear complexification: if f carries B to B', then f.baseChange ℂ carries the induced form of B to that of B'.

    source
    theorem LinearMap.BilinForm.sesqComplexification_eq_zero_of_mem_eigenspace {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) {f : V →ₗ[ℝ] V} (hf : ∀ (v w : V), (B (f v)) (f w) = (B v) w) {z w : ℂ} (hzw : (starRingEnd ℂ) z * w ≠ 1) {x y : TensorProduct ℝ ℂ V} (hx : x ∈ Module.End.eigenspace (baseChange ℂ f) z) (hy : y ∈ Module.End.eigenspace (baseChange ℂ f) w) :
    (B.sesqComplexification x) y = 0

    Eigenspaces of a complexified map preserving a real bilinear form are orthogonal for its sesquilinear complexification unless their eigenvalues satisfy conj z * w = 1: the complexification of f preserves h, and scales h (x, y) by conj z * w on eigenvectors.

    source
    theorem LinearMap.BilinForm.sesqComplexification_baseChange_left_of_skewAdjoint {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) {f : V →ₗ[ℝ] V} (hf : ∀ (v w : V), (B (f v)) w = -(B v) (f w)) (x y : TensorProduct ℝ ℂ V) :
    (B.sesqComplexification ((baseChange ℂ f) x)) y = -(B.sesqComplexification x) ((baseChange ℂ f) y)

    A real skew-adjoint endomorphism remains skew-adjoint for the sesquilinear complexification. Neither symmetry nor nondegeneracy of the form is required.

    source
    theorem LinearMap.BilinForm.sesqComplexification_eq_zero_of_mem_eigenspace_of_skewAdjoint {V : Type u_1} [AddCommGroup V] [Module ℝ V] (B : LinearMap.BilinForm ℝ V) {f : V →ₗ[ℝ] V} (hf : ∀ (v w : V), (B (f v)) w = -(B v) (f w)) {z w : ℂ} (hzw : (starRingEnd ℂ) z + w ≠ 0) {x y : TensorProduct ℝ ℂ V} (hx : x ∈ Module.End.eigenspace (baseChange ℂ f) z) (hy : y ∈ Module.End.eigenspace (baseChange ℂ f) w) :
    (B.sesqComplexification x) y = 0

    Eigenvectors of a complexified skew-adjoint endomorphism are orthogonal unless their eigenvalues satisfy conj z + w = 0.

    Hermitian symmetry and positivity #

    source
    theorem LinearMap.BilinForm.IsSymm.sesqComplexification {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsSymm) :
    B.sesqComplexification.IsSymm

    The sesquilinear complexification of a symmetric form is Hermitian.

    source
    theorem LinearMap.BilinForm.sesqComplexification_one_tmul_add_I_tmul_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsSymm) (a b : V) :
    (B.sesqComplexification (1 ⊗ₜ[ℝ] a + Complex.I ⊗ₜ[ℝ] b)) (1 ⊗ₜ[ℝ] a + Complex.I ⊗ₜ[ℝ] b) = ↑((B a) a + (B b) b)

    The diagonal of the sesquilinear complexification of a symmetric form: writing a vector of the complexification as a + i b with a, b real, h (a + i b, a + i b) is the real number B (a, a) + B (b, b).

    source
    theorem LinearMap.BilinForm.IsPosSemidef.sesqComplexification {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsPosSemidef) :
    B.sesqComplexification.IsPosSemidef

    The sesquilinear complexification of a positive semidefinite form is positive semidefinite.

    source
    theorem LinearMap.BilinForm.sesqComplexification_self_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsSymm) (hpos : (BilinMap.toQuadraticMap B).PosDef) {x : TensorProduct ℝ ℂ V} (hx : x ≠ 0) :
    0 < (B.sesqComplexification x) x

    The sesquilinear complexification of a positive definite symmetric form is positive definite.