Regularity of quadratic forms: the radical, IsGPRNondegenerate, IsGPRRegular,

IsGPRNonsingular, IsEKMNondegenerate

There is no agreement in the literature on the right words (nonsingular, regular, non-degenerate, etc.) for regularity conditions on quadratic forms, and worse, the same word means different things in different sources. To keep this straight, every regularity predicate in this file is named after the source whose convention it follows.

GPR 11.11 distinguishes four notions: weakly regular (the polar form is injective — mathlib's polarBilin.Nondegenerate/SeparatingLeft, overview §6(b)), non-degenerate (radical Q = ⊥, GN C.8(d)), non-singular (the radical vanishes after every field base change, GN C.8(e)), and regular (the polar form is an isomorphism onto the dual, not just injective).

⚠ Over a general ring these do not form a linear ladder. Since radical Q lies in the kernel of the polar form, regular ⇒ weakly regular ⇒ non-degenerate; and regular ⇒ non-singular for M finitely generated projective (GN (C.8.1)). Nothing else holds in general. x² over 𝔽₂ is non-degenerate (indeed non-singular) but not weakly regular, its polar form being zero; x² over 𝔽₂[ε]/(ε²) is non-singular but has ε in its radical; and 2x² over ℤ is weakly regular but not non-singular, since it vanishes modulo 2. Over any field non-singular ⇒ non-degenerate (the converse fails for x² + t y² over 𝔽₂(t), which acquires a radical vector over 𝔽₂(√t)), and for finite-dimensional forms over a field of characteristic not 2 all four notions agree.

EKM independently has its own two-rung ladder built from the same radical, calling its rungs "regular" and "non-degenerate" — words that collide with, but do not mean the same thing as, GPR's "regular" and "non-degenerate".

Main definitions

• QuadraticForm.IsGPRNondegenerate : QuadraticMap.radical Q = ⊥, GPR's own "non-degenerate" rung. The radical is mathlib's QuadraticMap.radical, the submodule of vectors on which both Q and its polar form vanish (GN C.8(d), EKM II §7). It lies in the kernel of the polar form, so radical Q = ⊥ is weaker than mathlib's LinearMap.BilinForm.Nondegenerate/SeparatingLeft (injectivity of the polar form); x² over 𝔽₂ separates them. IsGPRNondegenerate is not the same as mathlib's QuadraticMap.Nondegenerate, which also bounds the rank of the polar radical and over a field is the IsGPRNonsingular condition (QuadraticForm/NonsingularOverFields.lean), nor the same as EKM's "non-degenerate" (see QuadraticForm.IsEKMNondegenerate below).
• QuadraticForm.IsGPRRegular : polarBilin Q is a bijection onto Module.Dual R M, not merely injective (SeparatingLeft/weakly regular only asks injectivity). Equivalently, polarBilin Q is a mathlib perfect pairing (QuadraticForm.isGPRRegular_iff_isPerfPair).
• QuadraticForm.IsGPRNonsingular : radical (Q.baseChangeOfProjective F) = ⊥ for every field F with [Algebra R F] (GN C.8(e)). GPR calls this property non-singular; readers may know the same condition as non-degenerate, ordinary, or semiregular, especially over fields (GPR Exc. 11.37, Remark (2)).
• QuadraticForm.IsEKMNondegenerate : for Q over a field F, radical (Q.baseChangeOfProjective K) = ⊥ for every field K with [Algebra F K] (EKM Definition 7.17, condition (1) of Lemma 7.16). Literally the same universal statement as IsGPRNonsingular specialized to R already a field — see QuadraticForm.isEKMNondegenerate_iff_isGPRNonsingular below.

Main results

• QuadraticForm.IsGPRRegular.isGPRNondegenerate : regularity implies that the radical vanishes.
• QuadraticForm.radical_eq_bot_iff_injective_polarBilin : when 2 ∈ Rˣ, Q.radical = ⊥ agrees exactly with mathlib's weakly-regular/Nondegenerate (GN (C.8.2), non-base-changed half). This is what makes IsGPRNondegenerate collapse onto mathlib's Nondegenerate once 2 is invertible, and it needs no base change at all: it is a fact about Q over R itself.
• QuadraticForm.IsGPRRegular.isGPRNonsingular : Q regular implies Q non-singular for M finitely generated projective (GN (C.8.1)), via QuadraticForm.IsGPRRegular.injective_polarBilin_baseChangeOfProjective — regularity survives base change as injectivity of the polar form.
• Module.Dual.bijective_of_forall_residue_field_injective : a map from a finite free module to its dual that is injective after base change to every residue field is bijective — the determinant heart of GN (C.8.2)'s converse.
• QuadraticForm.isGPRRegular_of_forall_baseChangeOfProjective_isGPRRegular : regularity after every field base change implies regularity over the base ring, for a finite projective module.
• QuadraticForm.IsGPRNonsingular.bijective_baseChange_of_isLocalRing : the same statement for M finite projective, after base change to an arbitrary local R-algebra, where M becomes free.
• QuadraticForm.IsGPRNonsingular.isGPRRegular, QuadraticForm.isGPRRegular_iff_isGPRNonsingular : GN (C.8.2)'s converse (non-singular implies regular when 2 ∈ Rˣ) and the resulting equivalence.
• QuadraticMap.radical_prod_eq_bot, QuadraticMap.radical_eq_bot_left_of_radical_prod_eq_bot : how the radical of an orthogonal sum QuadraticMap.prod relates to those of its summands, over an arbitrary base ring.
• QuadraticForm.baseChangeOfProjective_prod : base change of an orthogonal sum is the orthogonal sum of the base changes, along the canonical A ⊗[R] (M₁ × M₂) ≃ (A ⊗ M₁) × (A ⊗ M₂).
• QuadraticForm.IsGPRNonsingular.of_prod_left, .of_prod_right, QuadraticForm.IsGPRRegular.prod_isGPRNonsingular : GN (C.8.3), the two implications relating non-singularity to orthogonal sums. The asymmetry is essential — the second needs q₁ regular, not merely non-singular.
• QuadraticForm.isGPRNonsingular_rankOne, QuadraticForm.isGPRRegular_rankOne_iff : the rank-one form ⟨u⟩ : r ↦ u * r ^ 2 is non-singular for u a unit, but regular only when 2 * u is one — so IsGPRNonsingular is strictly weaker than IsGPRRegular, and the 2 ∈ Rˣ hypothesis above is sharp. QuadraticForm.not_isGPRRegular_rankOne_one_int is the concrete witness over ℤ.
• QuadraticForm.isEKMNondegenerate_iff_isGPRNonsingular : over a field R, IsEKMNondegenerate and IsGPRNonsingular are the same predicate.
• QuadraticForm.isGPRRegular_prod_iff : an orthogonal sum is regular exactly when both summands are.
• QuadraticForm.IsGPRRegular.smul_of_isUnit, QuadraticForm.isUnit_of_isGPRRegular_smul : rescaling by a unit preserves regularity, and on a module with a unimodular element a regular rescaling c • q forces c to be a unit.
• QuadraticMap.injOn_ker_polarBilin, QuadraticMap.two_smul_eq_zero_of_mem_ker_polarBilin : for Q with vanishing radical, Q is injective on the kernel of its polar form, and 2 kills that kernel (the assertion 2 C⊥ = 0 of GPR 19.3).

All results in this file are complete; there are no sorrys.

Implementation notes

IsGPRNonsingular is stated for M finitely generated projective over R, matching GN's own definition of a "quadratic form" (finite projectivity of the module is part of the data, not a separate hypothesis). It routes through QuadraticForm.baseChangeOfProjective (QuadraticForm/BaseChangeProjective.lean), not mathlib's QuadraticForm.baseChange: the latter requires [Invertible (2 : R)] (built from the halved QuadraticMap.associated) and is therefore inapplicable to exactly the characteristic-2 example (GPR 19.4, Layer 8) this development exists to support — the trap overview §6(a) is about.

What is used, and from where. GPR 9.15, that duals of finitely generated projective modules commute with base change, is TauCeti's TauCeti.Module.Dual.baseChangeEvaluationEquiv, which identifies A ⊗[R] (Module.Dual R M) with Module.Dual A (A ⊗[R] M); its rank consequence is TauCeti.Module.rankAtStalk_dual.

Consequently, GN (C.8.1) (Q regular implies Q non-singular) is proved for every finitely generated projective M, with no freeness hypothesis.

The other piece the free case needed was a compatibility fact between mathlib's LinearMap.BilinForm.baseChange (built via tensorDistrib) and the composite of ordinary linear base change with the dual-comparison map above; that is LinearMap.BilinForm.baseChange_eq_comp_dualBaseChange, proved directly by checking both sides on pure tensors.

The converse half of GN (C.8.2), and why it needed care. Non-singular implies regular is the classical local-global argument, in three steps, none of them deep:

1. Over a ring where the module is free, polarBilin Q is a square matrix, and a matrix is invertible iff its determinant is a unit iff that determinant lies in no maximal ideal — so injectivity after base change to each residue field (which is what non-singularity supplies) forces invertibility. That is Module.Dual.bijective_of_forall_residue_field_injective.
2. Over a local ring S, a finite projective M becomes free (finite + flat over a local ring), so step 1 applies to S ⊗[R] M. That is QuadraticForm.IsGPRNonsingular.bijective_baseChange_of_isLocalRing.
3. A linear map that is bijective after base change to Localization.AtPrime 𝔪 for every maximal 𝔪 is bijective. That is LinearMap.bijective_of_forall_baseChange_atPrime_bijective.

Mathematically that is the whole proof, and every step was easy. What made it hard in Lean was naming residue fields concretely, and the fix in both places was to keep them abstract:

• Step 1's hypothesis is phrased as "for every field F with [Algebra S F] whose structure map has kernel 𝔪", not as "for S ⧸ 𝔪". Since IsGPRNonsingular accepts any field carrying an R-algebra structure, and a residue field of S carries one via R → S → F, step 2 can feed it such an F with no residue-field identification at all — no IsLocalization.AtPrime.equivQuotMaximalIdeal, no IsLocalRing.eq_maximalIdeal. Had the hypothesis kept the concrete S ⧸ 𝔪, step 2 would have to elaborate Localization.AtPrime 𝔪 ⧸ 𝔫, a quotient of a localization, whose CommSemiring instance diverges against the ring structure underlying Ideal.Quotient.field 𝔫; an earlier attempt along those lines ran for eight hours without terminating.
• Step 2 is likewise stated for an arbitrary local R-algebra S, with the localization supplied only in the one-line corollary bijective_baseChange_atPrime. With S a variable, SMul R S can only be Algebra.toSMul, so the IsScalarTower R S F the proof builds for a residue field typechecks on the nose; at the concrete localization it would have to be reconciled with OreLocalization.instSMulOfIsScalarTower.

One further instance subtlety, recorded because it is easy to hit again: inside step 1 the residue field structure on S ⧸ 𝔪 must be introduced with letI, not haveI. hinj synthesizes Field F first and then wants an Algebra S F over that semiring structure; an opaque haveI prevents Field.toSemiring from unfolding to the quotient's own CommRing, and Algebra S (S ⧸ 𝔪) then fails to synthesize outright.

Sharpness of 2 ∈ Rˣ. That hypothesis in GN (C.8.2) is not an artifact of the proof: QuadraticForm.rankOne, the form ⟨u⟩ : r ↦ u * r ^ 2 on R itself, is non-singular for every unit u (isGPRNonsingular_rankOne) but regular exactly when 2 * u — equivalently 2 — is a unit (isGPRRegular_rankOne_iff, isGPRRegular_rankOne_iff_isUnit_two). Over ℤ with u = 1 this separates the two predicates outright. See the section at the end of this file.

Comparison with EKM. GN C.9 identifies non-singularity over a field with EKM's notion of non-degeneracy. Traced to source: GN cites EKM Definition 7.17, which in turn rests on EKM Lemma 7.16. Unlike GPR and GN, EKM only ever works with quadratic forms over a field, never over a general commutative ring — so its terminology only competes with GPR's once R is specialized to a field, and any Lean statement relating the two must carry that hypothesis explicitly rather than silently inheriting it. For a quadratic form ϕ over a field F with polar form b_ϕ, EKM write rad ϕ := {v ∈ rad b_ϕ : ϕ(v) = 0} — precisely mathlib's QuadraticMap.radical — and call ϕ regular if rad ϕ = 0.

⚠ This is a third name for our IsGPRNondegenerate, not for IsGPRRegular. EKM's "regular" means rad ϕ = 0, matching QuadraticForm.IsGPRNondegenerate, not the bijective-polar-form QuadraticForm.IsGPRRegular above — a second, independent collision on top of the "non-degenerate" one already noted, both worth getting right before formalizing EKM's statements here.

EKM Lemma 7.16 shows TFAE: (1) ϕ_K is EKM-regular for every field extension K/F; (2) ϕ_K is EKM-regular for some algebraically closed K ⊇ F; (3) ϕ is EKM-regular and dim (rad b_ϕ) ≤ 1. Definition 7.17 calls ϕ non-degenerate when these hold; this is QuadraticForm.IsEKMNondegenerate below, defined via condition (1) since it is the one that reads verbatim as a base-change statement. When R is already a field, condition (1) is literally IsGPRNonsingular Q (Algebra R F for F a field is automatically a field extension of R, field homomorphisms being injective) — the two quantify over exactly the same class of base changes — which is QuadraticForm.isEKMNondegenerate_iff_isGPRNonsingular below. That equality of predicates is immediate from the definitions. EKM Lemma 7.16 itself (that conditions (1)–(3) agree) is proved in QuadraticForm/NonsingularOverFields.lean, by EKM's own elementary argument rather than by GN's C.9, whose proof cites an external étale-cover argument GN does not reprove and which overview §8 asks us not to import wholesale. That file also proves GPR Exercise 11.37 and most of its Remark (1).

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Cambridge University Press, New Mathematical Monographs vol. 48, 2024. 11.11, 19.3, 19.4.
• [GPR 42] Calmès, Fasel, Groupes classiques, Panoramas & Synthèses 46 (2015), 1–133.
• [GPR 53] Conrad, Reductive group schemes, in Autour des schémas en groupes, vol. I, Panoramas & Synthèses 42/43 (2014), 93–444.
• [GPR 60] Deligne, Katz, Groupes de Monodromie en Géométrie Algébrique: Séminaire de Géométrie Algébrique du Bois-Marie 1967–1969 (SGA 7 II), vol. 340, Springer, 2006.
• [GPR 157] Knus, Quadratic and Hermitian Forms over Rings, vol. 294, Springer-Verlag, 1991.
• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, Appendix C (C.8, C.9).
• [EKM] Elman, Karpenko, Merkurjev, The Algebraic and Geometric Theory of Quadratic Forms, AMS Colloquium Publications vol. 56, 2008. §7.A, Lemma 7.16, Definition 7.17.

def QuadraticForm.IsGPRNondegenerate {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Prop

Q is non-degenerate in GPR's sense (GPR 11.11, overview §6(b)): QuadraticMap.radical Q = ⊥. This is a genuinely different, weaker notion than mathlib's polarBilin.Nondegenerate (GPR's "weakly regular"), which asks the polar form itself to be injective: the radical lies in the kernel of the polar form, so an injective polar form forces radical Q = ⊥, but not conversely — x² over 𝔽₂ has zero polar form and zero radical.

The radical itself is mathlib's QuadraticMap.radical — the submodule of vectors on which both Q and its polar form vanish (GN C.8(d), EKM Chapter II §7). Constraining Q itself, not just the polar form, is what makes it smaller than the kernel of the polar form, which is all that mathlib's bilinear-form nondegeneracy predicates see — see overview §6(b).

Terminology. Named for its source, GPR, since EKM uses "non-degenerate" for a different, stronger condition — see QuadraticForm.IsEKMNondegenerate below. Note in particular that this is not mathlib's QuadraticMap.Nondegenerate, which additionally bounds the rank of the polar radical and over a field is the IsGPRNonsingular condition; see QuadraticForm/NonsingularOverFields.lean.

Equations

• Q.IsGPRNondegenerate = (QuadraticMap.radical Q = ⊥)

def QuadraticForm.IsGPRRegular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Prop

Q is regular: its polar form is a bijection M ≃ Module.Dual R M, not merely injective. The strongest of GPR 11.11's notions: it implies the other three (non-singularity for M finitely generated projective).

Terminology. Named for its source, GPR, since EKM uses "regular" for the weaker condition radical Q = ⊥ — see QuadraticForm.IsEKMNondegenerate below.

Equations

• Q.IsGPRRegular = Function.Bijective ⇑(QuadraticMap.polarBilin Q)

theorem QuadraticForm.isGPRRegular_iff_isPerfPair {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : Q.IsGPRRegular ↔ LinearMap.IsPerfPair (QuadraticMap.polarBilin Q)

GPR's regularity is mathlib's perfect pairing: Q is regular exactly when its polar form is a LinearMap.IsPerfPair. The polar form is symmetric, so bijectivity in one argument already gives it in the other. This opens mathlib's perfect-pairing API to regular forms.

theorem QuadraticForm.IsGPRRegular.isGPRNondegenerate {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (h : Q.IsGPRRegular) : Q.IsGPRNondegenerate

A regular quadratic form is non-degenerate in GPR's sense: its radical lies in the kernel of the polar map, and that kernel vanishes because the polar map is injective.

def QuadraticForm.IsGPRNonsingular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (Q : QuadraticForm R M) : Prop

Q is non-singular (GN C.8(e)): its radical vanishes after base change to every field extension of R. Uses QuadraticForm.baseChangeOfProjective (QuadraticForm/BaseChangeProjective.lean), which needs no hypothesis on 2.

Terminology. Named for its source, GPR. GPR's Remark (2) following Exercise 11.37 notes that this condition is called non-degenerate in [GPR 53, §6.1 and Exercise 1.6.10], ordinary in [GPR 60, §XII.1], and semiregular in [GPR 157, §IV.3] or [GPR 42, §2.6]. Thus, over a field, a reader may have met GPR's "non-singular" quadratic forms under any of those names. Here non-degenerate in that literature-synonym sense must not be confused with either QuadraticForm.IsGPRNondegenerate above (the radical Q = ⊥ rung over the base ring) or mathlib's LinearMap.BilinForm.Nondegenerate (GPR's "weakly regular": an injective polar form). When R is already a field, this condition coincides with EKM's own "non-degenerate" — QuadraticForm.IsEKMNondegenerate below.

Equations

• Q.IsGPRNonsingular = ∀ (F : Type ?u.1) [inst : Field F] [inst_1 : Algebra R F], QuadraticMap.radical (QuadraticForm.baseChangeOfProjective F Q) = ⊥

theorem QuadraticForm.radical_eq_bot_iff_injective_polarBilin {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) : QuadraticMap.radical Q = ⊥ ↔ Function.Injective ⇑(QuadraticMap.polarBilin Q)

When 2 is invertible, radical Q = ⊥ (GPR's non-degenerate) agrees exactly with mathlib's polarBilin.Nondegenerate/SeparatingLeft (GPR's weakly regular) — GN (C.8.2)'s non-base-changed half. No base change is involved: 2 • Q m = polar Q m m lets Q m = 0 be recovered from the polar form vanishing, so the extra Q m = 0 clause in the radical becomes redundant. That last step is mathlib's QuadraticMap.radical_eq_ker_polarBilin.

theorem Module.Dual.bijective_of_forall_residue_field_injective {S : Type s} [CommRing S] {P : Type u_1} [AddCommGroup P] [Module S P] {ι : Type u_2} [Finite ι] (v : Basis ι S P) {g : P →ₗ[S] Dual S P} (hinj : ∀ (𝔪 : Ideal S) [𝔪.IsMaximal] (F : Type s) [inst : Field F] [inst_1 : Algebra S F], RingHom.ker (algebraMap S F) = 𝔪 → Function.Injective ⇑(LinearMap.baseChange F g)) : Function.Bijective ⇑g

If a linear map from a finite free module into its own dual is injective after base change to every residue field of the base ring, it is bijective. Used for the base-changed half of GN (C.8.2) (QuadraticForm.IsGPRNonsingular.isGPRRegular below), applied after localizing at each maximal ideal.

The matrix of the map, computed in a chosen basis and its dual basis, has determinant that cannot lie in any maximal ideal: its image in each residue field is the determinant of a matrix representing an injective — hence, by a dimension count, bijective — map, so is nonzero. Hence the determinant is a unit, and a unit-determinant map is bijective.

The residue field is kept abstract, presented as any field F with [Algebra S F] whose structure map has kernel 𝔪, rather than as the concrete S ⧸ 𝔪. Only the kernel condition is used (to see that a determinant lying in 𝔪 dies in F), and the proof instantiates F at S ⧸ 𝔪 internally — where S is still an abstract ring, so nothing expensive is formed. The payoff is at the call site: QuadraticForm.IsGPRNonsingular.bijective_baseChange_atPrime below instantiates S at Localization.AtPrime 𝔪, and the concrete form of this hypothesis would force Lean to elaborate Localization.AtPrime 𝔪 ⧸ 𝔫 — a quotient of a localization, whose CommSemiring instance search diverges against the one under Ideal.Quotient.field 𝔫. With F abstract that term never appears, and IsGPRNonsingular — which accepts any field carrying an R-algebra structure, in particular F via R → S → F — applies directly, with no residue-field identification needed at all. F shares S's universe because the internal instantiation at S ⧸ 𝔪 lives there.

theorem LinearMap.bijective_of_forall_baseChange_atPrime_bijective {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (𝔪 : Ideal R) [inst : 𝔪.IsMaximal], Function.Bijective ⇑(baseChange (Localization.AtPrime 𝔪) f)) : Function.Bijective ⇑f

A linear map between two R-modules is bijective if it becomes bijective after base change to the localization at every maximal ideal of R. Bridges bijective_of_localized_maximal (stated for the concrete LocalizedModule localization) to base change along Localization.AtPrime, via the natural equivalence LocalizedModule.equivTensorProduct.

theorem LinearMap.BilinForm.baseChange_eq_comp_dualBaseChange {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Projective R M] [Module.Finite R M] (A : Type u_1) [CommRing A] [Algebra R A] (B : LinearMap.BilinForm R M) : BilinForm.baseChange A B = ↑TauCeti.Module.Dual.baseChangeEvaluationEquiv ∘ₗ baseChange A B

The base change of a bilinear form (LinearMap.BilinForm.baseChange, built via tensorDistrib) agrees with base-changing it as a linear map into the dual and then applying the dual-base-change equivalence from GPR 9.15. Checked directly on pure tensors.

theorem QuadraticForm.isGPRRegular_of_forall_baseChangeOfProjective_isGPRRegular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Projective R M] [Module.Finite R M] (Q : QuadraticForm R M) (h : ∀ (F : Type u) [inst : Field F] [inst_1 : Algebra R F], (baseChangeOfProjective F Q).IsGPRRegular) : Q.IsGPRRegular

A quadratic form on a finite projective module is regular if it becomes regular after base change to every field over the base ring.

This is the local-global principle for the polar map. After localizing at a maximal ideal, the module becomes finite free. The polar map is then bijective by Nakayama's lemma because its base change to every residue field is injective; the latter is the assumed regularity after the corresponding composite field extension of R.

theorem QuadraticForm.IsGPRRegular.injective_polarBilin_baseChangeOfProjective {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Projective R M] [Module.Finite R M] {Q : QuadraticForm R M} (hReg : Q.IsGPRRegular) (A : Type u_1) [CommRing A] [Algebra R A] : Function.Injective ⇑(QuadraticMap.polarBilin (baseChangeOfProjective A Q))

Regularity is stable under base change. Base-changing the bijection polarBilin Q : M ≃ Module.Dual R M as a plain linear map keeps it injective, and composing with the always-bijective dual-comparison map of GPR 9.15 (LinearMap.BilinForm.baseChange_eq_comp_dualBaseChange) identifies the result with the polar form of the base-changed quadratic form.

theorem QuadraticForm.IsGPRRegular.isGPRNonsingular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Projective R M] [Module.Finite R M] {Q : QuadraticForm R M} (hReg : Q.IsGPRRegular) : Q.IsGPRNonsingular

GN (C.8.1). Q regular implies Q non-singular: over every field the polar form of the base change stays injective (IsGPRRegular.injective_polarBilin_baseChangeOfProjective), which is exactly what a vanishing radical needs.

theorem QuadraticForm.IsGPRNonsingular.baseChangeOfProjective {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) (S : Type s) [CommRing S] [Algebra R S] : (QuadraticForm.baseChangeOfProjective S Q).IsGPRNonsingular

Non-singularity is stable under base change. This is the whole point of quantifying over every field in R-alg rather than asking for radical Q = ⊥ over R itself: a field over S is a field over R, and QuadraticForm.baseChangeOfProjectiveIsometryEquiv identifies the iterated base change (Q_S)_F with the direct one Q_F, whose radical vanishes by hypothesis.

The Algebra R F and IsScalarTower R S F instances are built inside the proof from Algebra R S and Algebra S F; they are not available to instance search, and the whole statement would be false-by-elaboration if F carried an unrelated R-algebra structure.

theorem QuadraticForm.IsGPRNonsingular.injective_baseChange {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) {F : Type u} [Field F] [Algebra R F] [Invertible 2] : Function.Injective ⇑(LinearMap.baseChange F (QuadraticMap.polarBilin Q))

If Q is non-singular, polarBilin Q stays injective after base change to any field F with Invertible (2 : F). The field-level half of the translation between IsGPRNonsingular and injectivity of polarBilin, isolated at the top level (rather than nested inside QuadraticForm.IsGPRNonsingular.isGPRRegular's proof) to keep its elaboration cheap.

theorem QuadraticForm.IsGPRNonsingular.injective_baseChange_baseChange {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) {S : Type u} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra S F] [Algebra R F] [IsScalarTower R S F] [Invertible 2] : Function.Injective ⇑(LinearMap.baseChange F (LinearMap.baseChange S (QuadraticMap.polarBilin Q)))

Iterating injective_baseChange through an intermediate ring S: if Q is non-singular, polarBilin Q base-changed to S and then to a further S-algebra field F stays injective. LinearMap.baseChange_baseChange identifies the iterated base change with the direct one to F (an R-algebra via R → S → F), where injective_baseChange applies.

F is kept fully generic (a bare {F : Type u} [Field F] [Algebra S F] [IsScalarTower R S F]), rather than fixed to a concrete S ⧸ 𝔫: baking a concrete quotient into the statement fixes some CommSemiring F instance for LinearMap.baseChange the moment the statement is elaborated, and separately deriving [Field F] from [𝔫.IsMaximal] inside the proof gives a second, propositionally-but-not-definitionally-equal instance — reconciling the two costs an expensive isDefEq on every use of Q.baseChangeOfProjective F. Keeping F abstract sidesteps the diamond; callers instantiate it (e.g. at S ⧸ 𝔫) themselves.

theorem QuadraticForm.IsGPRNonsingular.bijective_baseChange_of_isLocalRing {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Invertible 2] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] : Function.Bijective ⇑(LinearMap.baseChange S (QuadraticMap.polarBilin Q))

Over any local R-algebra S, polarBilin Q becomes bijective after base change: a finite projective M is free after base change to a local ring (M projective ⇒ flat, Module.Flat.of_projective; finite flat over a local ring is free, Module.free_of_flat_of_isLocalRing), so Module.Dual.bijective_of_forall_residue_field_injective applies to the resulting free module, with injective_baseChange_baseChange supplying its hypothesis at each residue field.

S is deliberately kept abstract rather than fixed to Localization.AtPrime 𝔪 (that is bijective_baseChange_atPrime below, an immediate corollary). With S a variable, SMul R S can only be Algebra.toSMul, so the IsScalarTower R S F this proof must build for a residue field F typechecks on the nose. At the concrete localization it would instead have to reconcile Algebra.toSMul with OreLocalization.instSMulOfIsScalarTower — the same class of instance diamond that made the earlier, localization-first version of this proof intractable.

theorem QuadraticForm.IsGPRNonsingular.bijective_baseChange_atPrime {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Invertible 2] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) (𝔪 : Ideal R) [𝔪.IsMaximal] : Function.Bijective ⇑(LinearMap.baseChange (Localization.AtPrime 𝔪) (QuadraticMap.polarBilin Q))

For a fixed maximal ideal 𝔪, polarBilin Q becomes bijective after base change to Localization.AtPrime 𝔪. Immediate from bijective_baseChange_of_isLocalRing, since a localization at a prime is local.

theorem QuadraticForm.IsGPRNonsingular.isGPRRegular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Invertible 2] {Q : QuadraticForm R M} (hNS : Q.IsGPRNonsingular) : Q.IsGPRRegular

GN (C.8.2), converse direction. Q non-singular implies Q regular, when 2 ∈ Rˣ: bundle bijective_baseChange_atPrime over every maximal ideal via LinearMap.bijective_of_forall_baseChange_atPrime_bijective.

theorem QuadraticForm.isGPRRegular_iff_isGPRNonsingular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Invertible 2] (Q : QuadraticForm R M) : Q.IsGPRRegular ↔ Q.IsGPRNonsingular

