Isometry classes of regular quadratic forms

Over a field in which 2 is invertible, every nondegenerate quadratic form on a finite-dimensional space is isometric to a weighted sum of squares whose weights are units. This file turns that diagonalization into a carrier for the isometry classes themselves: a diagonal presentation is a rank n together with a tuple w : Fin n → Kˣ, presenting the form ⟨w 0, …, w (n - 1)⟩, and TauCeti.RegularFormClass K is the quotient of the presentations by isometry of the forms they present.

Presenting classes by tuples of units, rather than by quotienting quadratic forms on arbitrary finite-dimensional spaces, keeps the carrier in a single universe and makes the type a plain Quotient of a sigma type. Mathlib's QuadraticMap.Equivalent already compares forms living on different spaces, so nothing is lost: two regular forms are isometric exactly when their classes agree, and only presentations of equal rank are ever related.

Concatenating weight tuples presents the orthogonal sum of the presented forms, which makes the classes an additive commutative monoid whose zero is the class of the empty presentation and whose rank is additive.

Main definitions

• TauCeti.RegularFormPresentation: a rank together with a tuple of unit weights.
• TauCeti.presentedForm: the weighted sum of squares a presentation stands for.
• TauCeti.RegularFormClass: isometry classes of regular finite-dimensional quadratic forms.
• TauCeti.RegularFormClass.rank: the common rank of the presentations in a class.
• TauCeti.RegularFormPresentation.append: concatenation of presentations.
• TauCeti.formClass: the class of a regular form on a finite-dimensional space.

Main results

• TauCeti.RegularFormPresentation.ext: presentations with the same rank and weights agree.
• TauCeti.nondegenerate_presentedForm: a presented form is nondegenerate.
• QuadraticForm.orthogonalPairIsometryEquiv: two orthogonal anisotropic vectors identify their span with the corresponding diagonal plane.
• TauCeti.exists_presentedForm_equivalent: every regular form has a diagonal presentation.
• TauCeti.formClass_mk: the class of a form is computed by any of its diagonalizations.
• TauCeti.formClass_eq_iff: two regular forms are isometric exactly when their classes agree.
• TauCeti.formClass_eq_zero_iff: a regular form has zero class exactly when its space has dimension zero.
• TauCeti.formClass_lift_radical_eq_of_equivalent: equivalent forms have equal regular quotient classes.
• TauCeti.formClass_lift_radical_eq: a zero-plus-regular splitting computes the regular quotient class.
• TauCeti.RegularFormPresentation.prod_append: concatenation multiplies the weight products.
• TauCeti.presentedFormAppendIsometryEquiv: concatenating weights presents the orthogonal sum.
• TauCeti.presentedFormConsIsometryEquiv: peeling the first weight off presents the form as a line orthogonal to the presentation of the remaining weights.
• TauCeti.presentedForm_tail_isRepresentedBy: the tail of a diagonal presentation is represented by the full form.
• TauCeti.formClass_prod: the class of an orthogonal product is the sum of the classes.
• TauCeti.RegularFormClass.mk_succ_eq_mk_rankOne_add: the class of a presentation of positive rank is the rank-one class of its first weight plus the class of the remaining weights.
• TauCeti.RegularFormClass.induction_on_rankOne: every class is a sum of rank-one classes.
• TauCeti.RegularFormClass.exists_eq_add_mk_rankOne and TauCeti.RegularFormClass.exists_eq_mk_binary_add: a class of positive rank splits off a line, and one of rank at least two splits off a binary plane.

References

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

Diagonal presentations

@[reducible, inline]

abbrev TauCeti.RegularFormPresentation (K : Type u) [Field K] : Type u

A diagonal presentation: a rank n together with a tuple of units, read as the diagonal form ⟨w 0, …, w (n - 1)⟩. The presented form is regular when 2 is invertible in K (TauCeti.nondegenerate_presentedForm); in characteristic two its polar form vanishes, so it need not be nondegenerate.

