Documentation

TauCeti.LinearAlgebra.QuadraticForm.Witt.TotallyIsotropic

Totally isotropic subspaces and the Witt index #

A subspace W of a quadratic space (V, Q) is totally isotropic (QuadraticMap.IsTotallyIsotropic) when Q vanishes on every vector of W. Over a field in which 2 is invertible, every maximal totally isotropic subspace of a regular finite-dimensional quadratic space has dimension equal to the Witt index of Q (Lam I.4.4). The Witt index, defined by TauCeti.RegularFormClass.wittIndex as the number of hyperbolic planes in the Witt decomposition Q ≅ m × ℍ ⊥ Q_a, is therefore intrinsic to the quadratic space: it is the common dimension of its maximal totally isotropic subspaces, and the largest dimension of a totally isotropic subspace.

Main results #

Implementation notes #

The comparison goes by induction on the dimension. A nonzero vector w of a maximal totally isotropic subspace W has an isotropic partner f with polar Q w f = 1. The span of w and f is a hyperbolic plane, its orthogonal complement U has Witt index one less, and W ∩ U is a maximal totally isotropic subspace of U of dimension one less.

References #

Splitting a hyperbolic pair off a totally isotropic subspace #

Throughout, w ∈ W lies in a totally isotropic subspace W and f satisfies polar Q w f = 1. Write U for the orthogonal complement of the span of w and f. Then W is the direct sum of the line through w and W ∩ U, and W ∩ U is maximal in U when W is maximal in V.

source
theorem QuadraticForm.finrank_eq_wittIndex_of_maximal {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {W : Submodule K V} (hW : Maximal (QuadraticMap.IsTotallyIsotropic Q) W) :
Module.finrank K ↥W = (TauCeti.formClass Q hQ).wittIndex

Lam I.4.4. Every maximal totally isotropic subspace of a regular finite-dimensional quadratic space has dimension the Witt index of the form.

source
theorem QuadraticMap.IsTotallyIsotropic.exists_le_finrank_eq_wittIndex {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W : Submodule K V} (hQ : Nondegenerate) (hW : IsTotallyIsotropic Q W) :
∃ (W' : Submodule K V), W ≤ W' ∧ IsTotallyIsotropic Q W' ∧ Module.finrank K ↥W' = (TauCeti.formClass Q hQ).wittIndex

Every totally isotropic subspace of a regular finite-dimensional quadratic space lies in a totally isotropic subspace whose dimension is the Witt index.

source
theorem QuadraticMap.IsTotallyIsotropic.finrank_le_wittIndex {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W : Submodule K V} (hQ : Nondegenerate) (hW : IsTotallyIsotropic Q W) :
Module.finrank K ↥W ≤ (TauCeti.formClass Q hQ).wittIndex

Every totally isotropic subspace of a regular finite-dimensional quadratic space has dimension at most the Witt index.

source
theorem QuadraticForm.maximal_isTotallyIsotropic_iff {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {W : Submodule K V} :
Maximal (QuadraticMap.IsTotallyIsotropic Q) W ↔ QuadraticMap.IsTotallyIsotropic Q W ∧ Module.finrank K ↥W = (TauCeti.formClass Q hQ).wittIndex

A totally isotropic subspace of a regular finite-dimensional quadratic space is maximal exactly when its dimension is the Witt index: the maximal totally isotropic subspaces are those of largest dimension.