The hyperbolic plane

The hyperbolic plane over a commutative ring in which two is invertible is the diagonal quadratic form ⟨1, -1⟩. It is nondegenerate, represents every scalar, and is isometric to the xy-form QuadraticForm.dualProd. Over a field in which two is invertible (that is, of characteristic not two), every plane ⟨a, -a⟩ with a ≠ 0 is isometric to it.

The main result is the hyperbolic splitting theorem: over a field of characteristic not two, every finite-dimensional nondegenerate isotropic quadratic form splits as the orthogonal sum of a hyperbolic plane and another nondegenerate form. It is the inductive step of Witt decomposition: iterating it splits off hyperbolic planes until the remaining part is anisotropic. The companion statement that such a form is universal is QuadraticMap.represents_of_nondegenerate_of_not_anisotropic, which needs no finiteness hypothesis and is proved directly in TauCeti/LinearAlgebra/QuadraticForm/Representation.lean.

Main definitions

• TauCeti.hyperbolicPlane: the diagonal form ⟨1, -1⟩, over a commutative ring in which two is invertible.
• TauCeti.hyperbolicClass: the isometry class of the hyperbolic plane.

Main results

• TauCeti.represents_hyperbolicPlane: the hyperbolic plane represents every scalar.
• TauCeti.equivalent_hyperbolicPlane_dualProd: the hyperbolic plane is isometric to the xy-form QuadraticForm.dualProd.
• TauCeti.equivalent_weightedSumSquares_hyperbolicPlane_of_isSquare: a binary diagonal form whose discriminant differs from that of the hyperbolic plane by a square is hyperbolic.
• TauCeti.equivalent_weightedSumSquares_self_neg_hyperbolicPlane: in characteristic not two, every ⟨a, -a⟩, for a ≠ 0, is hyperbolic.
• QuadraticForm.equivalent_restrict_span_pair_hyperbolicPlane: two isotropic vectors with polar pairing one span a hyperbolic plane.
• QuadraticForm.equivalent_hyperbolicPlane_prod_restrict_orthogonal, QuadraticMap.Nondegenerate.nondegenerate_restrict_orthogonal_span_pair: such a pair splits a finite-dimensional form as the orthogonal sum of its hyperbolic plane and the orthogonal complement, which is regular when the form is.
• TauCeti.exists_hyperbolicPlane_prod_equivalent: in characteristic not two, every finite-dimensional nondegenerate isotropic form splits off a hyperbolic plane.
• TauCeti.formClass_hyperbolicPlane: the regular-form class of the hyperbolic plane is TauCeti.hyperbolicClass.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter I, §3.

def TauCeti.hyperbolicPlane (R : Type u) [CommRing R] [_i2 : Invertible 2] : QuadraticForm R (Fin 2 → R)

The hyperbolic plane ⟨1, -1⟩ over a commutative ring in which two is invertible.

The invertibility hypothesis is not used by the formula; it confines the definition to the setting where the diagonal form ⟨1, -1⟩ is the hyperbolic plane. In characteristic two it is ⟨1, 1⟩, whose polar form vanishes identically.

@[simp]

theorem TauCeti.hyperbolicPlane_apply {R : Type u} [CommRing R] [Invertible 2] (x : Fin 2 → R) : (hyperbolicPlane R) x = x 0 ^ 2 - x 1 ^ 2

Evaluation of the hyperbolic plane in its diagonal coordinates.

@[simp]

theorem TauCeti.polar_hyperbolicPlane {R : Type u} [CommRing R] [Invertible 2] (x y : Fin 2 → R) : QuadraticMap.polar (⇑(hyperbolicPlane R)) x y = 2 * (x 0 * y 0 - x 1 * y 1)

The polar form of the hyperbolic plane in its diagonal coordinates.

theorem TauCeti.nondegenerate_hyperbolicPlane {R : Type u} [CommRing R] [Invertible 2] : QuadraticMap.Nondegenerate

The hyperbolic plane is nondegenerate when two is invertible.

theorem TauCeti.represents_hyperbolicPlane {R : Type u} [CommRing R] [Invertible 2] (a : R) : QuadraticMap.Represents (hyperbolicPlane R) a

When two is invertible, the hyperbolic plane represents every scalar.

theorem TauCeti.equivalent_hyperbolicPlane_dualProd {R : Type u} [CommRing R] [Invertible 2] : QuadraticMap.Equivalent (hyperbolicPlane R) (QuadraticForm.dualProd R R)

When two is invertible, the hyperbolic plane is isometric to the xy-form QuadraticForm.dualProd R R, whose value at (f, z) is f z.