theorem TauCeti.RegularFormPresentation.ext {K : Type u} [Field K] {p q : RegularFormPresentation K} (hrank : p.fst = q.fst) (hweight : ∀ (i : Fin p.fst), p.snd i = q.snd (Fin.cast hrank i)) : p = q

Two presentations agree as soon as they have the same rank and, at every index read through that identification, the same weight.

def TauCeti.presentedForm {K : Type u} [Field K] (p : RegularFormPresentation K) : QuadraticForm K (Fin p.fst → K)

The form presented by (n, w), namely the weighted sum of squares with weights w.

@[simp]

theorem TauCeti.presentedForm_apply {K : Type u} [Field K] (p : RegularFormPresentation K) (x : Fin p.fst → K) : (presentedForm p) x = ∑ i : Fin p.fst, ↑(p.snd i) * (x i * x i)

The presented form evaluates as the weighted sum of the squares of the coordinates.

theorem TauCeti.presentedForm_eq_weightedSumSquares {K : Type u} [Field K] (p : RegularFormPresentation K) : presentedForm p = QuadraticMap.weightedSumSquares K p.snd

The presented form is Mathlib's weighted sum of squares taken with the Kˣ-action, which is the shape produced by QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'.

theorem TauCeti.presentedForm_eq_weightedSumSquares_coe {K : Type u} [Field K] {n : ℕ} (w : Fin n → Kˣ) : presentedForm ⟨n, w⟩ = QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(w i)

A presented form is the scalar-coefficient weighted sum of squares obtained by coercing its unit weights to the base field.

theorem TauCeti.presentedForm_two {K : Type u} [Field K] (w : Fin 2 → Kˣ) : presentedForm ⟨2, w⟩ = QuadraticMap.weightedSumSquares K ![↑(w 0), ↑(w 1)]

A binary presented form ⟨w₀, w₁⟩ is the weighted sum of squares with the two coerced weights w₀, w₁, which is the shape in which the binary value and classification criteria are stated.

