Documentation

TauCeti.LinearAlgebra.BilinearForm.Diagonalization

Diagonalization of symmetric bilinear forms in every characteristic #

Over a commutative ring, an orthogonal basis reduces divisibility of all pairings to divisibility of its diagonal values. The hyperbolic plane can therefore have an orthogonal basis only when 2 is a unit. Over a local ring with 2 invertible, a pairing dividing every value can be replaced by a self-pairing with the same property.

Over a field in which 2 is invertible, every symmetric bilinear form on a finite-dimensional space has an orthogonal basis (LinearMap.BilinForm.exists_orthogonal_basis). In characteristic two this fails: a nonzero alternating form is symmetric, and an orthogonal basis for it would make every basis pairing vanish, hence the whole form. This file shows that the alternating forms are the only obstruction, in every characteristic: a symmetric form has an orthogonal basis if and only if it is zero or not alternating (LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_iff).

For a nondegenerate form over a field in which every element is a square, for instance a finite field of characteristic two (isSquare_of_charTwo'), the orthogonal basis can be rescaled: a symmetric form that is not alternating has an orthonormal basis, one in which its matrix is the identity (LinearMap.BilinForm.IsSymm.exists_basis_toMatrix_eq_one). Hence it is equivalent to the standard form Matrix.toBilin' 1, which is itself such a form in every positive dimension (Matrix.isAlt_toBilin'_one_iff in TauCeti.LinearAlgebra.Matrix.BilinearForm), and any two such forms of the same dimension are equivalent. Together with the symplectic normal form of TauCeti.LinearAlgebra.BilinearForm.SymplecticBasis this gives the dichotomy for nondegenerate forms that are alternating or symmetric: a symplectic basis when the form is alternating, an orthonormal basis when it is not (LinearMap.BilinForm.Nondegenerate.exists_basis_toMatrix_eq_J_or_toMatrix_eq_one). Over 𝔽₂, where every form that is alternating is symmetric, this classifies the nondegenerate symmetric bilinear forms, which is the input to the normal forms of one-relator pro-2 groups.

Main results #

References #

source
theorem LinearMap.BilinForm.dvd_apply_of_forall_dvd_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_3} (b : Module.Basis ι R M) {d : R} (hd : ∀ (i j : ι), d ∣ (B (b i)) (b j)) (x y : M) :
d ∣ (B x) y

A common divisor of the Gram entries of a bilinear form in a basis divides every value of the form.

source
theorem LinearMap.BilinForm.iIsOrtho.dvd_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_3} {b : Module.Basis ι R M} (hb : B.iIsOrtho ⇑b) {d : R} (hd : ∀ (i : ι), d ∣ (B (b i)) (b i)) (x y : M) :
d ∣ (B x) y

Along an orthogonal basis, a common divisor of the diagonal values of a bilinear form divides every value of the form.

source
theorem LinearMap.BilinForm.isUnit_two_of_iIsOrtho_toBilin'_hyperbolic {R : Type u_1} [CommRing R] {ι : Type u_3} {b : Module.Basis ι R (Fin 2 → R)} (hb : (Matrix.toBilin' !![0, 1; 1, 0]).iIsOrtho ⇑b) :
IsUnit 2

If the hyperbolic plane, the form with Gram matrix !![0, 1; 1, 0] on R², has an orthogonal basis, then 2 is a unit in R. So over a ring such as ℤ_2 the hyperbolic plane is not diagonalizable.

source
theorem LinearMap.BilinForm.IsSymm.exists_forall_apply_self_dvd_of_forall_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [IsLocalRing R] (hB : B.IsSymm) (h2 : IsUnit 2) {u w : M} (h : ∀ (y z : M), (B u) w ∣ (B y) z) :
∃ (x : M), ∀ (y z : M), (B x) x ∣ (B y) z

Over a local ring in which 2 is a unit, if a value B u w of a symmetric bilinear form divides every value of the form, then so does one of the self-pairings B u u, B w w and B (u + w) (u + w).

