Common local values of the summands of a non-anisotropic orthogonal sum

Let U and W be quadratic forms over a number field. If U ⊥ W is not anisotropic at a finite or real place, with U regular and W anisotropic on a nonzero space at that place, this file produces local vectors x of U and y of W with

U(x) = -W(y) ≠ 0.

These are the local values that a global vector of U has to approximate in the proof of the Hasse–Minkowski theorem in rank at least five, where U is a binary summand and W is its (regular) orthogonal complement: at the places where the regular form W stays isotropic every nonzero scalar is already represented by W, so only the places where W is anisotropic impose a condition. The results of this file do not assume W regular.

Main results

• QuadraticForm.exists_atFinitePlace_ne_zero_eq_neg
• QuadraticForm.exists_atRealPlace_ne_zero_eq_neg

References

• O. T. O'Meara, Introduction to Quadratic Forms, 66:1.

theorem QuadraticForm.exists_atFinitePlace_ne_zero_eq_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [Nontrivial W] {U : QuadraticForm K V} {R : QuadraticForm K W} [NumberField K] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h : ¬QuadraticMap.Anisotropic (atFinitePlace (QuadraticMap.prod U R) v)) (hU : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Anisotropic (R.atFinitePlace v)) : ∃ (x : v.FiniteScalarExtension) (y : v.FiniteScalarExtension), (U.atFinitePlace v) x ≠ 0 ∧ (U.atFinitePlace v) x = -(R.atFinitePlace v) y

If U ⊥ R is not anisotropic at a finite place where R is anisotropic, with U regular and R on a nonzero space, then some nonzero local value of U is the negative of a local value of R.

theorem QuadraticForm.exists_atRealPlace_ne_zero_eq_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [Nontrivial W] {U : QuadraticForm K V} {R : QuadraticForm K W} {w : { w : NumberField.InfinitePlace K // w.IsReal }} (h : ¬QuadraticMap.Anisotropic (atRealPlace (QuadraticMap.prod U R) w)) (hU : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Anisotropic (R.atRealPlace w)) : ∃ (x : TauCeti.RealScalarExtension w) (y : TauCeti.RealScalarExtension w), (U.atRealPlace w) x ≠ 0 ∧ (U.atRealPlace w) x = -(R.atRealPlace w) y

If U ⊥ R is not anisotropic at a real place where R is anisotropic, with U regular and R on a nonzero space, then some nonzero local value of U is the negative of a local value of R.