GN (C.8.2), in full: for M finitely generated projective and 2 ∈ Rˣ, Q is regular iff Q is non-singular. Combines QuadraticForm.IsGPRRegular.isGPRNonsingular (no hypothesis on 2 needed) with QuadraticForm.IsGPRNonsingular.isGPRRegular (the converse, needing 2 ∈ Rˣ).

The rank-one form ⟨u⟩, and the sharpness of 2 ∈ Rˣ

GN (C.8.1) says regular implies non-singular unconditionally; GN (C.8.2) says the converse holds when 2 ∈ Rˣ. The rank-one form ⟨u⟩ : r ↦ u * r ^ 2 shows that hypothesis cannot be dropped: for u a unit, ⟨u⟩ is non-singular over any commutative ring but regular exactly when 2 is a unit. R = ℤ, u = 1 is the concrete separating example.

The two directions use genuinely different features of the definitions. Non-singularity needs only the Q m = 0 clause of QuadraticMap.radical — the clause that makes the radical smaller than the kernel of the polar form, which is all that mathlib's LinearMap.BilinForm.Nondegenerate sees — together with the absence of zero divisors in a field. Regularity, by contrast, is entirely about the polar form x ↦ 2 * u * x, which is where the 2 enters.

def QuadraticForm.rankOne {R : Type u} [CommRing R] (u : R) : QuadraticForm R R

