Tensor products of regular-form classes

The tensor product of diagonal forms is diagonal: if p has weights a i and q has weights b j, their tensor product has weights a i * b j. This file packages that operation on TauCeti.RegularFormPresentation, proves that it presents Mathlib's QuadraticForm.tmul, and descends it to isometry classes.

Tensor product makes TauCeti.RegularFormClass K a commutative monoid. Together with the orthogonal-sum structure from TauCeti.LinearAlgebra.QuadraticForm.RegularFormClass.Basic, this is the multiplicative half of the semiring whose additive group completion underlies the Witt--Grothendieck ring.

Main definitions

• TauCeti.RegularFormPresentation.tmul: the diagonal presentation of a tensor product.
• TauCeti.presentedFormTensorIsometryEquiv: its comparison with QuadraticForm.tmul.

Main results

• TauCeti.RegularFormPresentation.prod_tmul: the weight product of a tensor presentation.
• TauCeti.RegularFormClass.mk_mul_mk: multiplication computes by tensoring presentations.
• TauCeti.formClass_tmul: the class of a tensor product is the product of the classes.
• TauCeti.formClass_smul: the class of a scalar multiple by a unit is a product with a rank-one class.
• TauCeti.RegularFormClass.rank_mul: rank is multiplicative.

References

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

Tensor products of presentations

def TauCeti.RegularFormPresentation.tmul {K : Type u} [Field K] (p q : RegularFormPresentation K) : RegularFormPresentation K

The diagonal presentation of the tensor product of two presented forms. Its weights are all pairwise products of a weight from each factor.

@[simp]

theorem TauCeti.RegularFormPresentation.fst_tmul {K : Type u} [Field K] (p q : RegularFormPresentation K) : (p.tmul q).fst = p.fst * q.fst

Tensor product multiplies the ranks of presentations.

@[simp]

theorem TauCeti.RegularFormPresentation.tmul_apply {K : Type u} [Field K] (p q : RegularFormPresentation K) (i : Fin p.fst) (j : Fin q.fst) : (p.tmul q).snd (Fin.cast ⋯ (finProdFinEquiv (i, j))) = p.snd i * q.snd j

A tensor-product weight is the product of the corresponding weights of its factors.

@[simp]

theorem TauCeti.RegularFormPresentation.rankOne_tmul {K : Type u} [Field K] (a : Kˣ) (p : RegularFormPresentation K) : tmul ⟨1, fun (x : Fin 1) => a⟩ p = ⟨p.fst, fun (i : Fin p.fst) => a * p.snd i⟩

Tensoring on the left with a rank-one presentation scales every coefficient.

theorem TauCeti.RegularFormPresentation.prod_tmul {K : Type u} [Field K] (p q : RegularFormPresentation K) : ∏ k : Fin (p.tmul q).fst, (p.tmul q).snd k = (∏ i : Fin p.fst, p.snd i) ^ q.fst * (∏ j : Fin q.fst, q.snd j) ^ p.fst

The weight product of a tensor presentation: each factor's weight product raised to the rank of the other factor.

noncomputable def TauCeti.presentedFormTensorIsometryEquiv {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) : QuadraticMap.IsometryEquiv ((presentedForm p).tmul (presentedForm q)) (presentedForm (p.tmul q))

Tensoring two diagonal presentations presents the tensor product of their quadratic forms.

@[simp]

theorem TauCeti.presentedFormTensorIsometryEquiv_tmul_apply {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) (x : Fin p.fst → K) (y : Fin q.fst → K) (i : Fin p.fst) (j : Fin q.fst) : (presentedFormTensorIsometryEquiv p q) (x ⊗ₜ[K] y) (Fin.cast ⋯ (finProdFinEquiv (i, j))) = x i * y j

The comparison isometry sends a pure tensor to the corresponding products of coordinates.

Multiplication of isometry classes

theorem TauCeti.equivalent_presentedForm_tmul {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (p.tmul q)) ((presentedForm p).tmul (presentedForm q))

The form presented by tensoring two presentations is isometric to the tensor product of the forms they present.

theorem TauCeti.presentedForm_tmul_congr {K : Type u} [Field K] [Invertible 2] {p p' q q' : RegularFormPresentation K} (hp : QuadraticMap.Equivalent (presentedForm p) (presentedForm p')) (hq : QuadraticMap.Equivalent (presentedForm q) (presentedForm q')) : QuadraticMap.Equivalent (presentedForm (p.tmul q)) (presentedForm (p'.tmul q'))

