Witt decomposition

Over a field in which 2 is invertible, every regular quadratic form on a finite-dimensional space is isometric to an orthogonal sum of hyperbolic planes and an anisotropic form, and both the number of planes and the anisotropic summand are determined by the isometry class. The number of planes is the Witt index and the last summand is the anisotropic part.

The existence and uniqueness statements are phrased on TauCeti.RegularFormClass K, the isometry classes of regular forms, whose addition is orthogonal sum. m hyperbolic planes are then m • hyperbolicClass K, so the decomposition reads c = m • hyperbolicClass K + a, and the invariance of the Witt index and of the anisotropic part under isometry is automatic. TauCeti.hyperbolicPresentation names the diagonal presentation ⟨1, -1, …, 1, -1⟩ realising m • hyperbolicClass K, which is what turns the statement back into an isometry of forms in QuadraticForm.exists_equivalent_hyperbolicPresentation_prod.

This file treats the regular case, which is the case the Witt ring needs. A form with a nonzero radical is the orthogonal sum of the zero form on its radical and a regular form, and its Witt decomposition follows from the regular one.

Main definitions

• TauCeti.hyperbolicPresentation: the diagonal presentation of m hyperbolic planes.
• TauCeti.RegularFormClass.Anisotropic: anisotropy of an isometry class.
• TauCeti.RegularFormClass.wittIndex: the number of hyperbolic planes in a class.
• TauCeti.RegularFormClass.anisotropicPart: the anisotropic summand of a class.

Main results

• TauCeti.RegularFormClass.anisotropic_of_rank_le_one: a regular class of rank at most one is anisotropic.
• TauCeti.exists_nsmul_hyperbolicClass_add: Witt decomposition (Lam I.4.1), existence.
• TauCeti.eq_of_nsmul_hyperbolicClass_add_eq: Witt decomposition, uniqueness of both the number of hyperbolic planes and the anisotropic summand.
• TauCeti.RegularFormClass.wittDecomposition: the decomposition of a class by its own Witt index and anisotropic part.
• TauCeti.RegularFormClass.rank_eq_two_mul_wittIndex_add: the rank formula rank c = 2 * wittIndex c + rank (anisotropicPart c).
• TauCeti.RegularFormClass.eq_hyperbolicClass_of_rank_eq_two_of_not_anisotropic: an isotropic class of rank two is the hyperbolic class.
• QuadraticForm.exists_equivalent_hyperbolicPresentation_prod: the decomposition read as an isometry of quadratic forms.
• QuadraticForm.mem_unitValueSet_iff_not_anisotropic_mk_rankOne_add: a regular form represents a unit c exactly when adjoining ⟨-c⟩ to its class gives an isotropic class.

References

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

Hyperbolic presentations and hyperbolic classes

def TauCeti.hyperbolicPresentation (K : Type u) [Field K] [_i2 : Invertible 2] : ℕ → RegularFormPresentation K

The diagonal presentation ⟨1, -1, …, 1, -1⟩ of m hyperbolic planes.

@[simp]

theorem TauCeti.fst_hyperbolicPresentation {K : Type u} [Field K] [Invertible 2] (m : ℕ) : (hyperbolicPresentation K m).fst = 2 * m

m hyperbolic planes are presented by 2 * m weights.

@[simp]

theorem TauCeti.mk_hyperbolicPresentation {K : Type u} [Field K] [Invertible 2] (m : ℕ) : ⟦hyperbolicPresentation K m⟧ = m • hyperbolicClass K

The presentation of m hyperbolic planes presents the m-fold sum of the hyperbolic class.

Anisotropic classes

def TauCeti.RegularFormClass.Anisotropic {K : Type u} [Field K] (c : RegularFormClass K) : Prop

An isometry class is anisotropic when the forms in it are: being anisotropic is an isometry invariant, by QuadraticMap.Equivalent.anisotropic_iff, so it descends to the classes.

@[simp]

theorem TauCeti.RegularFormClass.anisotropic_mk {K : Type u} [Field K] (p : RegularFormPresentation K) : Anisotropic ⟦p⟧ ↔ QuadraticMap.Anisotropic (presentedForm p)

