Non-singular quadratic forms over fields: EKM Lemma 7.16 and GPR Exercise 11.37

Over a field, the base-change-stable regularity condition QuadraticForm.IsGPRNonsingular admits a finite, checkable characterisation: Q is non-singular iff its radical vanishes and the radical of its polar form is at most a line. That is EKM Lemma 7.16, and GPR Exercise 11.37 with one extra rung. This file proves both, and the part of GPR Exc. 11.37's Remark (1) that describes what the two cases look like.

Relation to mathlib

Both mathlib notions from Mathlib/LinearAlgebra/QuadraticForm/Radical.lean are used directly; this development defines no competing radical or non-degeneracy predicate.

• QuadraticMap.radical — the submodule of vectors on which both Q and its polar form vanish — is the radical throughout, including in QuadraticForm/Regularity.lean, where the whole regularity ladder (IsGPRNondegenerate, IsGPRNonsingular, IsEKMNondegenerate) is phrased as radical … = ⊥.
• QuadraticMap.Nondegenerate is EKM's condition (3), taken as mathlib's definition. Our QuadraticForm.IsEKMNondegenerate formalizes EKM's condition (1) instead, since that is the one that reads verbatim as a base-change statement, and IsGPRNonsingular is its ring-level generalisation, which mathlib has no name for. EKM 7.16 is exactly the assertion that condition (1) and mathlib's predicate agree; that is QuadraticForm.isEKMNondegenerate_iff_nondegenerate below.

⚠ Do not read mathlib's QuadraticMap.Nondegenerate as GPR's "non-degenerate": it is strictly stronger, and over a field it is GPR's non-singular rung. GPR's "non-degenerate" is the bare radical Q = ⊥, i.e. QuadraticForm.IsGPRNondegenerate.

Main results

• QuadraticForm.finrank_le_one_of_anisotropic_of_isAlgClosed : over an algebraically closed field an anisotropic quadratic form has dimension at most 1. Proved in every characteristic by finding a root of Q(e) t² + b(e, f) t + Q(f), so it applies in the characteristic-2 case that mathlib's QuadraticForm/AlgClosed.lean (which assumes Invertible (2 : K)) does not cover.
• QuadraticForm.finrank_ker_polarBilin_baseChangeOfProjective : the radical of the polar form commutes with base change, hence has the same dimension. Flatness of L over F, via mathlib's LinearMap.tensorKerEquiv.
• QuadraticForm.isGPRNonsingular_iff_nondegenerate, QuadraticForm.isEKMNondegenerate_iff_nondegenerate : EKM Lemma 7.16, as the equivalence of conditions (1) and (3), and its restatement for IsEKMNondegenerate.
• QuadraticForm.isGPRNonsingular_tfae : GPR Exercise 11.37, all four conditions.
• QuadraticForm.isGPRNonsingular_of_isAlgClosed : GPR Exc. 11.37 (iii) ⇒ (i) for an arbitrary algebraically closed K, which is what makes the "for some K" reading of (iii) legitimate.
• QuadraticForm.isGPRRegular_xor_finrank_ker_polarBilin_eq_one, QuadraticForm.ringChar_eq_two_of_finrank_ker_polarBilin_eq_one, QuadraticForm.exists_isometryEquiv_rankOne_prod : GPR Exc. 11.37, Remark (1) — see below.

GPR Exc. 11.37, Remark (1), and what is missing

Remark (1) says that for finite-dimensional V, condition (ii) holds iff exactly one of

(a) char F = 2, dim V is odd, and Q ≅ ⟨α⟩ ⊥ Q₀ with Q₀ regular and α ∈ Fˣ; (b) Q is regular

holds. Everything here is proved except the parity clause "dim V is odd" in (a):

• the dichotomy — the polar radical of a non-degenerate form is either 0 (case (b)) or a line (case (a)), exclusively — is isGPRRegular_xor_finrank_ker_polarBilin_eq_one;
• char F = 2 in case (a) is ringChar_eq_two_of_finrank_ker_polarBilin_eq_one;
• the decomposition in case (a) is exists_isometryEquiv_rankOne_prod, and needs no orthogonalisation: the generator u of the polar radical is orthogonal to everything already, so any complement of F u splits Q orthogonally.

