The Witt-Grothendieck ring and the Witt ring of a field

Over a field in which 2 is invertible the isometry classes of regular finite-dimensional quadratic forms form a commutative semiring under orthogonal sum and tensor product, and Witt cancellation makes that semiring additively cancellative. Its Grothendieck ring is the Witt-Grothendieck ring GW(K), and the Witt ring W(K) is the quotient of GW(K) by the ideal generated by the class of the hyperbolic plane.

The ideal is easy to describe because the hyperbolic plane absorbs tensor products: q ⊗ ℍ is dim q copies of ℍ for every regular q, so the ideal it generates is exactly the cyclic subgroup ℤ · [ℍ]. Consequently two forms have the same Witt class exactly when they differ by hyperbolic planes, which by the uniqueness half of Witt decomposition happens exactly when their anisotropic parts are isometric. Each Witt class therefore has a canonical representative, the anisotropic part, unique up to isometry. Under this identification the ring operations take the anisotropic part after the usual operations on forms.

Scaling by -1 supplies additive inverses modulo hyperbolic planes — q ⊥ (-q) is dim q copies of ℍ — so every element of W(K) is the Witt class of an honest form even though GW(K) also contains formal differences.

Main definitions

• TauCeti.WittGrothendieckRing: the Witt-Grothendieck ring GW(K).
• TauCeti.toWittGrothendieck: the class of a regular form in GW(K).
• TauCeti.WittGrothendieckRing.rank: the rank of a virtual form, as a map to ℤ.
• TauCeti.hyperbolicIdeal: the ideal of GW(K) generated by the hyperbolic plane.
• TauCeti.WittRing: the Witt ring W(K).
• TauCeti.wittClass: the Witt class of a regular form.
• TauCeti.WittRing.dimMod2: the dimension map W(K) → ZMod 2.

Main results

• TauCeti.RegularFormClass.mul_hyperbolicClass: q ⊗ ℍ is dim q copies of ℍ.
• TauCeti.mem_hyperbolicIdeal_iff: the hyperbolic ideal is the cyclic subgroup on [ℍ].
• TauCeti.wittClass_eq_iff_anisotropicPart_eq: two forms have the same Witt class exactly when their anisotropic parts agree.
• TauCeti.wittClass_surjective: every element of the Witt ring is the class of a form.

References

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

Multiples of the hyperbolic class