source
theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_of_isAlt_imp_eq_zero {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hB : B.IsSymm) (h : B.IsAlt → B = 0) :
∃ (v : Module.Basis (Fin (Module.finrank K V)) K V), B.iIsOrtho ⇑v

A symmetric bilinear form that is zero or not alternating has an orthogonal basis, in every characteristic. Away from characteristic two the hypothesis is automatic for symmetric forms (TauCeti.BilinForm.eq_zero_of_isSymm_of_isAlt), which recovers LinearMap.BilinForm.exists_orthogonal_basis; in characteristic two it excludes exactly the nonzero alternating forms.

source
theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_iff {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hB : B.IsSymm) :
(∃ (v : Module.Basis (Fin (Module.finrank K V)) K V), B.iIsOrtho ⇑v) ↔ B.IsAlt → B = 0

A symmetric bilinear form has an orthogonal basis if and only if it is zero or not alternating. The forward direction is the observation that an orthogonal basis of an alternating form pairs every two basis vectors to zero.

source
theorem LinearMap.BilinForm.IsSymm.exists_basis_toMatrix_eq_one {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hsq : ∀ (a : K), IsSquare a) (hB : B.IsSymm) (hnd : B.Nondegenerate) (h : B.IsAlt → B = 0) :
∃ (v : Module.Basis (Fin (Module.finrank K V)) K V), (toMatrix v) B = 1

A nondegenerate symmetric form that is not alternating has an orthonormal basis, over a field in which every element is a square: rescaling an orthogonal basis by inverse square roots of the self-pairings makes the matrix of the form the identity. The hypothesis on squares holds in every finite field of characteristic two (isSquare_of_charTwo').

source
theorem LinearMap.BilinForm.IsSymm.equivalent_toBilin'_one {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hsq : ∀ (a : K), IsSquare a) (hB : B.IsSymm) (hnd : B.Nondegenerate) (h : B.IsAlt → B = 0) :
B.Equivalent (Matrix.toBilin' 1)

Over a field in which every element is a square, a nondegenerate symmetric form that is not alternating is equivalent to the standard form ∑ i, x i * y i on Fin n → K, for n the dimension.

source
theorem LinearMap.BilinForm.IsSymm.equivalent_of_finrank_eq {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] {V' : Type u_5} [AddCommGroup V'] [Module K V'] [FiniteDimensional K V'] {B' : LinearMap.BilinForm K V'} (hsq : ∀ (a : K), IsSquare a) (hB : B.IsSymm) (hnd : B.Nondegenerate) (h : B.IsAlt → B = 0) (hB' : B'.IsSymm) (hnd' : B'.Nondegenerate) (h' : B'.IsAlt → B' = 0) (hdim : Module.finrank K V = Module.finrank K V') :
B.Equivalent B'

Over a field in which every element is a square, two nondegenerate symmetric forms that are not alternating, on spaces of the same dimension, are equivalent.

source
theorem LinearMap.BilinForm.Nondegenerate.exists_basis_toMatrix_eq_J_or_toMatrix_eq_one {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hsq : ∀ (a : K), IsSquare a) (hnd : B.Nondegenerate) (h : B.IsAlt ∨ B.IsSymm) :
(B.IsAlt ∧ ∃ (m : ℕ) (v : Module.Basis (Fin m ⊕ Fin m) K V), (BilinForm.toMatrix v) B = Matrix.J (Fin m) K) ∨ ¬B.IsAlt ∧ ∃ (v : Module.Basis (Fin (Module.finrank K V)) K V), (BilinForm.toMatrix v) B = 1

The normal-form dichotomy for a nondegenerate form that is alternating or symmetric, over a field in which every element is a square: an alternating form has a symplectic basis, and a symmetric form that is not alternating has an orthonormal basis. In characteristic two every alternating form is symmetric, so the hypothesis is just symmetry there.