The missing clause is not about quadratic forms at all. In characteristic 2 the polar form is alternating, and "dim V odd" is the statement that an alternating bilinear form on a finite-dimensional space has dim V ≡ dim (rad b) (mod 2) — equivalently that a non-degenerate alternating form forces even dimension, the symplectic-basis theorem. mathlib has neither that nor the Pfaffian, and proving it means the usual induction: split off a hyperbolic plane span {v, w} with b v w = 1, pass to {x | b v x = 0 ∧ b w x = 0}, and induct. That is a self-contained piece of bilinear algebra, better placed in a file of its own (or upstreamed) than bolted on here. It is not attempted in this file.

Part A: isotropy over an algebraically closed field

theorem QuadraticForm.exists_ne_zero_eq_zero_of_isAlgClosed {K : Type u_1} [Field K] [IsAlgClosed K] {W : Type u_2} [AddCommGroup W] [Module K W] (Q : QuadraticForm K W) {e f : W} (he : e ≠ 0) (hf : ∀ (t : K), t • e + f ≠ 0) : ∃ (w : W), w ≠ 0 ∧ Q w = 0

theorem QuadraticForm.finrank_le_one_of_anisotropic_of_isAlgClosed {K : Type u_1} [Field K] [IsAlgClosed K] {W : Type u_2} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K W) (hQ : QuadraticMap.Anisotropic Q) : Module.finrank K W ≤ 1

Part B: base change of the radical of the polar form

theorem QuadraticForm.ker_polarBilin_baseChangeOfProjective {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Module.Finite F V] [Module.Projective F V] {L : Type u_1} [Field L] [Algebra F L] (Q : QuadraticForm F V) : LinearMap.ker (QuadraticMap.polarBilin (baseChangeOfProjective L Q)) = (LinearMap.baseChange L (QuadraticMap.polarBilin Q)).ker

The polar form of a base-changed quadratic form has the same kernel as the base change of the polar form as a plain linear map: the two differ by the dual-comparison isomorphism of GPR 9.15, which is injective.

theorem QuadraticForm.finrank_ker_polarBilin_baseChangeOfProjective {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Module.Finite F V] [Module.Projective F V] {L : Type u_1} [Field L] [Algebra F L] (Q : QuadraticForm F V) : Module.finrank L ↥(LinearMap.ker (QuadraticMap.polarBilin (baseChangeOfProjective L Q))) = Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q))

The radical of the polar form is compatible with base change. Its dimension is unchanged: L is flat over the field F, so L ⊗[F] ker b ≃ ker b_L (LinearMap.tensorKerEquiv).

theorem QuadraticForm.one_tmul_mem_ker_polarBilin_baseChangeOfProjective {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Module.Finite F V] [Module.Projective F V] {L : Type u_1} [Field L] [Algebra F L] (Q : QuadraticForm F V) {u : V} (hu : u ∈ LinearMap.ker (QuadraticMap.polarBilin Q)) : 1 ⊗ₜ[F] u ∈ LinearMap.ker (QuadraticMap.polarBilin (baseChangeOfProjective L Q))

A vector killed by the polar form stays killed after base change.

Part C: the two substantive implications

theorem QuadraticForm.one_tmul_ne_zero {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] {L : Type u_1} [Field L] [Algebra F L] {u : V} (hu : u ≠ 0) : 1 ⊗ₜ[F] u ≠ 0

A nonzero vector stays nonzero in L ⊗[F] V: apply a functional separating it from 0.

theorem QuadraticForm.isGPRNonsingular_of_radical_eq_bot_of_finrank_ker_le_one {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hrad : QuadraticMap.radical Q = ⊥) (hdim : Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) ≤ 1) : Q.IsGPRNonsingular

EKM 7.16, (3) ⇒ (1); GPR Exc. 11.37, (ii) ⇒ (i). If the radical of Q vanishes and the radical of its polar form has dimension at most 1, then Q is non-singular.

If dim (rad b_Q) = 0 the polar radical stays 0 after base change and there is nothing to kill. If dim (rad b_Q) = 1, say rad b_Q = F u, then Q u ≠ 0 (else u would lie in the radical of Q), and after base change rad b_{Q_L} = L (1 ⊗ u); an element a ⊗ u of the radical of Q_L has 0 = Q_L (a ⊗ u) = Q(u) a², forcing a = 0.

