Approximating a global value of one summand of an orthogonal sum

Let U and W be quadratic forms over a number field K, with W regular. Suppose that W is anisotropic at only finitely many finite places, and that at every finite or real place v where W_v is anisotropic there are local vectors x_v of U_v and y_v of W_v with U(x_v) = -W(y_v) ≠ 0. Then there is one global vector x of U such that b := U(x) is nonzero and -b is represented by W at every finite and real place.

The vector x is produced by weak approximation of vectors: near each x_v the value of U stays in the square class of U(x_v), so -b differs from the local value W(y_v) by a square. At the remaining places W_v is regular and isotropic, hence universal. The scalar b is defined as the value of the approximating vector; it is not approximated directly. Consequently b is represented by U over K by construction, which is what makes the argument close up: if W satisfies the local-global principle for the representation of nonzero scalars, then -b is represented by W over K, and the two global vectors give a nonzero isotropic vector of U ⊥ W.

This is the inductive step of the Hasse–Minkowski theorem in rank at least five, where U is a binary summand and W its complement of rank at least three.

Main results

• QuadraticForm.exists_apply_ne_zero_locallyRepresentsScalar_neg: a global vector x with U x ≠ 0 whose negated value is locally represented by W.
• QuadraticForm.not_anisotropic_prod_of_forall_represents: if W satisfies the local-global principle for representing nonzero scalars, then U ⊥ W is isotropic over K.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1973), 66:1, the case of dimension at least five.

theorem QuadraticForm.exists_apply_ne_zero_locallyRepresentsScalar_neg {K : Type u_1} {X : Type u_2} {Y : Type u_3} [Field K] [NumberField K] [AddCommGroup X] [Module K X] [FiniteDimensional K X] [AddCommGroup Y] [Module K Y] [FiniteDimensional K Y] (U : QuadraticForm K X) (W : QuadraticForm K Y) (hU : U ≠ 0) (hW : QuadraticMap.Nondegenerate) (hfin : {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | QuadraticMap.Anisotropic (W.atFinitePlace v)}.Finite) (hfinite : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Anisotropic (W.atFinitePlace v) → ∃ (x : v.FiniteScalarExtension) (y : v.FiniteScalarExtension), (U.atFinitePlace v) x ≠ 0 ∧ (U.atFinitePlace v) x = -(W.atFinitePlace v) y) (hreal : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Anisotropic (W.atRealPlace w) → ∃ (x : TauCeti.RealScalarExtension w) (y : TauCeti.RealScalarExtension w), (U.atRealPlace w) x ≠ 0 ∧ (U.atRealPlace w) x = -(W.atRealPlace w) y) : ∃ (x : X), U x ≠ 0 ∧ W.LocallyRepresentsScalar (-U x)

Let W be a regular quadratic form over a number field that is anisotropic at only finitely many finite places. If at every finite or real place where W is anisotropic some nonzero local value of U is the negative of a local value of W, then there is a global vector x with U x ≠ 0 such that -U x is represented by W at every finite and real place.

theorem QuadraticForm.not_anisotropic_prod_of_forall_represents {K : Type u_1} {X : Type u_2} {Y : Type u_3} [Field K] [NumberField K] [AddCommGroup X] [Module K X] [FiniteDimensional K X] [AddCommGroup Y] [Module K Y] [FiniteDimensional K Y] (U : QuadraticForm K X) (W : QuadraticForm K Y) (hU : U ≠ 0) (hW : QuadraticMap.Nondegenerate) (hfin : {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | QuadraticMap.Anisotropic (W.atFinitePlace v)}.Finite) (hfinite : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Anisotropic (W.atFinitePlace v) → ∃ (x : v.FiniteScalarExtension) (y : v.FiniteScalarExtension), (U.atFinitePlace v) x ≠ 0 ∧ (U.atFinitePlace v) x = -(W.atFinitePlace v) y) (hreal : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Anisotropic (W.atRealPlace w) → ∃ (x : TauCeti.RealScalarExtension w) (y : TauCeti.RealScalarExtension w), (U.atRealPlace w) x ≠ 0 ∧ (U.atRealPlace w) x = -(W.atRealPlace w) y) (hlocal : ∀ (b : K), b ≠ 0 → W.LocallyRepresentsScalar b → QuadraticMap.Represents W b) : ¬(QuadraticMap.prod U W).Anisotropic

Let W be a regular quadratic form over a number field that is anisotropic at only finitely many finite places, and suppose that at every finite or real place where W is anisotropic some nonzero local value of U is the negative of a local value of W. If W represents over K every nonzero scalar that it represents at every finite and real place, then the orthogonal sum U ⊥ W is isotropic over K.