The standard sesquilinear form with a specified twist

For a ring endomorphism σ, the form sesquilinearForm σ is linear in its first argument and σ-semilinear in its second: h(x,y) = ∑ i, x i * σ (y i). It is nondegenerate when σ is injective, and for an automorphism σ it identifies the second coordinate space semilinearly with the dual of the first. When σ is involutive, the form has Hermitian symmetry. This orientation is useful for Hermitian duals of codes over finite fields.

This identification with the dual gives a nondegenerate pairing for studying orthogonality in finite coordinate spaces.

The API is in RingHom: use σ.sesquilinearForm, or RingHom.sesquilinearForm σ. Results that need an automorphism are in RingEquiv.

For a module with a finite basis b, Mathlib's Matrix.toLinearMapₛₗ₂ σ b b 1 is the sesquilinear form, σ-semilinear in its first argument, for which b is orthonormal. In coordinates it is ∑ i, σ (x i) * y i (Matrix.toLinearMapₛₗ₂_one_apply). For complex conjugation, or any star ring, it is Hermitian (Matrix.star_toLinearMapₛₗ₂_one_apply), and over a star-ordered ring without zero divisors it is positive definite (Matrix.toLinearMapₛₗ₂_one_self_nonneg, Matrix.toLinearMapₛₗ₂_one_self_eq_zero_iff). This is the Hermitian metric making a chosen basis orthonormal, for instance the increasing wedge basis of an exterior algebra.

More generally, for a ring endomorphism σ and a Gram matrix Q, write B(x, y) = σ(x)ᵀ Q y for the coordinate form (σ ∘ x) ⬝ᵥ (Q *ᵥ y). A matrix g with σ(g)ᵀ Q g = Q preserves it (Matrix.comp_mulVec_dotProduct_mulVec_mulVec), and if σ is an involution and σ(Q)ᵀ = ε Q, it is ε-Hermitian, σ(B(x, y)) = ε B(y, x) (Matrix.apply_comp_dotProduct_mulVec). With ε * ε = 1, this gives B(y, x) = ε σ(B(x, y)) (Matrix.comp_dotProduct_mulVec_swap) and a formula for B(u + c x, u + c x) when x is isotropic (Matrix.comp_add_smul_dotProduct_mulVec_add_smul).

Over a field, if the trace t ↦ t + ε σ(t) is onto the elements s with σ(s) = ε s, a vector u with B(u, x) ≠ 0 corrects to an isotropic u + c x (Matrix.exists_comp_add_smul_dotProduct_mulVec_add_smul_eq_zero). For invertible Q, any two nonzero vectors pair nontrivially with a common vector (Matrix.exists_comp_dotProduct_mulVec_ne_zero_pair). If moreover the trace has a nonzero kernel element and some nonzero vector is isotropic, a matrix scaling every isotropic vector is scalar (Matrix.exists_eq_scalar_of_forall_mulVec_eq_smul).

noncomputable def RingHom.sesquilinearForm {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R →+* R) : (ι → R) →ₛₗ[id R] (ι → R) →ₛₗ[σ] R

The standard sesquilinear form, linear in the first argument and twisted by σ in the second. It is Hermitian when σ is involutive.

@[simp]

theorem RingHom.sesquilinearForm_apply {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R →+* R) (x y : ι → R) : (σ.sesquilinearForm x) y = ∑ i : ι, x i * σ (y i)

The standard sesquilinear form evaluates as the coordinate sum ∑ i, x i * σ (y i).

theorem RingHom.sesquilinearForm_swap {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R →+* R) (hσ : Function.Involutive ⇑σ) (x y : ι → R) : (σ.sesquilinearForm y) x = σ ((σ.sesquilinearForm x) y)

For an involutive endomorphism, swapping the arguments conjugates the value.

theorem RingHom.nondegenerate_sesquilinearForm {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R →+* R) (hσ : Function.Injective ⇑σ) : σ.sesquilinearForm.Nondegenerate

The standard sesquilinear form is nondegenerate over any commutative semiring when the twist is injective.

theorem RingEquiv.sesquilinearForm_symm_swap {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R ≃+* R) (x y : ι → R) : ((↑σ.symm).sesquilinearForm y) x = σ.symm (((↑σ).sesquilinearForm x) y)

Swapping the arguments and inverting the automorphism applies the inverse automorphism to the value of the standard sesquilinear form.

