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.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.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.

Equations

• p.tmul q = ⟨p.fst * q.fst, fun (k : Fin (p.fst * q.fst)) => p.snd (finProdFinEquiv.symm k).1 * q.snd (finProdFinEquiv.symm k).2⟩

@[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.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• TauCeti.RegularFormPresentation.one = ⟨1, fun (x : Fin 1) => 1⟩

@[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.

Equations

• TauCeti.presentedFormOneIsometryEquiv = { toLinearEquiv := LinearEquiv.funUnique (Fin 1) K K, map_app' := ⋯ }

@[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] [Invertible 2] (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.

Equations

• TauCeti.instMulRegularFormClass = { mul := Quotient.map₂ TauCeti.RegularFormPresentation.tmul ⋯ }

@[instance_reducible]

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

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

Equations

• TauCeti.instOneRegularFormClass = { one := ⟦TauCeti.RegularFormPresentation.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.

@[instance_reducible]

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

Tensor product makes regular-form classes a commutative monoid.

Equations

• One or more equations did not get rendered due to their size.

@[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.