Pfister classes and powers of the fundamental ideal

For units a₁, …, aₙ, the n-fold Pfister form is the tensor product

<<a₁, …, aₙ>> = <<a₁>> ⋯ <<aₙ>>,

where <<a>> = <1, -a>. This file defines its diagonal presentation, isometry class, and Witt class, and proves that, for every positive n, the additive group underlying I(K)^n is generated by the n-fold Pfister classes. The explicit two- and three-fold corollaries are the forms used to define and control the Clifford invariant.

The positivity condition is necessary: I(K)^0 = W(K), while the sole zero-fold Pfister class is <1>, and a Witt ring need not be additively cyclic.

Main definitions

• TauCeti.pfisterFormClass: the isometry class of an iterated Pfister tensor product.
• TauCeti.pfisterClass: its Witt class.
• TauCeti.pfisterForm: its diagonal tuple of weights.

Main results

• TauCeti.discr_pfisterFormClass: Pfister forms of fold at least two have trivial discriminant.
• TauCeti.fundamentalIdeal_pow_eq_addClosure: positive powers of the fundamental ideal are additively generated by Pfister classes.
• TauCeti.fundamentalIdeal_sq_eq_addClosure and TauCeti.fundamentalIdeal_cube_eq_addClosure: the cases needed for the Clifford invariant.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter II, §1 and Chapter X, with the convention <<a>> = <1, -a>.

def TauCeti.pfisterForm {K : Type u} [Field K] {n : ℕ} : (Fin n → Kˣ) → Fin (2 ^ n) → Kˣ

The diagonal weights of the n-fold Pfister form, ordered by the binary subsets of its slots.

@[simp]

theorem TauCeti.pfisterForm_zero {K : Type u} [Field K] (a : Fin 0 → Kˣ) : pfisterForm a = fun (x : Fin (2 ^ 0)) => 1

The zero-fold Pfister form has the single diagonal weight 1.

@[simp]

theorem TauCeti.pfisterForm_one {K : Type u} [Field K] (a : Kˣ) : pfisterForm ![a] = ![1, -a]

⟨⟨a⟩⟩ = ⟨1, -a⟩.

@[simp]

theorem TauCeti.pfisterForm_two {K : Type u} [Field K] (a b : Kˣ) : pfisterForm ![a, b] = ![1, -a, -b, a * b]

⟨⟨a, b⟩⟩ = ⟨1, -a, -b, ab⟩.

theorem TauCeti.pfisterPresentation_cons {K : Type u} [Field K] {n : ℕ} (a : Fin (n + 1) → Kˣ) : ⟨2 ^ (n + 1), pfisterForm a⟩ = RegularFormPresentation.tmul ⟨2 ^ n, pfisterForm (Fin.tail a)⟩ ⟨2, ![1, -a 0]⟩

Splitting off the first slot identifies the diagonal Pfister presentation with the tensor product of the remaining presentation and the corresponding one-fold presentation.

noncomputable def TauCeti.pfisterFormClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : RegularFormClass K

The isometry class of the n-fold Pfister form, using the convention <<a>> = <1, -a>. Orthogonal sum is addition and tensor product is multiplication on RegularFormClass; the empty product is therefore the zero-fold form <1>.