A class is anisotropic exactly when one, equivalently every, presented form in it is.

@[simp]

theorem TauCeti.RegularFormClass.anisotropic_zero {K : Type u} [Field K] : Anisotropic 0

The rank-zero class is anisotropic: its space has no nonzero vector.

theorem TauCeti.RegularFormClass.anisotropic_of_rank_le_one {K : Type u} [Field K] {x : RegularFormClass K} (hx : x.rank ≤ 1) : x.Anisotropic

A regular-form class of rank at most one is anisotropic: a form ⟨a⟩ with a a unit vanishes only at the origin.

theorem QuadraticForm.not_anisotropic_hyperbolicPlane_prod {K : Type u} [Field K] [Invertible 2] {W : Type v} [AddCommGroup W] [Module K W] (R : QuadraticForm K W) : ¬(QuadraticMap.prod (TauCeti.hyperbolicPlane K) R).Anisotropic

A hyperbolic plane is isotropic, so an orthogonal sum with one is never anisotropic.

@[simp]

theorem TauCeti.not_anisotropic_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : ¬(hyperbolicClass K + c).Anisotropic

A class with a hyperbolic summand is not anisotropic.

theorem TauCeti.not_anisotropic_succ_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (m : ℕ) (c : RegularFormClass K) : ¬((m + 1) • hyperbolicClass K + c).Anisotropic

A class with at least one hyperbolic plane split off is not anisotropic.

The decomposition

theorem TauCeti.exists_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : ∃ (m : ℕ) (a : RegularFormClass K), a.Anisotropic ∧ c = m • hyperbolicClass K + a

Witt decomposition (Lam I.4.1), existence: every isometry class of regular forms is the orthogonal sum of a number of hyperbolic planes and an anisotropic class.

theorem TauCeti.eq_of_nsmul_hyperbolicClass_add_eq {K : Type u} [Field K] [Invertible 2] {m m' : ℕ} {a a' : RegularFormClass K} (ha : a.Anisotropic) (ha' : a'.Anisotropic) (h : m • hyperbolicClass K + a = m' • hyperbolicClass K + a') : m = m' ∧ a = a'

Witt decomposition (Lam I.4.1), uniqueness: the number of hyperbolic planes and the anisotropic summand are determined by the class.