theorem QuadraticForm.radical_eq_bot_of_radical_baseChangeOfProjective_eq_bot {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {K : Type u_1} [Field K] [Algebra F K] (Q : QuadraticForm F V) (hK : QuadraticMap.radical (baseChangeOfProjective K Q) = ⊥) : QuadraticMap.radical Q = ⊥

Half of EKM 7.16, (2) ⇒ (3); GPR Exc. 11.37, (iii) ⇒ (ii): the radical of Q already vanishes as soon as it vanishes after one base change, algebraically closed or not. (rad Q)_K ⊆ rad Q_K, and 1 ⊗ u = 0 forces u = 0.

theorem QuadraticForm.finrank_ker_polarBilin_le_one_of_isAlgClosed {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {K : Type u_1} [Field K] [IsAlgClosed K] [Algebra F K] (Q : QuadraticForm F V) (hK : QuadraticMap.radical (baseChangeOfProjective K Q) = ⊥) : Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) ≤ 1

The other half of EKM 7.16, (2) ⇒ (3); GPR Exc. 11.37, (iii) ⇒ (ii): over an algebraically closed K, vanishing of rad Q_K bounds the dimension of the polar radical by 1.

Q_K restricted to rad b_{Q_K} is anisotropic — an isotropic vector there would lie in rad Q_K — and over an algebraically closed field an anisotropic form has dimension at most one (QuadraticForm.finrank_le_one_of_anisotropic_of_isAlgClosed). The dimension then descends to F because the polar radical commutes with base change.

theorem QuadraticForm.isGPRNonsingular_of_isAlgClosed {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {K : Type u_1} [Field K] [IsAlgClosed K] [Algebra F K] (Q : QuadraticForm F V) (hK : QuadraticMap.radical (baseChangeOfProjective K Q) = ⊥) : Q.IsGPRNonsingular

GPR Exc. 11.37, (iii) ⇒ (i). A single algebraically closed base change suffices: if rad Q_K = 0 for one algebraically closed K ⊇ F, then Q is non-singular.

theorem QuadraticForm.isGPRNonsingular_iff_nondegenerate {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) : Q.IsGPRNonsingular ↔ QuadraticMap.Nondegenerate

EKM Lemma 7.16, (1) ↔ (3); GPR Exercise 11.37, (i) ↔ (ii). Q is non-singular exactly when its radical vanishes and the radical of its polar form is at most a line.

The right-hand side is mathlib's QuadraticMap.Nondegenerate, which is EKM's condition (3) taken as the definition. So this identifies our base-change-stable IsGPRNonsingular — and therefore QuadraticForm.IsEKMNondegenerate — with mathlib's predicate.

theorem QuadraticForm.isEKMNondegenerate_iff_nondegenerate {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) : Q.IsEKMNondegenerate ↔ QuadraticMap.Nondegenerate

EKM Definition 7.17 is mathlib's QuadraticMap.Nondegenerate. EKM defines non-degeneracy by condition (1) of Lemma 7.16 — the reading QuadraticForm.IsEKMNondegenerate formalizes — while mathlib takes condition (3). EKM 7.16 says they agree.

theorem QuadraticForm.isGPRNonsingular_tfae {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) : [Q.IsGPRNonsingular, QuadraticMap.radical Q = ⊥ ∧ Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) ≤ 1, QuadraticMap.radical (baseChangeOfProjective (AlgebraicClosure F) Q) = ⊥, ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra F K] [IsAlgClosed K], QuadraticMap.radical (baseChangeOfProjective K Q) = ⊥].TFAE

GPR Exercise 11.37. For a quadratic form over a field, on a finite-dimensional space, the following are equivalent:

(i) Q is non-singular; (ii) Q is non-degenerate and the radical of its polar form has dimension at most 1; (iii) Q_K is non-degenerate for some algebraically closed K ⊇ F; (iv) Q_K is non-degenerate for every algebraically closed K ⊇ F.

Condition (ii) is QuadraticMap.Nondegenerate, so this is EKM Lemma 7.16 with the extra rung (iv). Condition (iii) is stated at the canonical choice AlgebraicClosure F; that this really captures "some" is QuadraticForm.isGPRNonsingular_of_isAlgClosed, which accepts any algebraically closed K.

Part D: GPR Exc. 11.37, Remark (1)

theorem QuadraticForm.isGPRRegular_iff_ker_polarBilin_eq_bot {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) : Q.IsGPRRegular ↔ LinearMap.ker (QuadraticMap.polarBilin Q) = ⊥