The rank-one form ⟨u⟩ : r ↦ u * r ^ 2 on R itself.

This is mathlib's QuadraticMap.sq scaled by u, not a new construction; the abbreviation exists only so that GPR's ⟨u⟩ has a name here.

Equations

• QuadraticForm.rankOne u = u • QuadraticMap.sq

@[simp]

theorem QuadraticForm.rankOne_apply {R : Type u} [CommRing R] (u r : R) : (rankOne u) r = u * r ^ 2

@[simp]

theorem QuadraticForm.polar_rankOne {R : Type u} [CommRing R] (u x y : R) : QuadraticMap.polar (⇑(rankOne u)) x y = 2 * u * (x * y)

The polar form of ⟨u⟩ is (x, y) ↦ 2 * u * x * y: the factor 2 that GN (C.8.2) must invert is visible here, and is the whole content of the example.

theorem QuadraticForm.polarBilin_rankOne_apply_apply {R : Type u} [CommRing R] (u x y : R) : ((QuadraticMap.polarBilin (rankOne u)) x) y = 2 * u * (x * y)

The same computation for polarBilin. Not a simp lemma: simp already reaches this via QuadraticMap.polarBilin_apply_apply and QuadraticForm.polar_rankOne.

theorem QuadraticForm.isGPRRegular_rankOne_iff {R : Type u} [CommRing R] (u : R) : (rankOne u).IsGPRRegular ↔ IsUnit (2 * u)