theorem TauCeti.nondegenerate_presentedForm {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : QuadraticMap.Nondegenerate

A presented form is regular: all its weights are units, so its radical vanishes.

noncomputable def QuadraticForm.orthogonalPairIsometryEquiv {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) {x y : V} (a b : Kˣ) (hx : Q x = ↑a) (hy : Q y = ↑b) (hxy : QuadraticMap.polar (⇑Q) x y = 0) : QuadraticMap.IsometryEquiv (TauCeti.presentedForm ⟨2, ![a, b]⟩) (QuadraticMap.restrict Q (Fintype.linearCombination K ![x, y]).range)

Two orthogonal anisotropic vectors span a copy of the diagonal plane ⟨Q x, Q y⟩.

The carrier

@[instance_reducible]

instance TauCeti.regularFormSetoid (K : Type u) [Field K] : Setoid (RegularFormPresentation K)

Two presentations are related when the forms they present are isometric. Mathlib's QuadraticMap.Equivalent already compares forms on different spaces, so presentations of different ranks may be compared; TauCeti.fst_eq_of_presentedForm_equivalent shows that only presentations of equal rank are ever related.

@[simp]

theorem TauCeti.regularFormSetoid_iff {K : Type u} [Field K] {p q : RegularFormPresentation K} : p ≈ q ↔ QuadraticMap.Equivalent (presentedForm p) (presentedForm q)

The relation defining the setoid, unfolded.

@[reducible, inline]

abbrev TauCeti.RegularFormClass (K : Type u) [Field K] : Type u

Isometry classes of diagonal presentations. When 2 is invertible in K every presented form is regular and every regular form on a finite-dimensional space is presented, so this is exactly the set of isometry classes of regular finite-dimensional quadratic forms; over a field of characteristic two it is only the quotient of the diagonal presentations by isometry.

@[simp]

theorem TauCeti.RegularFormClass.mk_eq_mk_iff {K : Type u} [Field K] {p q : RegularFormPresentation K} : ⟦p⟧ = ⟦q⟧ ↔ QuadraticMap.Equivalent (presentedForm p) (presentedForm q)

Two presentations have the same class exactly when they present isometric forms.

theorem TauCeti.fst_eq_of_presentedForm_equivalent {K : Type u} [Field K] {p q : RegularFormPresentation K} (h : QuadraticMap.Equivalent (presentedForm p) (presentedForm q)) : p.fst = q.fst

Isometric presented forms have the same number of weights, because an isometry is in particular a linear equivalence of the underlying coordinate spaces.

def TauCeti.RegularFormClass.rank {K : Type u} [Field K] : RegularFormClass K → ℕ

The rank of an isometry class.

@[simp]

theorem TauCeti.RegularFormClass.rank_mk {K : Type u} [Field K] (p : RegularFormPresentation K) : rank ⟦p⟧ = p.fst

The rank of the class of a presentation is the length of its weight tuple.

The orthogonal sum

def TauCeti.RegularFormPresentation.append {K : Type u} [Field K] (p q : RegularFormPresentation K) : RegularFormPresentation K

The orthogonal sum of two diagonal presentations, obtained by concatenating the two weight tuples.

@[simp]

theorem TauCeti.RegularFormPresentation.fst_append {K : Type u} [Field K] (p q : RegularFormPresentation K) : (p.append q).fst = p.fst + q.fst

Concatenation adds the two ranks.

@[simp]

theorem TauCeti.RegularFormPresentation.append_apply_castAdd {K : Type u} [Field K] (p q : RegularFormPresentation K) (i : Fin p.fst) : (p.append q).snd (Fin.cast ⋯ (Fin.castAdd q.fst i)) = p.snd i

Concatenation restricts to the first tuple on the initial coordinates.

@[simp]

theorem TauCeti.RegularFormPresentation.append_apply_natAdd {K : Type u} [Field K] (p q : RegularFormPresentation K) (j : Fin q.fst) : (p.append q).snd (Fin.cast ⋯ (Fin.natAdd p.fst j)) = q.snd j

Concatenation restricts to the second tuple on the final coordinates.

theorem TauCeti.RegularFormPresentation.append_def {K : Type u} [Field K] (p q : RegularFormPresentation K) : p.append q = ⟨p.fst + q.fst, Fin.append p.snd q.snd⟩

Appending presentations concatenates their weight tuples.

theorem TauCeti.RegularFormPresentation.prod_append {K : Type u} [Field K] (p q : RegularFormPresentation K) : ∏ i : Fin (p.append q).fst, (p.append q).snd i = (∏ i : Fin p.fst, p.snd i) * ∏ j : Fin q.fst, q.snd j

The weight product of a concatenation is the product of the two weight products.

def TauCeti.presentedFormAppendIsometryEquiv {K : Type u} [Field K] (p q : RegularFormPresentation K) : QuadraticMap.IsometryEquiv (presentedForm (p.append q)) (QuadraticMap.prod (presentedForm p) (presentedForm q))

Concatenating the weight tuples presents the orthogonal sum of the two presented forms.

@[simp]

theorem TauCeti.presentedFormAppendIsometryEquiv_apply {K : Type u} [Field K] (p q : RegularFormPresentation K) (x : Fin (p.append q).fst → K) : (presentedFormAppendIsometryEquiv p q) x = (fun (i : Fin p.fst) => x (Fin.cast ⋯ (Fin.castAdd q.fst i)), fun (j : Fin q.fst) => x (Fin.cast ⋯ (Fin.natAdd p.fst j)))

The forward map of TauCeti.presentedFormAppendIsometryEquiv splits the coordinates into the two concatenated halves.

@[simp]

theorem TauCeti.presentedFormAppendIsometryEquiv_symm_apply {K : Type u} [Field K] (p q : RegularFormPresentation K) (x : (Fin p.fst → K) × (Fin q.fst → K)) : (presentedFormAppendIsometryEquiv p q).invFun x = Fin.append x.1 x.2 ∘ Fin.cast ⋯

The inverse map of TauCeti.presentedFormAppendIsometryEquiv concatenates the two coordinate tuples.

theorem TauCeti.equivalent_presentedForm_append_prod {K : Type u} [Field K] (p q : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (p.append q)) (QuadraticMap.prod (presentedForm p) (presentedForm q))

The form presented by a concatenation is isometric to the orthogonal sum of the two presented forms.

theorem TauCeti.RegularFormPresentation.append_castAdd_natAdd {K : Type u} [Field K] {m n : ℕ} (w : Fin (m + n) → Kˣ) : append ⟨m, fun (i : Fin m) => w (Fin.castAdd n i)⟩ ⟨n, fun (i : Fin n) => w (Fin.natAdd m i)⟩ = ⟨m + n, w⟩

A presentation of rank m + n is the concatenation of its first m and its last n weights.

theorem TauCeti.equivalent_presentedForm_prod_castAdd_natAdd {K : Type u} [Field K] {m n : ℕ} (w : Fin (m + n) → Kˣ) : QuadraticMap.Equivalent (presentedForm ⟨m + n, w⟩) (QuadraticMap.prod (presentedForm ⟨m, fun (i : Fin m) => w (Fin.castAdd n i)⟩) (presentedForm ⟨n, fun (i : Fin n) => w (Fin.natAdd m i)⟩))

The form presented by m + n weights is isometric to the orthogonal sum of the forms presented by its first m and by its last n weights.

def TauCeti.presentedFormConsIsometryEquiv {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 1) → Kˣ) : ((↑(w 0) • QuadraticMap.sq).prod (presentedForm ⟨n, fun (i : Fin n) => w i.succ⟩)).IsometryEquiv (presentedForm ⟨n + 1, w⟩)

