Layer 2a of the Hasse–Minkowski development: local isotropy

Hasse–Minkowski says that a quadratic form over ℚ is isotropic if and only if it becomes isotropic after extending scalars to every completion of ℚ, namely ℝ and the p-adic fields ℚ_[p] for all primes p. This file supplies the local side of the statement:

• EverywhereLocallyIsotropic Q: Q is isotropic over every completion.
• isotropic_everywhereLocallyIsotropic: the easy implication, by base-changing an isotropic vector along 1 ⊗ₜ x.
• baseChange_weightedSumSquares: base change commutes with the concrete form weightedSumSquares, a fact Mathlib 4.33 lacks and which the rank-two case below needs.

The tensor-product object Q.baseChange A is Mathlib's QuadraticForm.baseChange A Q, a form on A ⊗[ℚ] V.

Base change of a weighted sum of squares

Mathlib has no statement relating (weightedSumSquares R w).baseChange A to a weighted sum of squares over A. The canonical identification is A ⊗[R] (ι → R) ≃ₗ[A] (ι → A) (TensorProduct.piScalarRight), under which the two forms agree. We prove agreement by baseChange_ext, which reduces to the pure tensors 1 ⊗ₜ y.

theorem HasseMinkowski.baseChange_weightedSumSquares {R : Type u_1} {A : Type u_2} {ι : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Invertible 2] [Fintype ι] (w : ι → R) : QuadraticMap.Equivalent (QuadraticForm.baseChange A (QuadraticMap.weightedSumSquares R w)) (QuadraticMap.weightedSumSquares A fun (i : ι) => (algebraMap R A) (w i))

Base change preserves isotropy

The forward implication of Hasse–Minkowski is easy: if x ≠ 0 is isotropic for Q, then 1 ⊗ₜ x is isotropic for the base change. The only point to check is 1 ⊗ₜ x ≠ 0, which holds because a nontrivial algebra over a field is faithfully flat.

theorem HasseMinkowski.isotropic_baseChange {R : Type u_1} {A : Type u_2} {V : Type u_3} [Field R] [CommRing A] [Algebra R A] [Nontrivial A] [AddCommGroup V] [Module R V] [Invertible 2] {Q : QuadraticForm R V} (hQ : Isotropic Q) : Isotropic (QuadraticForm.baseChange A Q)

Everywhere local isotropy

def HasseMinkowski.EverywhereLocallyIsotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] (Q : QuadraticForm ℚ V) : Prop

A quadratic form over ℚ is everywhere locally isotropic if it is isotropic over every completion of ℚ: over ℝ and over every p-adic field ℚ_[p].

Equations

• One or more equations did not get rendered due to their size.

theorem HasseMinkowski.isotropic_everywhereLocallyIsotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (hQ : Isotropic Q) : EverywhereLocallyIsotropic Q

Dot-notation alias

Mirrors the aliases in Basic.lean, so that Q.EverywhereLocallyIsotropic works for a quadratic form Q.

@[reducible, inline]

abbrev HasseMinkowski.QuadraticMap.EverywhereLocallyIsotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] (Q : QuadraticForm ℚ V) : Prop

Dot-notation alias for HasseMinkowski.EverywhereLocallyIsotropic: the quadratic form is isotropic over ℝ and over every p-adic field ℚ_[p].

Equations

• HasseMinkowski.QuadraticMap.EverywhereLocallyIsotropic Q = HasseMinkowski.EverywhereLocallyIsotropic Q