Quaternary quadratic forms #
This file develops basic results about four-dimensional quadratic forms over fields in which two is invertible.
Main results #
QuadraticMap.Nondegenerate.equivalent_hyperbolicPlane_prod_self: a regular isotropic quaternary form with square discriminant is the orthogonal sum of two hyperbolic planes.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, Springer, 1963, §42:12.
theorem
QuadraticMap.Nondegenerate.equivalent_hyperbolicPlane_prod_self
{K : Type u}
[Field K]
[Invertible 2]
{V : Type v}
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
{Q : QuadraticForm K V}
(hQ : Nondegenerate)
(hrank : Module.finrank K V = 4)
(hdiscr : (TauCeti.formClass Q hQ).discr = 0)
(hiso : ¬Anisotropic Q)
:
Over a field in which two is invertible, a regular isotropic quaternary form with square discriminant is isometric to the orthogonal sum of two hyperbolic planes.