Peeling the first weight off a presentation of positive rank exhibits the presented form as the orthogonal sum of the line ⟨w 0⟩ and the presentation of the remaining weights: ⟨w 0⟩ ⊥ ⟨w 1, …, w n⟩ ≅ ⟨w 0, …, w n⟩. The first factor is carried by K itself rather than by Fin 1 → K, which is what makes it a line spanned by 1.

theorem TauCeti.presentedForm_tail_isRepresentedBy {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 1) → Kˣ) : QuadraticMap.IsRepresentedBy (presentedForm ⟨n, fun (i : Fin n) => w i.succ⟩) (presentedForm ⟨n + 1, w⟩)

The tail of a diagonal presentation is represented by the full presented form.

theorem TauCeti.not_anisotropic_presentedForm_succ_iff {K : Type u} [Field K] [Invertible 2] {n : ℕ} (w : Fin (n + 1) → Kˣ) : ¬QuadraticMap.Anisotropic (presentedForm ⟨n + 1, w⟩) ↔ -w 0 ∈ QuadraticMap.unitValueSet (presentedForm ⟨n, fun (i : Fin n) => w i.succ⟩)

A diagonal form ⟨w₀, w₁, …, wₙ⟩ is isotropic exactly when ⟨w₁, …, wₙ⟩ represents -w₀.

theorem TauCeti.not_anisotropic_presentedForm_two_add_iff {K : Type u} [Field K] [Invertible 2] {n : ℕ} [NeZero n] (w : Fin (2 + n) → Kˣ) : ¬QuadraticMap.Anisotropic (presentedForm ⟨2 + n, w⟩) ↔ ∃ x ∈ (QuadraticMap.weightedSumSquares K ![↑(w 0), ↑(w 1)]).unitValueSet, -x ∈ QuadraticMap.unitValueSet (presentedForm ⟨n, fun (i : Fin n) => w (Fin.natAdd 2 i)⟩)

A diagonal form ⟨w₀, w₁, w₂, …⟩ of rank 2 + n with n ≠ 0 is isotropic exactly when some unit value x of its binary head ⟨w₀, w₁⟩ has -x a value of its tail ⟨w₂, …⟩. The head is stated as a weighted sum of squares, the shape in which the binary value criteria are stated.

@[simp]

theorem TauCeti.presentedFormConsIsometryEquiv_apply {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 1) → Kˣ) (x : K × (Fin n → K)) : (presentedFormConsIsometryEquiv w) x = Fin.cons x.1 x.2

