The signed discriminant on the Witt ring and I/I² ≅ Kˣ/(Kˣ)²

Adding a hyperbolic plane does not change the signed discriminant d±, so d± is a well-defined function on the Witt ring W(K). It need not be additive on all of W(K): d±(q ⊥ r) picks up the sign (-1)^{mn} in ranks m and n. That sign disappears as soon as one summand has even rank. So d± restricts to an additive map on the fundamental ideal I(K), and this is where the signed discriminant, rather than the plain one, is forced.

On a one-fold Pfister class d±⟨⟨a⟩⟩ is the square class of a. The two-fold Pfister classes lie in its kernel, and they additively generate I(K)², so d± vanishes on I(K)². Conversely, the identity ⟨⟨a⟩⟩ + ⟨⟨b⟩⟩ = ⟨⟨ab⟩⟩ + ⟨⟨a, b⟩⟩ shows that every element of I(K) is congruent modulo I(K)² to a single one-fold Pfister class ⟨⟨a⟩⟩, with a in the square class d±(x). Together these describe I(K)² as the classes of the even-dimensional forms of trivial signed discriminant, and give the isomorphism I(K)/I(K)² ≅ Kˣ/(Kˣ)².

The quotient I/I² is Mathlib's Ideal.Cotangent. The square-class group is TauCeti.SquareClassGroup K, written additively.

Main definitions

• TauCeti.WittRing.signedDiscr: the signed discriminant of a Witt class.
• TauCeti.signedDiscrHom: its restriction to I(K). This map is semilinear along the dimension-mod-two map W(K) → ZMod 2.
• TauCeti.fundamentalIdealCotangentEquiv: the isomorphism I(K)/I(K)² ≃+ Kˣ/(Kˣ)².

Main results

• TauCeti.WittRing.signedDiscr_wittClass: d± of the Witt class of a form is d± of the form.
• TauCeti.WittRing.signedDiscr_add: the correction term for d± of a sum of Witt classes.
• TauCeti.WittRing.signedDiscr_add_of_mem_fundamentalIdeal: the correction term vanishes once one summand lies in I(K).
• TauCeti.WittRing.signedDiscr_oneFoldPfisterClass: d±⟨⟨a⟩⟩ is the square class of a.
• TauCeti.mem_fundamentalIdeal_sq_iff: I(K)² consists of the classes in I(K) with trivial signed discriminant.
• TauCeti.wittClass_mem_fundamentalIdeal_sq_iff: a form has Witt class in I(K)² exactly when it has even rank and trivial signed discriminant.
• TauCeti.oneFoldPfisterClass_eq_zero_iff: ⟨⟨a⟩⟩ = 0 in W(K) exactly when a is a square.
• TauCeti.signedDiscrHom_surjective and TauCeti.signedDiscrHom_eq_zero_iff: d± maps I(K) onto the square-class group with kernel I(K)².

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter II, §2, where the signed discriminant is shown to induce I/I² ≅ Kˣ/(Kˣ)².

The signed discriminant of a Witt class

noncomputable def TauCeti.WittRing.signedDiscr {K : Type u} [Field K] [Invertible 2] (x : WittRing K) : SquareClassGroup K

The signed discriminant of a Witt class: d± of any form representing it. This is well defined because adding a hyperbolic plane does not change d±; see TauCeti.WittRing.signedDiscr_wittClass.

@[simp]