noncomputable def TauCeti.RegularFormClass.wittIndex {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : ℕ

The Witt index of an isometry class of regular forms: the number of hyperbolic planes in its Witt decomposition.

noncomputable def TauCeti.RegularFormClass.anisotropicPart {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : RegularFormClass K

The anisotropic part of an isometry class of regular forms: the anisotropic summand of its Witt decomposition.

@[simp]

theorem TauCeti.RegularFormClass.anisotropic_anisotropicPart {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : c.anisotropicPart.Anisotropic

The anisotropic part of a class is anisotropic.

theorem TauCeti.RegularFormClass.wittDecomposition {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : c = c.wittIndex • hyperbolicClass K + c.anisotropicPart

Witt decomposition: a class is its Witt index worth of hyperbolic planes plus its anisotropic part.

theorem TauCeti.RegularFormClass.wittIndex_eq {K : Type u} [Field K] [Invertible 2] {c a : RegularFormClass K} {m : ℕ} (ha : a.Anisotropic) (h : c = m • hyperbolicClass K + a) : c.wittIndex = m

Any Witt decomposition of a class computes its Witt index.

theorem TauCeti.RegularFormClass.anisotropicPart_eq {K : Type u} [Field K] [Invertible 2] {c a : RegularFormClass K} {m : ℕ} (ha : a.Anisotropic) (h : c = m • hyperbolicClass K + a) : c.anisotropicPart = a

Any Witt decomposition of a class computes its anisotropic part.

theorem TauCeti.RegularFormClass.wittIndex_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (m : ℕ) (c : RegularFormClass K) : (m • hyperbolicClass K + c).wittIndex = m + c.wittIndex

Adjoining m hyperbolic planes raises the Witt index by m.

theorem TauCeti.RegularFormClass.anisotropicPart_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (m : ℕ) (c : RegularFormClass K) : (m • hyperbolicClass K + c).anisotropicPart = c.anisotropicPart

Adjoining hyperbolic planes leaves the anisotropic part unchanged.

@[simp]

theorem TauCeti.RegularFormClass.wittIndex_zero {K : Type u} [Field K] [Invertible 2] : wittIndex 0 = 0

The rank-zero class has Witt index zero.

@[simp]

theorem TauCeti.RegularFormClass.wittIndex_eq_zero_iff {K : Type u} [Field K] [Invertible 2] {c : RegularFormClass K} : c.wittIndex = 0 ↔ c.Anisotropic

An anisotropic class has Witt index zero, and conversely.

@[simp]

theorem TauCeti.RegularFormClass.anisotropicPart_eq_self {K : Type u} [Field K] [Invertible 2] {c : RegularFormClass K} (hc : c.Anisotropic) : c.anisotropicPart = c

An anisotropic class is its own anisotropic part.

@[simp]

theorem TauCeti.RegularFormClass.wittIndex_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : (hyperbolicClass K).wittIndex = 1

The hyperbolic plane has Witt index one.

@[simp]

theorem TauCeti.RegularFormClass.anisotropicPart_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : (hyperbolicClass K).anisotropicPart = 0

The hyperbolic plane has no anisotropic part.

theorem TauCeti.RegularFormClass.rank_eq_two_mul_wittIndex_add {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : c.rank = 2 * c.wittIndex + c.anisotropicPart.rank

The rank of a class splits as twice its Witt index plus the rank of its anisotropic part.

theorem TauCeti.RegularFormClass.two_mul_wittIndex_le_rank {K : Type u} [Field K] [Invertible 2] (c : RegularFormClass K) : 2 * c.wittIndex ≤ c.rank

Twice the Witt index is at most the rank.

theorem TauCeti.RegularFormClass.eq_hyperbolicClass_of_rank_eq_two_of_not_anisotropic {K : Type u} [Field K] [Invertible 2] {c : RegularFormClass K} (hc : c.rank = 2) (h : ¬c.Anisotropic) : c = hyperbolicClass K

An isotropic class of rank two is the hyperbolic class.

The decomposition of a form

@[simp]

theorem QuadraticForm.anisotropic_formClass {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (TauCeti.formClass Q hQ).Anisotropic ↔ QuadraticMap.Anisotropic Q

A regular form is anisotropic exactly when its isometry class is.

theorem QuadraticForm.mem_unitValueSet_iff_not_anisotropic_mk_rankOne_add {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (c : Kˣ) : c ∈ QuadraticMap.unitValueSet Q ↔ ¬TauCeti.RegularFormClass.Anisotropic (⟦⟨1, fun (x : Fin 1) => -c⟩⟧ + TauCeti.formClass Q hQ)

A regular form represents a unit c exactly when adjoining the line ⟨-c⟩ to its isometry class gives an isotropic class. This reduces questions about represented values to the isotropy criteria, which are stated in terms of the invariants of a class.

theorem QuadraticForm.exists_equivalent_hyperbolicPresentation_prod {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : ∃ (p : TauCeti.RegularFormPresentation K), QuadraticMap.Anisotropic (TauCeti.presentedForm p) ∧ Module.finrank K V = 2 * (TauCeti.formClass Q hQ).wittIndex + p.fst ∧ QuadraticMap.Equivalent Q (QuadraticMap.prod (TauCeti.presentedForm (TauCeti.hyperbolicPresentation K (TauCeti.formClass Q hQ).wittIndex)) (TauCeti.presentedForm p))

Witt decomposition for a regular form: a nondegenerate quadratic form on a finite-dimensional space is isometric to the orthogonal sum of m hyperbolic planes and an anisotropic diagonal form, and m is the Witt index of its class.

Worked examples

theorem TauCeti.anisotropic_presentedForm_one_one : QuadraticMap.Anisotropic (presentedForm ⟨2, ![1, 1]⟩)

Worked example. The binary form ⟨1, 1⟩ over ℚ is anisotropic, because a sum of two rational squares vanishes only at the origin.