The forward map of TauCeti.presentedFormConsIsometryEquiv prepends the line coordinate.

@[simp]

theorem TauCeti.presentedFormConsIsometryEquiv_symm_apply {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 1) → Kˣ) (x : Fin (n + 1) → K) : (presentedFormConsIsometryEquiv w).symm x = (x 0, Fin.tail x)

The inverse map of TauCeti.presentedFormConsIsometryEquiv separates the first coordinate from the remaining coordinates.

theorem TauCeti.presentedForm_append_congr {K : Type u} [Field K] {p p' q q' : RegularFormPresentation K} (hp : QuadraticMap.Equivalent (presentedForm p) (presentedForm p')) (hq : QuadraticMap.Equivalent (presentedForm q) (presentedForm q')) : QuadraticMap.Equivalent (presentedForm (p.append q)) (presentedForm (p'.append q'))

Concatenation of presentations respects isometry in each argument.

theorem TauCeti.presentedForm_append_comm {K : Type u} [Field K] (p q : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (p.append q)) (presentedForm (q.append p))

Concatenation of presentations is commutative up to isometry.

theorem TauCeti.presentedForm_append_assoc {K : Type u} [Field K] (p q r : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm ((p.append q).append r)) (presentedForm (p.append (q.append r)))

Concatenation of presentations is associative up to isometry.

theorem TauCeti.presentedForm_nil_append {K : Type u} [Field K] (w : Fin 0 → Kˣ) (q : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (RegularFormPresentation.append ⟨0, w⟩ q)) (presentedForm q)

Prepending an empty presentation does not change the form up to isometry.

@[instance_reducible]

instance TauCeti.instAddRegularFormClass {K : Type u} [Field K] : Add (RegularFormClass K)

Orthogonal sum of isometry classes.

@[instance_reducible]

instance TauCeti.instZeroRegularFormClass {K : Type u} [Field K] : Zero (RegularFormClass K)

The class of the rank-zero form.

@[simp]

theorem TauCeti.RegularFormClass.mk_add_mk {K : Type u} [Field K] (p q : RegularFormPresentation K) : ⟦p⟧ + ⟦q⟧ = ⟦p.append q⟧

The sum of two classes is the class of the concatenated presentation.

theorem TauCeti.RegularFormClass.zero_def {K : Type u} [Field K] : 0 = ⟦⟨0, Fin.elim0⟩⟧

The zero class is the class of the empty presentation.

@[instance_reducible]

instance TauCeti.instAddCommMonoidRegularFormClass {K : Type u} [Field K] : AddCommMonoid (RegularFormClass K)

Orthogonal sum makes the isometry classes a commutative monoid. This is the additive half of the semiring structure that carries the Witt-Grothendieck ring.

@[simp]

theorem TauCeti.RegularFormClass.rank_add {K : Type u} [Field K] (x y : RegularFormClass K) : (x + y).rank = x.rank + y.rank

Rank is additive on orthogonal sums.

@[simp]

theorem TauCeti.RegularFormClass.rank_zero {K : Type u} [Field K] : rank 0 = 0

The zero class has rank zero.

theorem TauCeti.RegularFormClass.rank_nsmul {K : Type u} [Field K] (n : ℕ) (x : RegularFormClass K) : (n • x).rank = n * x.rank

The orthogonal sum of n copies of a class has n times its rank.

@[simp]

theorem TauCeti.RegularFormClass.rank_eq_zero_iff {K : Type u} [Field K] {x : RegularFormClass K} : x.rank = 0 ↔ x = 0

A regular-form class has rank zero exactly when it is the zero class.

Induction on the rank

theorem TauCeti.RegularFormClass.mk_succ_eq_mk_rankOne_add {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 1) → Kˣ) : ⟦⟨n + 1, w⟩⟧ = ⟦⟨1, fun (x : Fin 1) => w 0⟩⟧ + ⟦⟨n, fun (i : Fin n) => w i.succ⟩⟧

Peeling the first weight off a presentation of positive rank splits its class as the rank-one class ⟨w 0⟩ plus the class of the remaining weights.