theorem TauCeti.WittRing.signedDiscr_wittClass {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : (wittClass x).signedDiscr = x.signedDiscr

The signed discriminant of the Witt class of a form is the signed discriminant of the form.

@[simp]

theorem TauCeti.WittRing.signedDiscr_zero {K : Type u} [Field K] [Invertible 2] : signedDiscr 0 = 0

The zero Witt class has trivial signed discriminant.

@[simp]

theorem TauCeti.WittRing.signedDiscr_one {K : Type u} [Field K] [Invertible 2] : signedDiscr 1 = 0

The Witt class of ⟨1⟩ has trivial signed discriminant.

theorem TauCeti.WittRing.signedDiscr_add {K : Type u} [Field K] [Invertible 2] (x y : WittRing K) : (x + y).signedDiscr = (dimMod2 x * dimMod2 y) • squareClass (-1) + x.signedDiscr + y.signedDiscr

The signed discriminant of a sum of Witt classes: the correction term is the product of their dimensions modulo two, times the square class of -1.

@[simp]

theorem TauCeti.WittRing.signedDiscr_add_of_mem_fundamentalIdeal {K : Type u} [Field K] [Invertible 2] {x : WittRing K} (hx : x ∈ fundamentalIdeal K) (y : WittRing K) : (x + y).signedDiscr = x.signedDiscr + y.signedDiscr

The signed discriminant is additive on the fundamental ideal: d±(x + y) = d±(x) + d±(y) as soon as x has even dimension.

@[simp]

theorem TauCeti.WittRing.signedDiscr_neg_of_mem_fundamentalIdeal {K : Type u} [Field K] [Invertible 2] {x : WittRing K} (hx : x ∈ fundamentalIdeal K) : (-x).signedDiscr = x.signedDiscr

On the fundamental ideal the signed discriminant is invariant under negation.

theorem TauCeti.WittRing.signedDiscr_nsmul_of_mem_fundamentalIdeal {K : Type u} [Field K] [Invertible 2] (n : ℕ) {x : WittRing K} (hx : x ∈ fundamentalIdeal K) : (n • x).signedDiscr = n • x.signedDiscr

On the fundamental ideal the signed discriminant commutes with natural multiples.

@[simp]

theorem TauCeti.WittRing.signedDiscr_oneFoldPfisterClass {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : (oneFoldPfisterClass a).signedDiscr = squareClass a

The signed discriminant of a one-fold Pfister class: d±⟨⟨a⟩⟩ = d±⟨1, -a⟩ is the square class of a.

theorem TauCeti.WittRing.signedDiscr_oneFoldPfisterClass_mul {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : (oneFoldPfisterClass a * oneFoldPfisterClass b).signedDiscr = 0

The signed discriminant of a two-fold Pfister class ⟨⟨a, b⟩⟩ is trivial.

theorem TauCeti.WittRing.signedDiscr_eq_zero_of_mem_fundamentalIdeal_sq {K : Type u} [Field K] [Invertible 2] {x : WittRing K} (hx : x ∈ fundamentalIdeal K ^ 2) : x.signedDiscr = 0

The signed discriminant vanishes on I(K)². The two-fold Pfister classes additively generate I(K)² and have trivial signed discriminant, and d± is additive on I(K).

@[simp]

theorem TauCeti.WittRing.signedDiscr_mul_of_mem_fundamentalIdeal {K : Type u} [Field K] [Invertible 2] (w : WittRing K) {x : WittRing K} (hx : x ∈ fundamentalIdeal K) : (w * x).signedDiscr = dimMod2 w • x.signedDiscr

The signed discriminant is semilinear on the fundamental ideal: for x ∈ I(K), d±(w x) = dim(w) • d±(x), with the dimension of w read modulo two.

I(K)² is the kernel of the signed discriminant

@[simp]

theorem TauCeti.oneFoldPfisterClass_eq_zero_iff {K : Type u} [Field K] [Invertible 2] {a : Kˣ} : oneFoldPfisterClass a = 0 ↔ IsSquare a

⟨⟨a⟩⟩ = ⟨1, -a⟩ vanishes in the Witt ring exactly when a is a square.

@[simp]

theorem TauCeti.mem_fundamentalIdeal_sq_iff {K : Type u} [Field K] [Invertible 2] {x : WittRing K} : x ∈ fundamentalIdeal K ^ 2 ↔ x ∈ fundamentalIdeal K ∧ x.signedDiscr = 0

The description of I(K)² by the signed discriminant: a Witt class lies in I(K)² exactly when it lies in I(K) and has trivial signed discriminant.

theorem TauCeti.wittClass_mem_fundamentalIdeal_sq_iff {K : Type u} [Field K] [Invertible 2] (q : RegularFormClass K) : wittClass q ∈ fundamentalIdeal K ^ 2 ↔ Even q.rank ∧ q.signedDiscr = 0

A form has Witt class in I(K)² exactly when it has even rank and trivial signed discriminant.

theorem TauCeti.oneFoldPfisterClass_mem_fundamentalIdeal_sq_iff {K : Type u} [Field K] [Invertible 2] {a : Kˣ} : oneFoldPfisterClass a ∈ fundamentalIdeal K ^ 2 ↔ IsSquare a

A one-fold Pfister class ⟨⟨a⟩⟩ lies in I(K)² exactly when a is a square, in which case it is already zero.

The isomorphism I(K)/I(K)² ≅ Kˣ/(Kˣ)²

noncomputable def TauCeti.signedDiscrHom {K : Type u} [Field K] [Invertible 2] : ↥(fundamentalIdeal K) →ₛₗ[WittRing.dimMod2] SquareClassGroup K

The signed discriminant on the fundamental ideal, as a map I(K) → Kˣ/(Kˣ)² that is semilinear along the dimension-mod-two map W(K) → ZMod 2. Its kernel is I(K)², by TauCeti.signedDiscrHom_eq_zero_iff, and it is surjective, by TauCeti.signedDiscrHom_surjective.

@[simp]

theorem TauCeti.signedDiscrHom_apply {K : Type u} [Field K] [Invertible 2] (x : ↥(fundamentalIdeal K)) : signedDiscrHom x = (↑x).signedDiscr

signedDiscrHom evaluates the signed discriminant.

theorem TauCeti.signedDiscrHom_surjective {K : Type u} [Field K] [Invertible 2] : Function.Surjective ⇑signedDiscrHom

The signed discriminant maps the one-fold Pfister class ⟨⟨a⟩⟩ to the square class of a; in particular it maps I(K) onto the square-class group.

theorem TauCeti.signedDiscrHom_eq_zero_iff {K : Type u} [Field K] [Invertible 2] (x : ↥(fundamentalIdeal K)) : signedDiscrHom x = 0 ↔ ↑x ∈ fundamentalIdeal K ^ 2

The kernel of the signed discriminant on I(K) is I(K)².

noncomputable def TauCeti.fundamentalIdealCotangentEquiv {K : Type u} [Field K] [Invertible 2] : (fundamentalIdeal K).Cotangent ≃+ SquareClassGroup K

I(K)/I(K)² ≅ Kˣ/(Kˣ)²: the signed discriminant induces an isomorphism from the cotangent space I(K)/I(K)² of the fundamental ideal onto the square-class group.

@[simp]

theorem TauCeti.fundamentalIdealCotangentEquiv_toCotangent {K : Type u} [Field K] [Invertible 2] (x : ↥(fundamentalIdeal K)) : fundamentalIdealCotangentEquiv ((fundamentalIdeal K).toCotangent x) = (↑x).signedDiscr

The isomorphism I(K)/I(K)² ≅ Kˣ/(Kˣ)² sends the class of x ∈ I(K) to d±(x).

@[simp]

theorem TauCeti.fundamentalIdealCotangentEquiv_symm_squareClass {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : fundamentalIdealCotangentEquiv.symm (squareClass a) = (fundamentalIdeal K).toCotangent ⟨oneFoldPfisterClass a, ⋯⟩

The inverse isomorphism Kˣ/(Kˣ)² ≅ I(K)/I(K)² sends the square class of a to the class of the one-fold Pfister form ⟨⟨a⟩⟩.