Signature of regular quadratic forms over ordered fields

The integer signature is the positive index minus the negative index of inertia. It descends to isometry classes over any ordered field, is additive under orthogonal sum, and is multiplicative under tensor product. It therefore defines a semiring homomorphism to ℤ and vanishes on the hyperbolic plane.

Over an ordered real closed field, every positive coefficient is a square. Positive lines are therefore isometric to ⟨1⟩, and negative lines to ⟨-1⟩. These reductions are used to identify the Witt ring with ℤ by signature.

Main results

• TauCeti.RegularFormClass.signatureHom: the integer signature as a semiring homomorphism.
• TauCeti.signature_formClass: computes signature from the inertia indices of a regular form.
• TauCeti.RegularFormClass.mk_rankOne_eq_one_of_pos: positive lines over real closed fields are isometric to the unit line.
• TauCeti.RegularFormClass.mk_rankOne_eq_mk_neg_one_of_neg: negative lines over real closed fields are isometric to the negative unit line.

References

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

noncomputable def TauCeti.RegularFormClass.signature {K : Type u_1} [Field K] [LinearOrder K] : RegularFormClass K → ℤ

The integer signature of a regular-form class: its positive index minus its negative index.

@[simp]

theorem TauCeti.RegularFormClass.signature_mk {K : Type u_1} [Field K] [LinearOrder K] (p : RegularFormPresentation K) : signature ⟦p⟧ = ↑(sigPos (presentedForm p)) - ↑(sigNeg (presentedForm p))

The signature of a diagonal presentation is the difference of its inertia indices.

@[simp]

theorem TauCeti.signature_formClass {K : Type u_1} [Field K] [LinearOrder K] {M : Type u_2} [AddCommGroup M] [Module K M] [FiniteDimensional K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : QuadraticMap.Nondegenerate) : (formClass Q hQ).signature = ↑(sigPos Q) - ↑(sigNeg Q)

The signature on isometry classes agrees with the inertia indices of any regular form.

@[simp]

theorem TauCeti.RegularFormClass.signature_zero {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : signature 0 = 0

The zero-dimensional form has signature zero.

@[simp]

theorem TauCeti.RegularFormClass.signature_add {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (x y : RegularFormClass K) : (x + y).signature = x.signature + y.signature

Signature is additive under orthogonal sum.

@[simp]

theorem TauCeti.RegularFormClass.signature_mk_rankOne {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (a : Kˣ) : signature ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = if 0 < ↑a then 1 else -1

A line has signature 1 or -1, according to the sign of its coefficient.

@[simp]

theorem TauCeti.RegularFormClass.signature_one {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : signature 1 = 1

The positive unit line has signature one.

@[simp]

theorem TauCeti.RegularFormClass.signature_hyperbolicClass {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] : (hyperbolicClass K).signature = 0

The hyperbolic plane has signature zero.

@[simp]

theorem TauCeti.RegularFormClass.signature_mul {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] (x y : RegularFormClass K) : (x * y).signature = x.signature * y.signature

Signature is multiplicative under tensor product.

noncomputable def TauCeti.RegularFormClass.signatureHom {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] : RegularFormClass K →+* ℤ

The integer signature as a semiring homomorphism on regular-form classes.

@[simp]

theorem TauCeti.RegularFormClass.signatureHom_apply {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] (x : RegularFormClass K) : signatureHom x = x.signature

theorem TauCeti.RegularFormClass.signature_nsmul {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] (n : ℕ) (x : RegularFormClass K) : (n • x).signature = n • x.signature

The signature of the orthogonal sum of n copies of a class is n times its signature.

theorem TauCeti.RegularFormClass.mk_rankOne_eq_one_of_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] {a : Kˣ} (ha : 0 < ↑a) : ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = 1

A positive line over a real closed field is isometric to the unit line.

theorem TauCeti.RegularFormClass.mk_rankOne_eq_mk_neg_one_of_neg {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] {a : Kˣ} (ha : ↑a < 0) : ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = ⟦⟨1, fun (x : Fin 1) => -1⟩⟧

A negative line over a real closed field is isometric to the line with coefficient -1.