⟨u⟩ is regular exactly when 2 * u is a unit. Under Module.Dual R R ≅ R the polar form is multiplication by 2 * u; surjectivity forces 2 * u * x = 1 for some x, and conversely an inverse w of 2 * u builds both the injectivity witness and the preimage w * f 1 of an arbitrary functional f.

theorem QuadraticForm.isGPRRegular_rankOne_iff_isUnit_two {R : Type u} [CommRing R] {u : R} (hu : IsUnit u) : (rankOne u).IsGPRRegular ↔ IsUnit 2

For u a unit, ⟨u⟩ is regular exactly when 2 ∈ Rˣ.

theorem QuadraticForm.isGPRNonsingular_rankOne {R : Type u} [CommRing R] {u : R} (hu : IsUnit u) : (rankOne u).IsGPRNonsingular

For u a unit, ⟨u⟩ is non-singular over every base ring, with no hypothesis on 2.

Every element of F ⊗[R] R is a ⊗ₜ 1, on which the base-changed form takes the value u • (a * a). The image of u in F is a unit, so u • (a * a) = 0 forces a * a = 0, hence a = 0 since a field has no zero divisors. Only the Q m = 0 half of QuadraticMap.radical is used; the polar form never enters, which is exactly why no assumption on 2 is needed.