theorem TauCeti.pfisterFormClass_def {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : pfisterFormClass a = ∏ i : Fin n, (1 + ⟦⟨1, fun (x : Fin 1) => -a i⟩⟧)

The defining product for the isometry class of an n-fold Pfister form.

@[simp]

theorem TauCeti.pfisterFormClass_cons {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Kˣ) (b : Fin n → Kˣ) : pfisterFormClass (Fin.cons a b) = (1 + ⟦⟨1, fun (x : Fin 1) => -a⟩⟧) * pfisterFormClass b

Splitting off the first slot splits a Pfister form as a tensor product.

@[simp]

theorem TauCeti.pfisterFormClass_zero {K : Type u} [Field K] [Invertible 2] (a : Fin 0 → Kˣ) : pfisterFormClass a = 1

The zero-fold Pfister form is the rank-one unit form.

@[simp]

theorem TauCeti.pfisterFormClass_comp_equiv {K : Type u} [Field K] [Invertible 2] {m n : ℕ} (a : Fin n → Kˣ) (e : Fin m ≃ Fin n) : pfisterFormClass (a ∘ ⇑e) = pfisterFormClass a

Reindexing the slots of a Pfister form class by an equivalence does not change it.

theorem TauCeti.pfisterFormClass_eq_mk {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : pfisterFormClass a = ⟦⟨2 ^ n, pfisterForm a⟩⟧

The isometry class of a Pfister form is represented by its explicit diagonal tuple.

@[simp]

theorem TauCeti.pfisterFormClass_one {K : Type u} [Field K] [Invertible 2] (a : Fin 1 → Kˣ) : pfisterFormClass a = ⟦⟨2, ![1, -a 0]⟩⟧

A one-fold Pfister form has diagonal weights <1, -a>.

@[simp]

theorem TauCeti.pfisterFormClass_two {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : pfisterFormClass ![a, b] = ⟦⟨4, ![1, -a, -b, a * b]⟩⟧

A two-fold Pfister form has diagonal weights <1, -a, -b, ab>.

@[simp]

theorem TauCeti.rank_pfisterFormClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : (pfisterFormClass a).rank = 2 ^ n

An n-fold Pfister form has rank 2 ^ n.

@[simp]

theorem TauCeti.discr_pfisterFormClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) (hn : 2 ≤ n) : (pfisterFormClass a).discr = 0

Pfister forms of fold at least two have trivial discriminant: the signed discriminant of an n-fold Pfister form is the trivial square class once n ≥ 2.

noncomputable def TauCeti.pfisterClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : WittRing K

The Witt class of an n-fold Pfister form.

@[simp]

theorem TauCeti.wittClass_pfisterFormClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : wittClass (pfisterFormClass a) = pfisterClass a

Taking the Witt class of a Pfister form class gives its Pfister class.

theorem TauCeti.pfisterClass_eq_prod {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : pfisterClass a = ∏ i : Fin n, oneFoldPfisterClass (a i)

The Witt class of a Pfister form is the product of its one-fold factors.

@[simp]

theorem TauCeti.pfisterClass_zero {K : Type u} [Field K] [Invertible 2] (a : Fin 0 → Kˣ) : pfisterClass a = 1

The zero-fold Pfister class is the unit of the Witt ring.

@[simp]

theorem TauCeti.pfisterClass_cons {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Kˣ) (b : Fin n → Kˣ) : pfisterClass (Fin.cons a b) = oneFoldPfisterClass a * pfisterClass b

Splitting off the first slot splits a Pfister class as a product.

@[simp]

theorem TauCeti.pfisterClass_one {K : Type u} [Field K] [Invertible 2] (a : Fin 1 → Kˣ) : pfisterClass a = oneFoldPfisterClass (a 0)

A one-fold Pfister class agrees with the existing class of <1, -a>.

@[simp]

theorem TauCeti.pfisterClass_comp_equiv {K : Type u} [Field K] [Invertible 2] {m n : ℕ} (a : Fin n → Kˣ) (e : Fin m ≃ Fin n) : pfisterClass (a ∘ ⇑e) = pfisterClass a

Reindexing the slots of a Pfister class by an equivalence does not change it.

@[simp]

theorem TauCeti.pfisterClass_two {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : pfisterClass ![a, b] = oneFoldPfisterClass a * oneFoldPfisterClass b

The two-fold Pfister class is the product <<a>> * <<b>>.

@[simp]

theorem TauCeti.pfisterClass_mem_fundamentalIdeal_pow {K : Type u} [Field K] [Invertible 2] {n : ℕ} (a : Fin n → Kˣ) : pfisterClass a ∈ fundamentalIdeal K ^ n

Every n-fold Pfister class belongs to I(K)^n.

theorem TauCeti.fundamentalIdeal_pow_eq_addClosure {K : Type u} [Field K] [Invertible 2] {n : ℕ} (hn : 0 < n) : Submodule.toAddSubgroup (fundamentalIdeal K ^ n) = AddSubgroup.closure (Set.range pfisterClass)

For 0 < n, the additive group underlying I(K)^n is generated by the n-fold Pfister classes. The positivity hypothesis excludes the generally false assertion that W(K) = I(K)^0 is additively generated by the zero-fold class <1>.

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

The square of the fundamental ideal is additively generated by two-fold Pfister classes.

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

The cube of the fundamental ideal is additively generated by three-fold Pfister classes.