Ternary subspaces of quaternary quadratic spaces

This file proves that, over a field in which two is invertible, a subspace of dimension at least three in a regular four-dimensional isotropic quadratic space with square discriminant is isotropic. The ambient hypotheses first force the space to be the orthogonal sum of two hyperbolic planes. Such a space has a two-dimensional totally isotropic subspace, which must meet every subspace of dimension at least three nontrivially.

The resulting equivalence between isotropy of the restricted and ambient forms is the field-theoretic step used in the square-discriminant case of the quaternary Hasse principle. It is also stated for an arbitrary form of dimension at least three represented by the ambient form, which is the version that transfers through scalar extension.

Main results

• QuadraticMap.Nondegenerate.not_anisotropic_restrict_of_finrank_ge_three: isotropy of such an ambient form implies isotropy of any restriction of dimension at least three.
• QuadraticMap.Nondegenerate.not_anisotropic_restrict_iff_of_finrank_ge_three: isotropy of a restriction of dimension at least three is equivalent to isotropy of its regular quaternary ambient form when the latter has square discriminant.
• QuadraticMap.Nondegenerate.not_anisotropic_of_isRepresentedBy_of_finrank_ge_three: the same conclusion for any form of dimension at least three represented by such an ambient form.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer, 1963, §42:12.

theorem QuadraticMap.Nondegenerate.not_anisotropic_restrict_of_finrank_ge_three {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : Nondegenerate) (U : Submodule K V) (hUrank : 3 ≤ Module.finrank K ↥U) (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0) (hiso : ¬Anisotropic Q) : ¬(restrict Q U).Anisotropic

Over a field in which two is invertible, a subspace of dimension at least three in a regular quaternary isotropic space with square discriminant is isotropic. No regularity hypothesis on the subspace is needed.

theorem QuadraticMap.Nondegenerate.not_anisotropic_restrict_iff_of_finrank_ge_three {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : Nondegenerate) (U : Submodule K V) (hUrank : 3 ≤ Module.finrank K ↥U) (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0) : ¬(restrict Q U).Anisotropic ↔ ¬Anisotropic Q

O'Meara 42:12. Over a field in which two is invertible, for a subspace of dimension at least three in a regular quaternary quadratic space with square discriminant, the restricted form is isotropic exactly when the ambient form is.

The restriction need not be assumed regular.

theorem QuadraticMap.Nondegenerate.not_anisotropic_of_isRepresentedBy_of_finrank_ge_three {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : Nondegenerate) {W : Type u_1} [AddCommGroup W] [Module K W] {R : QuadraticForm K W} (hRQ : IsRepresentedBy R Q) (hRrank : 3 ≤ Module.finrank K W) (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0) (hiso : ¬Anisotropic Q) : ¬Anisotropic R

Over a field in which two is invertible, a form of dimension at least three represented by a regular quaternary isotropic form with square discriminant is isotropic.