theorem QuadraticForm.isGPRNonsingular_rankOne_one_int : (rankOne 1).IsGPRNonsingular

The separating example, half one. Over ℤ, the form ⟨1⟩ : r ↦ r ^ 2 is non-singular. Paired with QuadraticForm.not_isGPRRegular_rankOne_one_int, this shows IsGPRNonsingular is strictly weaker than IsGPRRegular over a general commutative ring.

theorem QuadraticForm.not_isGPRRegular_rankOne_one_int : ¬(rankOne 1).IsGPRRegular

The separating example, half two. Over ℤ, the form ⟨1⟩ : r ↦ r ^ 2 is not regular, since 2 is not a unit in ℤ. So the hypothesis [Invertible (2 : R)] in QuadraticForm.isGPRRegular_iff_isGPRNonsingular is not removable.

Rescaling by a unit

Multiplying a quadratic form by a unit changes neither its radical nor any of the rungs of the ladder. This is the ⟨-μ⟩ q of the Cayley–Dickson norm q ⊥ ⟨-μ⟩ q, where μ is a unit exactly in the theorems that need the double to be a composition algebra.

theorem QuadraticForm.IsGPRNonsingular.smul_of_isUnit {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {c : R} (hc : IsUnit c) {Q : QuadraticForm R M} (h : Q.IsGPRNonsingular) : (c • Q).IsGPRNonsingular

Rescaling by a unit preserves non-singularity, since it does so after every base change: the image of a unit under algebraMap is a unit.

GN (C.8.3): orthogonal sums

GN C.8(f) records how the ladder behaves under the orthogonal sum q₁ ⊥ q₂ — mathlib's QuadraticMap.prod. Regularity is symmetric (q₁ ⊥ q₂ is regular iff both are), but non-singularity is not, and (C.8.3) is exactly the pair of implications that do hold:

q₁ ⊥ q₂ non-singular ⇒ q₁ and q₂ non-singular, q₁ regular and q₂ non-singular ⇒ q₁ ⊥ q₂ non-singular.

The asymmetry is real, and visible in the radical: rad (q₁ ⊥ q₂) contains rad q₁ × rad q₂ but can be strictly larger, because q₁ m₁ + q₂ m₂ = 0 does not force q₁ m₁ = 0 = q₂ m₂. Regularity of q₁ is what kills the first coordinate outright and lets the second-coordinate equation collapse.

theorem QuadraticMap.inl_mem_radical_prod {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {x : M₁} (hx : x ∈ radical Q₁) : (x, 0) ∈ (prod Q₁ Q₂).radical

(x, 0) lies in the radical of Q₁ ⊥ Q₂ when x lies in the radical of Q₁.

theorem QuadraticMap.inr_mem_radical_prod {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {x : M₂} (hx : x ∈ radical Q₂) : (0, x) ∈ (prod Q₁ Q₂).radical

(0, x) lies in the radical of Q₁ ⊥ Q₂ when x lies in the radical of Q₂.

theorem QuadraticMap.radical_eq_bot_left_of_radical_prod_eq_bot {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : (prod Q₁ Q₂).radical = ⊥) : radical Q₁ = ⊥

A vanishing radical passes to the left summand.

theorem QuadraticMap.radical_eq_bot_right_of_radical_prod_eq_bot {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : (prod Q₁ Q₂).radical = ⊥) : radical Q₂ = ⊥

A vanishing radical passes to the right summand.

theorem QuadraticMap.radical_prod_eq_bot {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h₁ : Function.Injective ⇑(polarBilin Q₁)) (h₂ : radical Q₂ = ⊥) : (prod Q₁ Q₂).radical = ⊥

The ring-level heart of GN (C.8.3): an injective polar form on the left summand plus a vanishing radical on the right gives a vanishing radical on the sum.

Injectivity on the left is what breaks the symmetry. It forces the first coordinate of a radical vector to vanish, after which Q₁ 0 + Q₂ x₂ = 0 really does say Q₂ x₂ = 0.

theorem QuadraticMap.polar_comp_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (Q : QuadraticMap R M N) (f : M' →ₗ[R] M) (x y : M') : polar (⇑(Q.comp f)) x y = polar (⇑Q) (f x) (f y)

The polar form of a precomposition is the precomposed polar form: the pointwise form of mathlib's QuadraticMap.polarBilin_comp.

theorem QuadraticMap.mem_radical_comp_linearEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (Q : QuadraticMap R M N) (e : M' ≃ₗ[R] M) {x : M'} : x ∈ (Q.comp ↑e).radical ↔ e x ∈ Q.radical

Radical membership transports along a linear equivalence: mathlib's QuadraticMap.IsometryEquiv.map_radical for the isometry Q ≅ Q ∘ e.

theorem QuadraticMap.radical_comp_linearEquiv_eq_bot_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (Q : QuadraticMap R M N) (e : M' ≃ₗ[R] M) : (Q.comp ↑e).radical = ⊥ ↔ Q.radical = ⊥

Transporting a vanishing radical along a linear equivalence.

theorem QuadraticForm.baseChangeOfProjective_prod {R : Type u} [CommRing R] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_2} [AddCommGroup M₂] [Module R M₂] {A : Type u_3} [CommRing A] [Algebra R A] [Module.Finite R M₁] [Module.Projective R M₁] [Module.Finite R M₂] [Module.Projective R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : baseChangeOfProjective A (QuadraticMap.prod Q₁ Q₂) = (QuadraticMap.prod (baseChangeOfProjective A Q₁) (baseChangeOfProjective A Q₂)).comp ↑(TensorProduct.prodRight R A A M₁ M₂)

Base change of an orthogonal sum is the orthogonal sum of the base changes, along the canonical A ⊗[R] (M₁ × M₂) ≃ (A ⊗[R] M₁) × (A ⊗[R] M₂). Checked on pure tensors 1 ⊗ₜ m, where both sides come down to add_smul.

theorem QuadraticForm.IsGPRRegular.comp_linearEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type t₁} [AddCommGroup M'] [Module R M'] {Q : QuadraticForm R M} (h : Q.IsGPRRegular) (e : M' ≃ₗ[R] M) : IsGPRRegular (QuadraticMap.comp Q ↑e)

Regularity transports along a linear equivalence.

The polar map of Q ∘ e factors as e* ∘ polarBilin Q ∘ e, a composition of three bijections; no finiteness, projectivity or hypothesis on 2 is involved, unlike the non-singular version below, which has to pass through base change.

theorem QuadraticForm.isGPRRegular_comp_linearEquiv_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type t₁} [AddCommGroup M'] [Module R M'] {Q : QuadraticForm R M} (e : M' ≃ₗ[R] M) : IsGPRRegular (QuadraticMap.comp Q ↑e) ↔ Q.IsGPRRegular

Regularity is equivalent to regularity after precomposition with an equivalence.

theorem QuadraticForm.IsGPRNonsingular.comp_linearEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {M' : Type t₁} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [Module.Projective R M'] {Q : QuadraticForm R M} (h : Q.IsGPRNonsingular) (e : M' ≃ₗ[R] M) : IsGPRNonsingular (QuadraticMap.comp Q ↑e)

Non-singularity transports along a linear equivalence.

Base change turns the equivalence e : M' ≃ M into an equivalence F ⊗ M' ≃ F ⊗ M (LinearEquiv.baseChange), and a vanishing radical is invariant under precomposition with an equivalence (QuadraticMap.radical_comp_linearEquiv_eq_bot_iff).

theorem QuadraticForm.IsGPRNonsingular.of_prod_left {R : Type u} [CommRing R] {M₁ : Type t₁} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [Module.Projective R M₁] {M₂ : Type t₂} [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [Module.Projective R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : IsGPRNonsingular (QuadraticMap.prod Q₁ Q₂)) : Q₁.IsGPRNonsingular

GN (C.8.3), first implication (left summand). If q₁ ⊥ q₂ is non-singular, so is q₁.

Over any field, a radical vector of (q₁)_F gives the radical vector (x, 0) of (q₁ ⊥ q₂)_F.

theorem QuadraticForm.IsGPRNonsingular.of_prod_right {R : Type u} [CommRing R] {M₁ : Type t₁} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [Module.Projective R M₁] {M₂ : Type t₂} [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [Module.Projective R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : IsGPRNonsingular (QuadraticMap.prod Q₁ Q₂)) : Q₂.IsGPRNonsingular

GN (C.8.3), first implication (right summand). If q₁ ⊥ q₂ is non-singular, so is q₂.

theorem QuadraticForm.IsGPRRegular.prod_isGPRNonsingular {R : Type u} [CommRing R] {M₁ : Type t₁} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [Module.Projective R M₁] {M₂ : Type t₂} [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [Module.Projective R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h₁ : Q₁.IsGPRRegular) (h₂ : Q₂.IsGPRNonsingular) : IsGPRNonsingular (QuadraticMap.prod Q₁ Q₂)

GN (C.8.3), second implication. q₁ regular and q₂ non-singular imply q₁ ⊥ q₂ non-singular.

Regularity of q₁ — not merely non-singularity — is what is needed: it survives base change as injectivity of the polar form (IsGPRRegular.injective_polarBilin_baseChangeOfProjective), and that is exactly the hypothesis QuadraticMap.radical_prod_eq_bot consumes.

The hypothesis cannot be weakened to "q₁ non-singular". Over a field of characteristic 2 the polar form of ⟨1⟩ vanishes identically, so ⟨1⟩ is non-singular (isGPRNonsingular_rankOne) purely because a ^ 2 = 0 forces a = 0; but ⟨1⟩ ⊥ ⟨1⟩ sends (a, b) to a ^ 2 + b ^ 2 = (a + b) ^ 2, whose zero set is the line a = b, so the sum has a nonzero radical. That counterexample is not formalized here.

def QuadraticForm.IsEKMNondegenerate {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Module.Finite F V] [Module.Projective F V] (Q : QuadraticForm F V) : Prop

Q is non-degenerate in EKM's sense (EKM Definition 7.17, condition (1) of Lemma 7.16): unlike every other predicate in this file, this is only meaningful for Q over a field R — EKM never considers quadratic forms over a general commutative ring, so there is no ring-level analogue to state here. Q is IsEKMNondegenerate when its radical vanishes after base change along every field extension K of R.

Terminology. Named for its source, EKM, since EKM's "non-degenerate" is a different, stronger condition than GPR's "non-degenerate" — see QuadraticForm.IsGPRNondegenerate above. EKM's own weaker condition, radical Q = ⊥, is what EKM calls "regular", and is not what this predicate captures — that is QuadraticForm.IsGPRNondegenerate, again via the naming clash noted there.

Equations

• Q.IsEKMNondegenerate = Q.IsGPRNonsingular

theorem QuadraticForm.isEKMNondegenerate_iff_isGPRNonsingular {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Module.Finite F V] [Module.Projective F V] (Q : QuadraticForm F V) : Q.IsEKMNondegenerate ↔ Q.IsGPRNonsingular

Over a field R, EKM's non-degenerate (QuadraticForm.IsEKMNondegenerate) is literally the same universal statement as GPR's non-singular (QuadraticForm.IsGPRNonsingular): both quantify (Q.baseChangeOfProjective K).radical = ⊥ over the same class of fields K with [Algebra R K]. EKM Lemma 7.16 itself — that this condition agrees with EKM's other two formulations — is QuadraticForm.isEKMNondegenerate_iff_nondegenerate, in QuadraticForm/NonsingularOverFields.lean; this theorem only records that the definition chosen here for IsEKMNondegenerate (condition (1) of the lemma) coincides on the nose with the ring-theoretic IsGPRNonsingular once the ring is a field, which is GN C.9's claim.

Regularity of orthogonal sums and of rescaled forms

The orthogonal sum q₁ ⊥ q₂ of GPR 11.12 is mathlib's QuadraticMap.prod.

theorem QuadraticForm.IsGPRRegular.prod {R : Type u_1} [CommRing R] {M₁ : Type u_3} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_4} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h₁ : Q₁.IsGPRRegular) (h₂ : Q₂.IsGPRRegular) : IsGPRRegular (QuadraticMap.prod Q₁ Q₂)

An orthogonal sum of regular forms is regular. The polar map of q₁ ⊥ q₂ sends (x₁, x₂) to (y₁, y₂) ↦ q₁(x₁, y₁) + q₂(x₂, y₂), so it is the product of the two polar maps followed by the identification M₁* × M₂* ≃ (M₁ × M₂)*.

theorem QuadraticForm.IsGPRRegular.of_prod_left {R : Type u_1} [CommRing R] {M₁ : Type u_3} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_4} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : IsGPRRegular (QuadraticMap.prod Q₁ Q₂)) : Q₁.IsGPRRegular

The left summand of a regular orthogonal sum is regular. A preimage of f ∘ fst under the polar map of q₁ ⊥ q₂ has first component a preimage of f under the polar map of q₁.

theorem QuadraticForm.IsGPRRegular.of_prod_right {R : Type u_1} [CommRing R] {M₁ : Type u_3} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_4} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : IsGPRRegular (QuadraticMap.prod Q₁ Q₂)) : Q₂.IsGPRRegular

The right summand of a regular orthogonal sum is regular.

theorem QuadraticForm.isGPRRegular_prod_iff {R : Type u_1} [CommRing R] {M₁ : Type u_3} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_4} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} : IsGPRRegular (QuadraticMap.prod Q₁ Q₂) ↔ Q₁.IsGPRRegular ∧ Q₂.IsGPRRegular