theorem TauCeti.RegularFormClass.induction_on_rankOne {K : Type u} [Field K] {motive : RegularFormClass K → Prop} (x : RegularFormClass K) (zero : motive 0) (add_rankOne : ∀ (y : RegularFormClass K) (a : Kˣ), motive y → motive (y + ⟦⟨1, fun (x : Fin 1) => a⟩⟧)) : motive x

Every isometry class of regular forms is built from the zero class by adjoining rank-one classes one at a time. This is the induction principle behind every statement proved by diagonalizing and working one weight at a time.

theorem TauCeti.RegularFormClass.exists_eq_add_mk_rankOne {K : Type u} [Field K] {x : RegularFormClass K} (hx : 1 ≤ x.rank) : ∃ (a : Kˣ) (y : RegularFormClass K), y.rank + 1 = x.rank ∧ x = y + ⟦⟨1, fun (x : Fin 1) => a⟩⟧

A class of positive rank splits off a line: it is y + ⟨a⟩ for some unit a and a class y of rank one less.

theorem TauCeti.RegularFormClass.exists_eq_mk_binary_add {K : Type u} [Field K] {x : RegularFormClass K} (hx : 2 ≤ x.rank) : ∃ (a : Kˣ) (b : Kˣ) (y : RegularFormClass K), y.rank + 2 = x.rank ∧ x = ⟦⟨2, ![a, b]⟩⟧ + y

A class of rank at least two splits off a binary plane: it is ⟨a, b⟩ + y for some units a, b and a class y of rank two less.

The class of a regular form

theorem TauCeti.exists_presentedForm_equivalent {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 : RegularFormPresentation K), QuadraticMap.Equivalent Q (presentedForm p)

Every regular form on a finite-dimensional space has a diagonal presentation.

noncomputable def TauCeti.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) : RegularFormClass K

The isometry class of a regular form on a finite-dimensional space.

theorem TauCeti.formClass_mk {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 : RegularFormPresentation K) (hp : QuadraticMap.Equivalent Q (presentedForm p)) : formClass Q hQ = ⟦p⟧

The class of a regular form is computed by any of its diagonalizations.

@[simp]

theorem TauCeti.formClass_eq_iff {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) : formClass Q hQ = formClass R hR ↔ QuadraticMap.Equivalent Q R

Two regular forms are isometric exactly when their classes agree.

theorem TauCeti.formClass_lift_radical_eq_of_equivalent {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : QuadraticMap.Equivalent Q R) : formClass (QuadraticMap.lift Q (QuadraticMap.radical Q) ⋯) ⋯ = formClass (QuadraticMap.lift R (QuadraticMap.radical R) ⋯) ⋯

Isometric forms, including degenerate ones, have the same isometry class after quotienting by their radicals.

theorem TauCeti.formClass_lift_radical_eq {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {T : Type u_1} [AddCommGroup T] [Module K T] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hR : QuadraticMap.Nondegenerate) (h : QuadraticMap.Equivalent Q (QuadraticMap.prod 0 R)) : formClass (QuadraticMap.lift Q (QuadraticMap.radical Q) ⋯) ⋯ = formClass R hR

The class of the regular part of Q is the class of the regular summand in any splitting of Q as the orthogonal sum of a zero form and a regular form.

@[simp]

theorem TauCeti.formClass_presentedForm {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : formClass (presentedForm p) ⋯ = ⟦p⟧

The class of a presented form is the class of its presentation.

@[simp]

theorem TauCeti.rank_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) : (formClass Q hQ).rank = Module.finrank K V

The rank of the class of a regular form is the dimension of its space.

@[simp]

theorem TauCeti.formClass_eq_zero_iff {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) : formClass Q hQ = 0 ↔ Module.finrank K V = 0

A regular quadratic form has zero isometry class exactly when its underlying space has dimension zero.

@[simp]

theorem TauCeti.formClass_prod {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) : formClass (QuadraticMap.prod Q R) ⋯ = formClass Q hQ + formClass R hR

The class of an orthogonal product is the sum of the classes.