theorem TauCeti.RegularFormClass.mk_rankOne_mul_hyperbolicClass {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : ⟦⟨1, fun (x : Fin 1) => a⟩⟧ * hyperbolicClass K = hyperbolicClass K

Scaling a hyperbolic plane by a unit gives a hyperbolic plane: ⟨a⟩ ⊗ ℍ ≅ ⟨a, -a⟩ ≅ ℍ.

theorem TauCeti.RegularFormClass.mul_hyperbolicClass {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : x * hyperbolicClass K = x.rank • hyperbolicClass K

The hyperbolic plane absorbs tensor products: q ⊗ ℍ is dim q copies of ℍ. This is what makes the ideal generated by the hyperbolic plane a cyclic subgroup.

theorem TauCeti.RegularFormClass.mk_rankOne_add_neg_one_mul {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : ⟦⟨1, fun (x : Fin 1) => a⟩⟧ + ⟦⟨1, fun (x : Fin 1) => -1⟩⟧ * ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = hyperbolicClass K

Adding a rank-one class to its scaling by -1 produces a hyperbolic plane: ⟨a, -a⟩ ≅ ℍ.

theorem TauCeti.RegularFormClass.add_neg_one_mul {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : x + ⟦⟨1, fun (x : Fin 1) => -1⟩⟧ * x = x.rank • hyperbolicClass K

Scaling by -1 inverts a form modulo hyperbolic planes: q ⊥ (-q) is dim q copies of ℍ. This is what makes the Witt class of every form invertible in W(K) without leaving the image of the forms.

The Witt-Grothendieck ring

@[irreducible]

def TauCeti.WittGrothendieckRing (K : Type u) [Field K] : Type u

The Witt-Grothendieck ring GW(K): the Grothendieck ring of the semiring of isometry classes of regular quadratic forms, with orthogonal sum for addition and tensor product for multiplication.

@[instance_reducible]

noncomputable instance TauCeti.instCommRingWittGrothendieckRing {K : Type u} [Field K] [Invertible 2] : CommRing (WittGrothendieckRing K)

The ring structure on the Witt-Grothendieck ring induced by orthogonal sum and tensor product.

noncomputable def TauCeti.WittGrothendieckRing.equivGrothendieck {K : Type u} [Field K] [Invertible 2] : WittGrothendieckRing K ≃+* Algebra.GrothendieckAddGroup (RegularFormClass K)

The canonical ring equivalence from the Witt-Grothendieck ring to the additive Grothendieck group equipped with its induced multiplication.

noncomputable def TauCeti.toWittGrothendieck {K : Type u} [Field K] [Invertible 2] : RegularFormClass K →+* WittGrothendieckRing K

The class of an isometry class of regular forms in the Witt-Grothendieck ring.

theorem TauCeti.toWittGrothendieck_injective {K : Type u} [Field K] [Invertible 2] : Function.Injective ⇑toWittGrothendieck

Witt cancellation makes the map into the Witt-Grothendieck ring injective: no information about a regular form is lost by passing to its virtual class.

theorem TauCeti.toWittGrothendieck_apply {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : WittGrothendieckRing.equivGrothendieck (toWittGrothendieck x) = Algebra.GrothendieckAddGroup.of x

The Witt–Grothendieck class map agrees with the canonical map into the underlying additive Grothendieck group.

theorem TauCeti.exists_eq_sub_toWittGrothendieck {K : Type u} [Field K] [Invertible 2] (z : WittGrothendieckRing K) : ∃ (x : RegularFormClass K) (y : RegularFormClass K), z = toWittGrothendieck x - toWittGrothendieck y

Every element of the Witt-Grothendieck ring is a formal difference of two isometry classes.

noncomputable def TauCeti.WittGrothendieckRing.rank {K : Type u} [Field K] [Invertible 2] : WittGrothendieckRing K →+* ℤ

The rank of a virtual form, as a ring homomorphism to ℤ. On the class of an honest form it is the dimension of the underlying space.

@[simp]

theorem TauCeti.WittGrothendieckRing.rank_toWittGrothendieck {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : rank (toWittGrothendieck x) = ↑x.rank

The rank map sends the Grothendieck class of a form to its dimension.

The hyperbolic ideal

noncomputable def TauCeti.hyperbolicIdeal (K : Type u) [Field K] [Invertible 2] : Ideal (WittGrothendieckRing K)

The ideal of the Witt-Grothendieck ring generated by the class of the hyperbolic plane.

theorem TauCeti.mem_hyperbolicIdeal_iff {K : Type u} [Field K] [Invertible 2] {z : WittGrothendieckRing K} : z ∈ hyperbolicIdeal K ↔ ∃ (m : ℤ), z = m • toWittGrothendieck (hyperbolicClass K)

The hyperbolic ideal is the cyclic subgroup generated by the hyperbolic plane. An ideal generated by a single element consists of its multiples, and multiplying [ℍ] by the class of a form only produces integer multiples of [ℍ], by TauCeti.RegularFormClass.mul_hyperbolicClass.

The Witt ring

@[irreducible]

def TauCeti.WittRing (K : Type u) [Field K] [Invertible 2] : Type u

The Witt ring W(K): the Witt-Grothendieck ring modulo the ideal generated by the hyperbolic plane.

@[instance_reducible]

noncomputable instance TauCeti.instCommRingWittRing {K : Type u} [Field K] [Invertible 2] : CommRing (WittRing K)

The quotient ring structure on the Witt ring.

noncomputable def TauCeti.WittRing.equivQuotient {K : Type u} [Field K] [Invertible 2] : WittRing K ≃+* WittGrothendieckRing K ⧸ hyperbolicIdeal K

The canonical ring equivalence from the Witt ring to the quotient by the hyperbolic ideal.

noncomputable def TauCeti.WittRing.mk {K : Type u} [Field K] [Invertible 2] : WittGrothendieckRing K →+* WittRing K

The canonical quotient homomorphism from the Witt-Grothendieck ring to the Witt ring.

@[simp]

theorem TauCeti.WittRing.equivQuotient_mk {K : Type u} [Field K] [Invertible 2] (x : WittGrothendieckRing K) : equivQuotient (mk x) = (Ideal.Quotient.mk (hyperbolicIdeal K)) x

Under the quotient equivalence, WittRing.mk is the ordinary ideal-quotient map.

theorem TauCeti.WittRing.mk_eq_mk {K : Type u} [Field K] [Invertible 2] {x y : WittGrothendieckRing K} : mk x = mk y ↔ x - y ∈ hyperbolicIdeal K

Two virtual forms have the same image in the Witt ring exactly when their difference belongs to the hyperbolic ideal.

theorem TauCeti.WittRing.mk_eq_zero_iff_mem {K : Type u} [Field K] [Invertible 2] {x : WittGrothendieckRing K} : mk x = 0 ↔ x ∈ hyperbolicIdeal K

A virtual form maps to zero in the Witt ring exactly when it belongs to the hyperbolic ideal.

theorem TauCeti.WittRing.ker_mk {K : Type u} [Field K] [Invertible 2] : RingHom.ker mk = hyperbolicIdeal K

The kernel of the canonical map to the Witt ring is the hyperbolic ideal.

theorem TauCeti.WittRing.mk_surjective {K : Type u} [Field K] [Invertible 2] : Function.Surjective ⇑mk

The canonical map from the Witt-Grothendieck ring onto the Witt ring is surjective.

noncomputable def TauCeti.WittRing.lift {K : Type u} [Field K] [Invertible 2] {R : Type u_1} [Semiring R] (f : WittGrothendieckRing K →+* R) (h : hyperbolicIdeal K ≤ RingHom.ker f) : WittRing K →+* R

A ring homomorphism from the Witt-Grothendieck ring that kills the hyperbolic ideal factors through the Witt ring.

theorem TauCeti.WittRing.lift_comp_mk {K : Type u} [Field K] [Invertible 2] {R : Type u_1} [Semiring R] (f : WittGrothendieckRing K →+* R) (h : hyperbolicIdeal K ≤ RingHom.ker f) : (lift f h).comp mk = f

The factorization through the Witt ring agrees with the original map after the canonical quotient map.

noncomputable def TauCeti.wittClass {K : Type u} [Field K] [Invertible 2] : RegularFormClass K →+* WittRing K

The Witt class of an isometry class of regular quadratic forms.

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

The Witt class map is the composite of the Grothendieck map and the quotient map.

@[simp]

theorem TauCeti.wittClass_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : wittClass (hyperbolicClass K) = 0

The hyperbolic plane has trivial Witt class.

theorem TauCeti.wittClass_nsmul_hyperbolicClass_add {K : Type u} [Field K] [Invertible 2] (m : ℕ) (x : RegularFormClass K) : wittClass (m • hyperbolicClass K + x) = wittClass x

Adding hyperbolic planes does not change the Witt class.

theorem TauCeti.wittClass_eq_iff_exists_nsmul {K : Type u} [Field K] [Invertible 2] {x y : RegularFormClass K} : wittClass x = wittClass y ↔ ∃ (m : ℕ) (n : ℕ), m • hyperbolicClass K + x = n • hyperbolicClass K + y

Two forms have the same Witt class exactly when they differ by hyperbolic planes.

@[simp]

theorem TauCeti.wittClass_eq_iff_anisotropicPart_eq {K : Type u} [Field K] [Invertible 2] {x y : RegularFormClass K} : wittClass x = wittClass y ↔ x.anisotropicPart = y.anisotropicPart

The anisotropic part is the canonical representative of a Witt class: two regular forms have the same Witt class exactly when their anisotropic parts are isometric.

@[simp]

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

A form and its anisotropic part have the same Witt class.

theorem TauCeti.eq_of_anisotropic_of_anisotropic_of_wittClass_eq {K : Type u} [Field K] [Invertible 2] {x y : RegularFormClass K} (hx : x.Anisotropic) (hy : y.Anisotropic) (h : wittClass x = wittClass y) : x = y

Anisotropic forms are separated by their Witt classes: this is Witt's theorem that the anisotropic part is a complete invariant.

@[simp]

theorem TauCeti.wittClass_eq_zero_iff {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} : wittClass x = 0 ↔ x.anisotropicPart = 0

A form has trivial Witt class exactly when it is a sum of hyperbolic planes.

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

Every element of the Witt ring is the Witt class of a form. The inverse of the class of q is the class of -q, by TauCeti.RegularFormClass.add_neg_one_mul.

The dimension map

noncomputable def TauCeti.WittRing.dimMod2 {K : Type u} [Field K] [Invertible 2] : WittRing K →+* ZMod 2

The dimension map W(K) → ZMod 2: the rank of a form modulo two, which is well defined on Witt classes because a hyperbolic plane has rank two.

@[simp]

theorem TauCeti.WittRing.dimMod2_wittClass {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : dimMod2 (wittClass x) = ↑x.rank

The mod-two dimension of the Witt class of a form is its rank modulo two.