Tensoring presentations respects isometry in each argument.

theorem TauCeti.presentedForm_tmul_comm {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (p.tmul q)) (presentedForm (q.tmul p))

Tensoring presentations is commutative up to isometry.

theorem TauCeti.presentedForm_tmul_assoc {K : Type u} [Field K] [Invertible 2] (p q r : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm ((p.tmul q).tmul r)) (presentedForm (p.tmul (q.tmul r)))

Tensoring presentations is associative up to isometry.

def TauCeti.RegularFormPresentation.one {K : Type u} [Field K] : RegularFormPresentation K

The rank-one presentation with weight one.

@[simp]

theorem TauCeti.RegularFormPresentation.fst_one {K : Type u} [Field K] : one.fst = 1

The unit presentation has rank one.

@[simp]

theorem TauCeti.RegularFormPresentation.one_apply {K : Type u} [Field K] (i : Fin one.fst) : one.snd i = 1

The sole weight of the unit presentation is one.

noncomputable def TauCeti.presentedFormOneIsometryEquiv {K : Type u} [Field K] : QuadraticMap.IsometryEquiv (presentedForm RegularFormPresentation.one) QuadraticMap.sq

The rank-one presentation with weight one presents the square form.

@[simp]

theorem TauCeti.presentedFormOneIsometryEquiv_apply {K : Type u} [Field K] (x : Fin RegularFormPresentation.one.fst → K) : presentedFormOneIsometryEquiv x = x (Fin.cast ⋯ 0)

The comparison from the unit presentation to the square form evaluates its sole coordinate.

theorem TauCeti.presentedForm_tmul_one {K : Type u} [Field K] (p : RegularFormPresentation K) : QuadraticMap.Equivalent (presentedForm (p.tmul RegularFormPresentation.one)) (presentedForm p)

Tensoring a presentation on the right with the rank-one presentation preserves its form up to isometry.

@[instance_reducible]

instance TauCeti.instMulRegularFormClass {K : Type u} [Field K] [Invertible 2] : Mul (RegularFormClass K)

Tensor product of isometry classes.

@[instance_reducible]

instance TauCeti.instOneRegularFormClass {K : Type u} [Field K] : One (RegularFormClass K)

The class of the rank-one form with coefficient one.

@[simp]

theorem TauCeti.RegularFormClass.mk_mul_mk {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) : ⟦p⟧ * ⟦q⟧ = ⟦p.tmul q⟧

The product of two classes is represented by pairwise products of their weights.

theorem TauCeti.RegularFormClass.one_def {K : Type u} [Field K] : 1 = ⟦RegularFormPresentation.one⟧

The multiplicative unit is represented by the rank-one presentation with weight one.

theorem TauCeti.RegularFormClass.mk_rankOne_one {K : Type u} [Field K] : ⟦⟨1, fun (x : Fin 1) => 1⟩⟧ = 1

The class of the rank-one presentation with weight one is the multiplicative unit.

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

The tensor product of rank-one classes: ⟨a⟩ ⊗ ⟨b⟩ = ⟨ab⟩.

@[instance_reducible]

instance TauCeti.instCommMonoidRegularFormClass {K : Type u} [Field K] [Invertible 2] : CommMonoid (RegularFormClass K)

Tensor product makes regular-form classes a commutative monoid.

@[simp]

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

Rank is multiplicative on tensor products of classes.

@[simp]

theorem TauCeti.RegularFormClass.rank_one {K : Type u} [Field K] : rank 1 = 1

The multiplicative unit has rank one.

The class of a tensor product

theorem QuadraticMap.Nondegenerate.tmul {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : Nondegenerate) (hR : Nondegenerate) : Nondegenerate

The tensor product of two regular finite-dimensional quadratic forms is regular.

@[simp]

theorem TauCeti.formClass_tmul {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) : formClass (Q.tmul R) ⋯ = formClass Q hQ * formClass R hR

The class of a tensor product is the product of the classes of its factors.

theorem TauCeti.formClass_smul {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (a : Kˣ) (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : formClass (↑a • Q) ⋯ = ⟦⟨1, fun (x : Fin 1) => a⟩⟧ * formClass Q hQ

The class of the scalar multiple a • Q of a regular form by a unit a is the product of the class of Q with the rank-one class ⟨a⟩.