theorem RingEquiv.sesquilinearForm_flip_bijective {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (σ : R ≃+* R) : Function.Bijective ⇑(↑σ).sesquilinearForm.flip

The second argument of the standard sesquilinear form identifies the coordinate space with its dual.

theorem Matrix.comp_mulVec_dotProduct_mulVec_mulVec {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] {Q : Matrix n n R} {σ : R →+* R} {g : Matrix n n R} (hg : (g.map ⇑σ).transpose * Q * g = Q) (x y : n → R) : ⇑σ ∘ g.mulVec x ⬝ᵥ Q.mulVec (g.mulVec y) = ⇑σ ∘ x ⬝ᵥ Q.mulVec y

A matrix preserving the form preserves its values. For the σ-sesquilinear form B(x, y) = σ(x)ᵀ Q y of Gram matrix Q, if σ(g)ᵀ Q g = Q, then B(g x, g y) = B(x, y).

theorem Matrix.apply_comp_dotProduct_mulVec {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] {Q : Matrix n n R} {σ : R →+* R} (hσ : Function.Involutive ⇑σ) {ε : R} (hQ : (Q.map ⇑σ).transpose = ε • Q) (x y : n → R) : σ (⇑σ ∘ x ⬝ᵥ Q.mulVec y) = ε * ⇑σ ∘ y ⬝ᵥ Q.mulVec x

An ε-Hermitian form. For the σ-sesquilinear form B(x, y) = σ(x)ᵀ Q y of Gram matrix Q, if σ is an involution and σ(Q)ᵀ = ε Q, then σ(B(x, y)) = ε B(y, x).

theorem Matrix.comp_add_dotProduct_mulVec {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] {Q : Matrix n n R} {σ : R →+* R} (u v w : n → R) : ⇑σ ∘ (u + v) ⬝ᵥ Q.mulVec w = ⇑σ ∘ u ⬝ᵥ Q.mulVec w + ⇑σ ∘ v ⬝ᵥ Q.mulVec w

The form is additive in its first argument.

theorem Matrix.comp_dotProduct_mulVec_swap {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] {Q : Matrix n n R} {σ : R →+* R} (hσ : Function.Involutive ⇑σ) {ε : R} (hQ : (Q.map ⇑σ).transpose = ε • Q) (hε : ε * ε = 1) (x y : n → R) : ⇑σ ∘ y ⬝ᵥ Q.mulVec x = ε * σ (⇑σ ∘ x ⬝ᵥ Q.mulVec y)

With ε * ε = 1, the form is ε-Hermitian in the form B(y, x) = ε σ(B(x, y)).

theorem Matrix.comp_add_smul_dotProduct_mulVec_add_smul {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] {Q : Matrix n n R} {σ : R →+* R} (hσ : Function.Involutive ⇑σ) {ε : R} (hQ : (Q.map ⇑σ).transpose = ε • Q) (hε : ε * ε = 1) {x : n → R} (hx : ⇑σ ∘ x ⬝ᵥ Q.mulVec x = 0) (u : n → R) (c : R) : ⇑σ ∘ (u + c • x) ⬝ᵥ Q.mulVec (u + c • x) = ⇑σ ∘ u ⬝ᵥ Q.mulVec u + (c * ⇑σ ∘ u ⬝ᵥ Q.mulVec x + ε * σ (c * ⇑σ ∘ u ⬝ᵥ Q.mulVec x))

The value of the form at u + c • x for an isotropic x.

theorem Matrix.mul_self_eq_one_of_trace {n : Type u_1} {K : Type u_2} [Field K] {Q : Matrix n n K} {σ : K →+* K} {ε : K} (hσ : Function.Involutive ⇑σ) (hQ : (Q.map ⇑σ).transpose = ε • Q) (htr : ∀ (s : K), σ s = ε * s → ∃ (t : K), t + ε * σ t = s) (hQ0 : Q ≠ 0) : ε * ε = 1

If σ is an involution, Q is a nonzero ε-Hermitian matrix, and the trace t ↦ t + ε σ(t) is onto the elements s with σ(s) = ε s, then ε * ε = 1.

theorem Matrix.exists_comp_add_smul_dotProduct_mulVec_add_smul_eq_zero {n : Type u_1} {K : Type u_2} [Fintype n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {ε : K} (hσ : Function.Involutive ⇑σ) (hQ : (Q.map ⇑σ).transpose = ε • Q) (htr : ∀ (s : K), σ s = ε * s → ∃ (t : K), t + ε * σ t = s) {x : n → K} (hx : ⇑σ ∘ x ⬝ᵥ Q.mulVec x = 0) {u : n → K} (hux : ⇑σ ∘ u ⬝ᵥ Q.mulVec x ≠ 0) : ∃ (c : K), ⇑σ ∘ (u + c • x) ⬝ᵥ Q.mulVec (u + c • x) = 0

Correcting a vector to an isotropic one. If the trace t ↦ t + ε σ(t) is onto the elements s with σ(s) = ε s, then for isotropic x and B(u, x) ≠ 0 some u + c • x is isotropic.

theorem Matrix.exists_comp_dotProduct_mulVec_ne_zero_pair {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} (hdet : Q.det ≠ 0) {x y : n → K} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (u : n → K), ⇑σ ∘ u ⬝ᵥ Q.mulVec x ≠ 0 ∧ ⇑σ ∘ u ⬝ᵥ Q.mulVec y ≠ 0

For an invertible Q, two nonzero vectors pair nontrivially with a common vector.

theorem Matrix.exists_eq_scalar_of_forall_mulVec_eq_smul {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {ε : K} (hσ : Function.Involutive ⇑σ) (hQ : (Q.map ⇑σ).transpose = ε • Q) (hdet : Q.det ≠ 0) (htr : ∀ (s : K), σ s = ε * s → ∃ (t : K), t + ε * σ t = s) (hadm : ∃ (d : K), d ≠ 0 ∧ d + ε * σ d = 0) {x₀ : n → K} (hx₀ : x₀ ≠ 0) (hx₀iso : ⇑σ ∘ x₀ ⬝ᵥ Q.mulVec x₀ = 0) (M : Matrix n n K) (hM : ∀ (v : n → K), ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0 → ∃ (c : K), M.mulVec v = c • v) : ∃ (c : K), M = (scalar n) c

A matrix scaling every isotropic vector is scalar. Let σ be an involution and Q an invertible ε-Hermitian matrix, and suppose that the trace t ↦ t + ε σ(t) is onto the elements s with σ(s) = ε s and has a nonzero kernel element (surjectivity of the trace already forces ε * ε = 1, Matrix.mul_self_eq_one_of_trace). If some nonzero vector is isotropic and M maps every isotropic vector to a multiple of itself, then M is a scalar matrix.

theorem Matrix.toLinearMapₛₗ₂_one_apply {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (σ : R →+* R) (x y : M) : (((toLinearMapₛₗ₂ σ b b) 1) x) y = ∑ i : n, σ ((b.repr x) i) * (b.repr y) i

The sesquilinear form of the identity matrix in coordinates: for a basis b, toLinearMapₛₗ₂ σ b b 1 x y = ∑ i, σ (x i) * y i, the form for which b is orthonormal.

theorem Matrix.toLinearMapₛₗ₂_one_basis_eq_coord {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (σ : R →+* R) (i : n) : ((toLinearMapₛₗ₂ σ b b) 1) (b i) = b.coord i

For the form making a basis orthonormal, the functional attached to a basis vector is its coordinate functional.

theorem Matrix.star_toLinearMapₛₗ₂_one_apply {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] (b : Module.Basis n R M) [StarRing R] (x y : M) : star ((((toLinearMapₛₗ₂ (starRingEnd R) b b) 1) x) y) = (((toLinearMapₛₗ₂ (starRingEnd R) b b) 1) y) x

The orthonormal-basis form is Hermitian: for complex conjugation, or the star of any star ring, swapping the arguments of toLinearMapₛₗ₂ (starRingEnd R) b b 1 conjugates its value.

theorem Matrix.toLinearMapₛₗ₂_one_self_nonneg {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] (b : Module.Basis n R M) [StarRing R] [PartialOrder R] [StarOrderedRing R] (x : M) : 0 ≤ (((toLinearMapₛₗ₂ (starRingEnd R) b b) 1) x) x

The orthonormal-basis form is positive semidefinite over a star-ordered ring.

theorem Matrix.toLinearMapₛₗ₂_one_self_eq_zero_iff {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] (b : Module.Basis n R M) [StarRing R] [PartialOrder R] [StarOrderedRing R] [NoZeroDivisors R] {x : M} : (((toLinearMapₛₗ₂ (starRingEnd R) b b) 1) x) x = 0 ↔ x = 0

The orthonormal-basis form is definite over a star-ordered ring without zero divisors: toLinearMapₛₗ₂ (starRingEnd R) b b 1 x x = 0 only for x = 0.