theorem TauCeti.equivalent_weightedSumSquares_hyperbolicPlane_of_isSquare {K : Type u} [Field K] [Invertible 2] {a b : Kˣ} (hdisc : IsSquare (a * b * (1 * -1))) : (QuadraticMap.weightedSumSquares K ![↑a, ↑b]).Equivalent (hyperbolicPlane K)

Over a field in which two is invertible, a binary diagonal form whose discriminant differs from that of the hyperbolic plane by a square is isometric to the hyperbolic plane.

theorem TauCeti.equivalent_weightedSumSquares_self_neg_hyperbolicPlane {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : (QuadraticMap.weightedSumSquares K ![↑a, -↑a]).Equivalent (hyperbolicPlane K)

Over a field in which two is invertible, every diagonal plane ⟨a, -a⟩ with a a unit is isometric to the hyperbolic plane.

The hyperbolic class

@[simp]

theorem TauCeti.presentedForm_one_neg_one {K : Type u} [Field K] [Invertible 2] : presentedForm ⟨2, ![1, -1]⟩ = hyperbolicPlane K

The diagonal presentation ⟨1, -1⟩ presents the hyperbolic plane.

def TauCeti.hyperbolicClass (K : Type u) [Field K] [_i2 : Invertible 2] : RegularFormClass K

The isometry class of the hyperbolic plane ⟨1, -1⟩.

As with TauCeti.hyperbolicPlane, the invertibility hypothesis is not used by the formula; it confines the definition to characteristic not two, where ⟨1, -1⟩ is the hyperbolic plane.

theorem TauCeti.hyperbolicClass_def {K : Type u} [Field K] [Invertible 2] : hyperbolicClass K = ⟦⟨2, ![1, -1]⟩⟧

The defining presentation of the hyperbolic class.

@[simp]

theorem TauCeti.rank_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : (hyperbolicClass K).rank = 2

The hyperbolic class has rank two.

theorem TauCeti.rank_nsmul_hyperbolicClass {K : Type u} [Field K] [Invertible 2] (m : ℕ) : (m • hyperbolicClass K).rank = 2 * m

The sum of m hyperbolic classes has rank 2 * m.

@[simp]

theorem TauCeti.formClass_hyperbolicPlane {K : Type u} [Field K] [Invertible 2] : formClass (hyperbolicPlane K) ⋯ = hyperbolicClass K

The class of the hyperbolic plane, as a form, is the hyperbolic class.

theorem QuadraticForm.equivalent_restrict_span_pair_hyperbolicPlane {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) {x y : V} (hxQ : Q x = 0) (hyQ : Q y = 0) (hxy : QuadraticMap.polar (⇑Q) x y = 1) : (QuadraticMap.restrict Q (Submodule.span K {x, y})).Equivalent (TauCeti.hyperbolicPlane K)

Two isotropic vectors x, y with polar Q x y = 1 span a hyperbolic plane.

theorem QuadraticForm.equivalent_hyperbolicPlane_prod_restrict_orthogonal {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) {x y : V} (hxQ : Q x = 0) (hyQ : Q y = 0) (hxy : QuadraticMap.polar (⇑Q) x y = 1) : QuadraticMap.Equivalent Q (QuadraticMap.prod (TauCeti.hyperbolicPlane K) (QuadraticMap.restrict Q (LinearMap.BilinForm.orthogonal (QuadraticMap.polarBilin Q) (Submodule.span K {x, y}))))

Two isotropic vectors x, y with polar Q x y = 1 split Q as the orthogonal sum of the hyperbolic plane they span and its orthogonal complement.

theorem QuadraticMap.Nondegenerate.nondegenerate_restrict_orthogonal_span_pair {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [Invertible 2] {Q : QuadraticForm K V} (hQ : Nondegenerate) {x y : V} (hxQ : Q x = 0) (hyQ : Q y = 0) (hxy : polar (⇑Q) x y = 1) : Nondegenerate

In a regular quadratic space, the orthogonal complement of the hyperbolic plane spanned by isotropic vectors x, y with polar Q x y = 1 is regular.

theorem TauCeti.exists_hyperbolicPlane_prod_equivalent {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hiso : ¬QuadraticMap.Anisotropic Q) : ∃ (p : RegularFormPresentation K), QuadraticMap.Equivalent Q (QuadraticMap.prod (hyperbolicPlane K) (presentedForm p))

Over a field in which two is invertible, every finite-dimensional nondegenerate isotropic quadratic form splits as the orthogonal sum of a hyperbolic plane and a nondegenerate diagonal form.