Over a finite-dimensional space regularity is exactly vanishing of the polar radical: polarBilin Q is injective iff bijective, V and Module.Dual F V having equal dimension.

theorem QuadraticForm.isGPRRegular_iff_finrank_ker_polarBilin_eq_zero {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) : Q.IsGPRRegular ↔ Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 0

Regularity in terms of the dimension of the polar radical.

theorem QuadraticForm.isGPRRegular_xor_finrank_ker_polarBilin_eq_one {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hnd : QuadraticMap.Nondegenerate) : Xor Q.IsGPRRegular (Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 1)

Remark (1), the dichotomy. For a non-degenerate Q on a finite-dimensional space, the polar radical is either 0 — the regular case, (b) — or a line, case (a). The two are mutually exclusive, so exactly one holds.

theorem QuadraticForm.isGPRRegular_of_radical_eq_bot_of_invertible_two {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] [Invertible 2] (Q : QuadraticForm F V) (hrad : QuadraticMap.radical Q = ⊥) : Q.IsGPRRegular

Remark (1), case (a) forces characteristic 2. If 2 is invertible then a non-degenerate form is automatically regular, by GN (C.8.2)'s non-base-changed half (QuadraticForm.radical_eq_bot_iff_injective_polarBilin): with 2 invertible the extra Q m = 0 clause in the radical is redundant, so radical Q = ⊥ already says polarBilin Q is injective.

theorem QuadraticForm.two_eq_zero_of_finrank_ker_polarBilin_eq_one {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hrad : QuadraticMap.radical Q = ⊥) (hdim : Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 1) : 2 = 0

Remark (1), case (a) forces characteristic 2, stated as (2 : F) = 0.

theorem QuadraticForm.ringChar_eq_two_of_finrank_ker_polarBilin_eq_one {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hrad : QuadraticMap.radical Q = ⊥) (hdim : Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 1) : ringChar F = 2

The same conclusion as ringChar F = 2, matching GPR's phrasing "char F = 2".

theorem QuadraticForm.exists_isometryEquiv_rankOne_prod {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hrad : QuadraticMap.radical Q = ⊥) (hdim : Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 1) : ∃ (W : Submodule F V) (α : F), α ≠ 0 ∧ IsGPRRegular (QuadraticMap.comp Q W.subtype) ∧ Nonempty ((QuadraticMap.prod (rankOne α) (QuadraticMap.comp Q W.subtype)).IsometryEquiv Q)

Remark (1), case (a): the orthogonal decomposition q = q₀ ⊥ ⟨α⟩.

If the polar radical of a non-degenerate Q is the line F u, then α := Q u ≠ 0 and Q splits as ⟨α⟩ ⊥ Q|W for any complement W of F u, with Q|W regular.

No orthogonalisation is needed: u is in the radical of the polar form, so polar Q u w = 0 already holds for every w, making the decomposition orthogonal automatically. Q|W is regular because a vector of W killed by Q|W is killed by all of Q's polar form — it is orthogonal to u for free — hence lies in F u ⊓ W = 0.

theorem QuadraticForm.isGPRRegular_xor_charTwo_rankOne_decomposition {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hnd : QuadraticMap.Nondegenerate) : Xor Q.IsGPRRegular (Module.finrank F ↥(LinearMap.ker (QuadraticMap.polarBilin Q)) = 1 ∧ ringChar F = 2 ∧ ∃ (W : Submodule F V) (α : F), α ≠ 0 ∧ IsGPRRegular (QuadraticMap.comp Q W.subtype) ∧ Nonempty ((QuadraticMap.prod (rankOne α) (QuadraticMap.comp Q W.subtype)).IsometryEquiv Q))

GPR Exc. 11.37, Remark (1), assembled — except for the parity clause "dim V is odd" in case (a), which is not proved here (see the module docstring).

For a non-degenerate Q on a finite-dimensional space over a field, exactly one of:

(b) Q is regular; or (a) the radical of the polar form is a line, char F = 2, and Q ≅ ⟨α⟩ ⊥ Q₀ for some α ≠ 0 and some regular Q₀ on a complement of that line.

GPR states case (a) with "dim V is odd" in place of the clause "the polar radical is a line". The two are equivalent given the parity theorem for alternating forms; the version here uses the polar-radical clause, which is what actually drives the proof and what makes the dichotomy exclusive.