Signature on Witt rings over ordered fields

The integer signature, the positive index minus the negative index, defines a ring homomorphism from the Witt ring of an ordered field to ℤ. The hyperbolic plane has signature zero, while the positive and negative unit lines have signatures 1 and -1. Over a real closed field, every line is isometric to one of these unit lines, so every Witt class is an integer multiple of the positive unit line.

The signature extends first to the Witt-Grothendieck ring and then descends through the hyperbolic ideal. For an ordered real closed field, the resulting ring equivalence has integer cast as its inverse. In particular, two regular forms over such a field have the same Witt class exactly when their integer signatures agree, and two regular forms of the same rank are isometric exactly when their integer signatures agree. Taking K = ℝ gives the real Witt ring; the real closed instance is available in Mathlib.FieldTheory.IsRealClosed.Real.

Main definitions and results

• WittGrothendieckRing.signature: the signature of a virtual form over an ordered field.
• WittRing.signature: the integer signature on Witt classes over an ordered field.
• WittRing.equivInt: the signature isomorphism W(K) ≃+* ℤ for ordered real closed fields.
• WittRing.signature_wittClass: computes the signature from a regular-form class.
• WittRing.intCast_signature: reconstructs a Witt class from its signature.
• wittClass_eq_iff_signature_eq: Witt classes over ordered real closed fields are determined by the signature.
• RegularFormClass.eq_iff_rank_eq_and_signature_eq: Sylvester's law of inertia for isometry classes over ordered real closed fields.

References

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

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

The integer signature of a virtual form over an ordered field, extending the signature on regular-form classes to their Grothendieck ring.

@[simp]

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

The signature of the Grothendieck class of a regular form is its integer signature.

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

The integer signature of a Witt class over an ordered field. Signature vanishes on hyperbolic forms, so it is well defined on the quotient.

@[simp]

theorem TauCeti.WittRing.signature_mk {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] (x : WittGrothendieckRing K) : signature (mk x) = WittGrothendieckRing.signature x

Signature on the Witt ring agrees with signature on virtual forms.

@[simp]

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

Signature on the Witt ring agrees with signature on regular-form classes.

@[simp]

theorem TauCeti.WittRing.intCast_signature {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] (x : WittRing K) : ↑(signature x) = x

Every Witt class over an ordered real closed field is its signature times the positive unit line.

noncomputable def TauCeti.WittRing.equivInt {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] : WittRing K ≃+* ℤ

The Witt ring of an ordered real closed field is isomorphic to the integers by its signature. Its inverse is integer cast, as characterized by Mathlib's eq_intCast; simp simplifies inverse applications to integer casts.

@[simp]

theorem TauCeti.WittRing.equivInt_apply {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] (x : WittRing K) : equivInt x = signature x

The real closed Witt-ring isomorphism evaluates by taking the integer signature.

theorem TauCeti.wittClass_eq_iff_signature_eq {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] {x y : RegularFormClass K} : wittClass x = wittClass y ↔ x.signature = y.signature

Witt classes over a real closed field. Over an ordered real closed field, two regular-form classes have the same Witt class exactly when their signatures agree.

theorem TauCeti.RegularFormClass.eq_iff_rank_eq_and_signature_eq {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K] {x y : RegularFormClass K} : x = y ↔ x.rank = y.rank ∧ x.signature = y.signature

Sylvester's law of inertia for isometry classes. Over an ordered real closed field, two regular-form classes are equal exactly when they have the same rank and the same signature.