Regularity of an orthogonal sum (GN C.8(f)): q₁ ⊥ q₂ is regular if and only if both q₁ and q₂ are. Unlike non-singularity (GN (C.8.3), QuadraticForm.IsGPRRegular.prod_isGPRNonsingular), regularity is symmetric in the two summands, and needs no finiteness or projectivity.

theorem QuadraticForm.IsGPRRegular.smul_of_isUnit {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {c : R} (hc : IsUnit c) {Q : QuadraticForm R M} (h : Q.IsGPRRegular) : (c • Q).IsGPRRegular

A unit multiple of a regular form is regular: the polar map of c q is c times the polar map of q, and multiplication by a unit is bijective on the dual.

theorem QuadraticForm.isUnit_of_isGPRRegular_smul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {c : R} {Q : QuadraticForm R M} (h : (c • Q).IsGPRRegular) {m : M} (hm : Module.IsUnimodular R m) : IsUnit c

A regular rescaled form forces the scalar to be a unit, as soon as the module has a unimodular element m: if f m = 1 and x is a preimage of f under the polar map of c q, then c · q(x, m) = 1.

The polar radical of a quadratic map

theorem QuadraticMap.mem_ker_polarBilin_iff {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {Q : QuadraticMap R M P} {z : M} : z ∈ LinearMap.ker Q.polarBilin ↔ ∀ (y : M), polar (⇑Q) z y = 0

Membership in the kernel of the polar form Q.polarBilin: n(z, y) = 0 for every y. This kernel is Rad(DQ) in GPR's notation, not the radical QuadraticMap.radical Q.

theorem QuadraticMap.map_add_of_mem_ker_polarBilin {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {Q : QuadraticMap R M P} {a : M} (ha : a ∈ LinearMap.ker Q.polarBilin) (b : M) : Q (a + b) = Q a + Q b

A quadratic map is additive in an argument from the kernel of its polar form.

theorem QuadraticMap.injOn_ker_polarBilin {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {Q : QuadraticMap R M P} (hrad : Q.radical = ⊥) : Set.InjOn ⇑Q ↑(LinearMap.ker Q.polarBilin)

If the radical of Q vanishes (GPR's non-degeneracy), then Q is injective on the kernel of its polar form. For a, b in that kernel with Q a = Q b, the difference a - b is in the kernel too, and Q (a - b) = Q a + Q b = 2 • Q a = n(a, a) = 0, so a - b is in the radical. This is the first step of GPR 19.3's treatment of the polar radical.

theorem QuadraticMap.two_smul_eq_zero_of_mem_ker_polarBilin {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {Q : QuadraticMap R M P} (hrad : Q.radical = ⊥) {z : M} (hz : z ∈ LinearMap.ker Q.polarBilin) : 2 • z = 0

2 kills the polar radical of a quadratic map with vanishing radical (the assertion 2 C⊥ = 0 of GPR 19.3): for z in the kernel of the polar form, Q (2 • z) = 2 • n(z, z) = 0, so 2 • z is in the radical. No algebra structure is involved.