The fundamental ideal of the Witt ring

The fundamental ideal I(K) of the Witt ring is the kernel of dimension modulo two. Thus a Witt class belongs to I(K) precisely when it has an even-dimensional representative.

This file also gives the first generation theorem for the fundamental filtration. The additive group of I(K) is generated by the one-fold Pfister classes ⟨⟨a⟩⟩ = ⟨1, -a⟩. In particular these classes generate I(K) as an ideal.

Main definitions

• TauCeti.fundamentalIdeal: the kernel of WittRing.dimMod2.
• TauCeti.oneFoldPfisterClass: the Witt class of ⟨1, -a⟩.

Main results

• TauCeti.wittClass_mem_fundamentalIdeal_iff: a form has class in the fundamental ideal if and only if its rank is even.
• TauCeti.mem_fundamentalIdeal_iff_exists_evenRank: every element of the fundamental ideal is represented by an even-dimensional form.
• TauCeti.fundamentalIdeal_toAddSubgroup_eq_closure_oneFoldPfisterClass: the one-fold Pfister classes generate the additive group of the fundamental ideal.
• TauCeti.fundamentalIdeal_eq_span_oneFoldPfisterClass: the one-fold Pfister classes generate the fundamental ideal as an ideal.

References

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

The fundamental ideal

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

The fundamental ideal I(K) of the Witt ring: the kernel of dimension modulo two.

@[simp]

theorem TauCeti.mem_fundamentalIdeal_iff {K : Type u} [Field K] [Invertible 2] {x : WittRing K} : x ∈ fundamentalIdeal K ↔ WittRing.dimMod2 x = 0

Membership in the fundamental ideal means that dimension modulo two vanishes.

theorem TauCeti.wittClass_mem_fundamentalIdeal_iff {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : wittClass x ∈ fundamentalIdeal K ↔ Even x.rank

The Witt class of a regular form belongs to the fundamental ideal exactly when its rank is even.

theorem TauCeti.mem_fundamentalIdeal_iff_exists_evenRank {K : Type u} [Field K] [Invertible 2] {x : WittRing K} : x ∈ fundamentalIdeal K ↔ ∃ (q : RegularFormClass K), Even q.rank ∧ wittClass q = x

Every element of the fundamental ideal has an even-dimensional representative, and every even-dimensional representative determines an element of the fundamental ideal.

One-fold Pfister classes

noncomputable def TauCeti.oneFoldPfisterClass {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : WittRing K

The one-fold Pfister class ⟨⟨a⟩⟩ = ⟨1, -a⟩ in the Witt ring. This definition fixes the minus-sign convention used for Pfister forms.

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

A one-fold Pfister class is the sum of the unit class ⟨1⟩ and the rank-one class ⟨-a⟩.

@[simp]

theorem TauCeti.WittRing.dimMod2_oneFoldPfisterClass {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : dimMod2 (oneFoldPfisterClass a) = 0

Every one-fold Pfister class has even dimension.

theorem TauCeti.oneFoldPfisterClass_mem_fundamentalIdeal {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : oneFoldPfisterClass a ∈ fundamentalIdeal K

Every one-fold Pfister class belongs to the fundamental ideal.

theorem TauCeti.wittClass_rankOne_eq_oneFoldPfisterClass_sub {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : wittClass ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = oneFoldPfisterClass (-a) - 1

A rank-one class is a one-fold Pfister class minus ⟨1⟩.

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

In the Witt ring ⟨-a⟩ = -⟨a⟩, because ⟨a, -a⟩ is a hyperbolic plane.

theorem TauCeti.oneFoldPfisterClass_mul {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : oneFoldPfisterClass (a * b) = oneFoldPfisterClass a + oneFoldPfisterClass b - oneFoldPfisterClass a * oneFoldPfisterClass b

The one-fold Pfister class of a product: ⟨⟨ab⟩⟩ = ⟨⟨a⟩⟩ + ⟨⟨b⟩⟩ - ⟨⟨a⟩⟩⟨⟨b⟩⟩, that is ⟨⟨a⟩⟩ + ⟨⟨b⟩⟩ = ⟨⟨ab⟩⟩ + ⟨⟨a, b⟩⟩ in the Witt ring.

theorem TauCeti.oneFoldPfisterClass_neg_one {K : Type u} [Field K] [Invertible 2] : oneFoldPfisterClass (-1) = 2 • 1

The one-fold Pfister class ⟨⟨-1⟩⟩ is two copies of ⟨1⟩.

@[simp]

theorem TauCeti.oneFoldPfisterClass_one {K : Type u} [Field K] [Invertible 2] : oneFoldPfisterClass 1 = 0

The one-fold Pfister class ⟨⟨1⟩⟩ = ⟨1, -1⟩ is hyperbolic, hence zero in the Witt ring.

Additive generation

theorem TauCeti.fundamentalIdeal_toAddSubgroup_eq_closure_oneFoldPfisterClass {K : Type u} [Field K] [Invertible 2] : Submodule.toAddSubgroup (fundamentalIdeal K) = AddSubgroup.closure (Set.range oneFoldPfisterClass)

The additive group of the fundamental ideal is the subgroup generated by the one-fold Pfister classes ⟨⟨a⟩⟩. This is the additive generation statement needed for homomorphisms defined on the fundamental filtration.

theorem TauCeti.fundamentalIdeal_eq_span_oneFoldPfisterClass {K : Type u} [Field K] [Invertible 2] : fundamentalIdeal K = Ideal.span (Set.range oneFoldPfisterClass)

The one-fold Pfister classes generate the fundamental ideal as an ideal. The stronger additive-generation theorem is TauCeti.fundamentalIdeal_toAddSubgroup_eq_closure_oneFoldPfisterClass.