The semiring of regular-form classes

Orthogonal sum and tensor product make the isometry classes of regular finite-dimensional quadratic forms over a field of characteristic different from two into a commutative semiring. The essential compatibility is the isometry distributing tensor product over orthogonal product.

The rank is compatible with both operations, so it is packaged as a semiring homomorphism to the natural numbers. This is the dimension map from which parity invariants can be obtained by composition.

Main results

• TauCeti.instCommSemiringRegularFormClass: the commutative semiring structure.
• TauCeti.RegularFormClass.rankHom: rank as a semiring homomorphism to ℕ.

References

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

Distributivity

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

Tensor product distributes over concatenation of presentations, up to isometry of the presented forms.

The commutative semiring

@[instance_reducible]

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

Orthogonal sum and tensor product make regular-form classes a commutative semiring.

Rank

def TauCeti.RegularFormClass.rankHom {K : Type u} [Field K] [Invertible 2] : RegularFormClass K →+* ℕ

The rank of a regular-form class, as a semiring homomorphism. Orthogonal sum adds ranks and tensor product multiplies them.

@[simp]

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

Applying the rank homomorphism computes the rank.