Orthogonal sums and base change for quadratic forms #
This file supplies the infrastructure relating Mathlib's orthogonal sum QuadraticMap.prod
and base change QuadraticForm.baseChange:
baseChange_prod: base change commutes with the orthogonal sum.baseChange_prod_neg: the same with a negated second factor.QuadraticMap.Equivalent.nondegenerate{,_iff}: nondegeneracy is invariant under equivalence.mul_unit_isotropic_iff: isotropy is unchanged by scaling all weights by a unit.weightedSumSquares_mul_squares_equivalent: multiplying weights by squares gives an equivalent form.
The proofs mirror the reference development, adapted to Mathlib 4.33's API
(baseChange_ext on pure tensors avoids the bilinear-form machinery of the original).
Base change of an orthogonal sum #
Base change of the matrix and discriminant #
Nondegeneracy is invariant under equivalence #
Isotropy and rescaling weights #
Multiplying every weight by a fixed unit multiplies the whole form by that unit, and
multiplying weights by squares is an isometry (Mathlib's
isometryEquivWeightedSumSquaresWeightedSumSquares). Both leave isotropy unchanged.
Discriminants of weighted sums of squares #
Nondegeneracy via the discriminant #
Over a domain in which 2 is invertible, a quadratic form is nondegenerate exactly when its
discriminant (the determinant of its matrix in a basis) is nonzero. This is the standard
criterion: the radical of Q is the kernel of the associated bilinear form
(QuadraticMap.radical_eq_ker_associated), and a bilinear form over a domain is nondegenerate
iff its determinant is nonzero (LinearMap.nondegenerate_iff_det_ne_zero).
Base change preserves nondegeneracy #
baseChange_discr turns base change into the algebraMap on discriminants, and an injective
algebraMap (equivalently, FaithfulSMul R A) preserves being nonzero. Applying the
discriminant criterion nondegenerate_iff_discr_ne_zero on both sides gives the result.
The hypotheses are necessarily a little stronger than "A is nontrivial": ℚ → A is injective
for every nontrivial A, but over a general domain R this can fail (e.g. ℤ → 𝔽_p), so
injectivity is recorded as FaithfulSMul R A. The target must again be a domain (with 2
invertible) for the discriminant criterion to apply there.
Isotropy of an orthogonal sum #
The orthogonal sum Q₁.prod Q₂ evaluates to (x, y) ↦ Q₁ x + Q₂ y. It is isotropic
exactly when some summand already is, or when the two summands represent a common nonzero
value with opposite signs: a nonzero isotropic vector (x, y) with Q₁ x + Q₂ y = 0 has
Q₁ x = -Q₂ y, and the problematic case Q₁ x = Q₂ y = 0 is precisely when a summand is
isotropic. Nondegeneracy is not needed.
A common value from a signed orthogonal sum #
Over a field, isotropy together with nondegeneracy is very strong: a nondegenerate isotropic
form represents every value. Indeed, if Q x₀ = 0 with x₀ ≠ 0, nondegeneracy supplies
z with polarBilin Q x₀ z ≠ 0, and then Q (z + t • x₀) = Q z + t · polarBilin Q x₀ z
ranges over all of K as t varies.
This upgrades the "opposite signs" disjunct of prod_isotropic_iff for Q₁.prod (-Q₂): on
nontrivial spaces the two nondegenerate forms represent a common nonzero value. (The
hypotheses that the spaces are nontrivial cannot be dropped: if, say, V₂ = 0 then Q₂
represents nothing while Q₁.prod (-Q₂) ≅ Q₁ can still be isotropic.)