The radical of a quadratic form

We define the radical of a quadratic form. This is a standard construction if 2 is invertible in the coefficient ring, but is more fiddly otherwise. We follow the account in Chapter II, §7 of [EKM08].

def QuadraticMap.radical {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] (Q : QuadraticMap R M P) : Submodule R M

The radical of a quadratic form Q on M.

This is the largest submodule N such that Q lifts to a quadratic form on M ⧸ N; see Submodule.le_radical_iff for this characterization.

See also [EKM08], Chapter II, §7.

Equations

• Q.radical = { carrier := {x : M | Q x = 0 ∧ Q.polarBilin x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem QuadraticMap.mem_radical_iff' {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} {m : M} : m ∈ Q.radical ↔ Q m = 0 ∧ ∀ (n : M), Q (m + n) = Q n

@[simp]

theorem QuadraticMap.IsometryEquiv.map_radical {R : Type u_1} {M : Type u_2} {M' : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup M'] [AddCommGroup P] [CommRing R] [Module R M] [Module R M'] [Module R P] {Q : QuadraticMap R M P} {Q' : QuadraticMap R M' P} (e : Q.IsometryEquiv Q') : Submodule.map (↑e.toLinearEquiv) Q.radical = Q'.radical

The radical of a quadratic form is preserved by isometry equivalences.

theorem QuadraticMap.Equivalent.rank_radical_eq {R : Type u_1} {M : Type u_2} {M' : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup M'] [AddCommGroup P] [CommRing R] [Module R M] [Module R M'] [Module R P] {Q : QuadraticMap R M P} {Q' : QuadraticMap R M' P} (h : Q.Equivalent Q') : Module.finrank R ↥Q.radical = Module.finrank R ↥Q'.radical

The rank of the radical of a quadratic map is invariant under equivalences.

def QuadraticMap.lift {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] (Q : QuadraticMap R M P) (N : Submodule R M) (hN : N ≤ Q.radical) : QuadraticMap R (M ⧸ N) P

Lift a quadratic map on M to M ⧸ N, where N is contained in the radical.

Equations

• Q.lift N hN = { toFun := Quotient.lift ⇑Q ⋯, toFun_smul := ⋯, exists_companion' := ⋯ }

@[simp]

theorem QuadraticMap.lift_mk {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} {N : Submodule R M} (hN : N ≤ Q.radical) (m : M) : (Q.lift N hN) (Submodule.Quotient.mk m) = Q m

theorem QuadraticMap.le_radical_iff {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} {N : Submodule R M} : N ≤ Q.radical ↔ ∃ (Q' : QuadraticMap R (M ⧸ N) P), Q'.comp N.mkQ = Q

Universal property of the radical of a quadratic form: Q.radical is the largest subspace N such that Q factors through a quadratic form on M ⧸ N.

theorem QuadraticMap.radical_le_ker_polarBilin {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} : Q.radical ≤ LinearMap.ker Q.polarBilin

The radical of a quadratic map is contained in the kernel of its polar bilinear map.

See radical_eq_ker_polarBilin for the equality when 2 is invertible in the coefficient ring.

structure QuadraticMap.Nondegenerate {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} : Prop

A quadratic map is said to be nondegenerate if its radical is 0, and the radical of its associated polar form has rank ≤ 1. (The second condition is automatic if 2 is invertible in R, but not in general.)

See [EKM08], Chapter II, §7.

• radical_eq_bot : Q.radical = ⊥
• rank_rad_polar_le : Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1

theorem QuadraticMap.radical_eq_ker_polarBilin {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} [Invertible 2] : Q.radical = LinearMap.ker Q.polarBilin

If 2 is invertible in the coefficient ring, the radical of a quadratic map is the kernel of its polar bilinear map.

theorem QuadraticMap.radical_eq_ker_associated {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} [Invertible 2] : Q.radical = LinearMap.ker (associated Q)

If 2 is invertible in the coefficient ring, the radical of a quadratic map is the kernel of its associated bilinear map.

theorem QuadraticMap.nondegenerate_iff_radical_eq_bot {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} [Invertible 2] : Nondegenerate ↔ Q.radical = ⊥

If 2 is invertible in the coefficient ring, a quadratic map is nondegenerate iff its radical is 0. (Use QuadraticMap.Nondegenerate.radical_eq_bot for the one-way implication in all characteristics.)

theorem QuadraticMap.nondegenerate_associated_iff {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} [Invertible 2] : LinearMap.Nondegenerate (associated Q) ↔ Nondegenerate

If 2 is invertible in the coefficient ring, a quadratic map is nondegenerate iff its associated bilinear map is nondegenerate.

theorem QuadraticMap.nondegenerate_polar_iff {R : Type u_1} {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [CommRing R] [Module R M] [Module R P] {Q : QuadraticMap R M P} [Invertible 2] : LinearMap.Nondegenerate Q.polarBilin ↔ Nondegenerate

If 2 is invertible in the coefficient ring, a quadratic map is nondegenerate iff its polar bilinear map is nondegenerate.

theorem QuadraticForm.radical_weightedSumSquares {𝕜 : Type u_1} {ι : Type u_2} [Field 𝕜] [NeZero 2] [Fintype ι] {w : ι → 𝕜} : (QuadraticMap.weightedSumSquares 𝕜 w).radical = Pi.spanSubset 𝕜 {i : ι | w i = 0}

Over a field of characteristic different from 2, the radical of a weighted-sum-of-squares quadratic form is the number of zero weights.

theorem QuadraticForm.finrank_radical_of_equiv_weightedSumSquares {𝕜 : Type u_1} {ι : Type u_2} [Field 𝕜] [NeZero 2] [Fintype ι] {w : ι → 𝕜} {M : Type u_3} [AddCommGroup M] [Module 𝕜 M] {Q : QuadraticForm 𝕜 M} (hQ : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w)) : Module.finrank 𝕜 ↥(QuadraticMap.radical Q) = {i : ι | w i = 0}.ncard

If the quadratic form Q is equivalent to a weighted sum of squares with weights w, then the rank of Q.radical is equal to the number of zero weights.