The discriminant and the signed discriminant of a regular quadratic form #
Over a field in which two is invertible, a regular quadratic form is diagonalizable, and the
product of the weights of a diagonalization is well defined modulo squares. That square class is
the discriminant d(q); correcting it by the sign (-1)^{m(m-1)/2} in rank m gives the
signed discriminant d±(q), the variant that vanishes on a hyperbolic plane and is unchanged
by adding one.
Both invariants are defined on TauCeti.RegularFormClass, the carrier of isometry classes of
regular forms, so they are invariants of a form up to isometry by construction. Well-definedness
is a Gram-determinant computation: the Gram matrix of a diagonal presentation in the standard
basis is the diagonal matrix of its weights, and an isometry of the coordinate spaces changes that
matrix by a congruence, hence changes its determinant — the product of the weights — by the square
of a unit.
The sign is recorded as m.choose 2 rather than as the truncated quotient m * (m - 1) / 2; the
two agree by Nat.choose_two_right, and only the parity matters, because the square-class group
is killed by two.
Main definitions #
TauCeti.RegularFormClass.discrandTauCeti.RegularFormClass.discrHom: the discriminant of an isometry class, and its packaging as an additive homomorphism for the orthogonal sum.TauCeti.RegularFormClass.signedDiscr: the signed discriminant.
Main results #
TauCeti.squareClass_prod_eq_of_equivalent: isometric diagonal presentations have weight products in the same square class.TauCeti.equivalent_presentedForm_hyperbolicPlane_of_squareClass_prod_eq_neg_one: a binary presentation whose weight product has square class[-1]presents a hyperbolic plane.TauCeti.RegularFormClass.discr_addandTauCeti.RegularFormClass.discr_mul: the discriminant of an orthogonal sum is the sum of the discriminants, and the discriminant of a tensor product of classes of ranksmandnisd(q)^n d(r)^m.TauCeti.RegularFormClass.signedDiscr_addandTauCeti.RegularFormClass.signedDiscr_mul: the signed discriminant of an orthogonal sum picks up the sign(-1)^{mn}, and that of a tensor product is(-1)^{mn(mn-1)/2} d(q)^n d(r)^m.TauCeti.discr_formClass_eq_squareClass: the discriminant of a regular form is the square class of its Gram determinant in any basis.TauCeti.RegularFormClass.discr_mk_rankOne_mulandTauCeti.RegularFormClass.signedDiscr_mk_rankOne_mul: scaling byaaddsm • squareClass ato the (signed) discriminant of a class of rankm.TauCeti.RegularFormClass.discr_mk_rankOne_mul_of_evenandTauCeti.RegularFormClass.signedDiscr_mk_rankOne_mul_of_even: scaling a class of even rank leaves its (signed) discriminant unchanged.TauCeti.RegularFormClass.discr_mk_rankOne_add: adjoining the line⟨a⟩addssquareClass ato the discriminant.TauCeti.RegularFormClass.eq_one_of_rank_eq_one_of_discr_eq_zero: a rank-one class of trivial discriminant is⟨1⟩.TauCeti.RegularFormClass.mk_rankOne_mul_self: scaling twice by the same unit is the identity,⟨a⟩ ⊗ ⟨a⟩ ≅ ⟨1⟩.TauCeti.RegularFormClass.exists_eq_mk_neg_neg_mul: a rank-three class with trivial discriminant has a presentation⟨-a, -b, ab⟩.TauCeti.RegularFormClass.signedDiscr_mk_rankOne:d±⟨a⟩ = squareClass a.TauCeti.RegularFormClass.discr_hyperbolicClassandTauCeti.RegularFormClass.signedDiscr_hyperbolicClass: the discriminant of a hyperbolic plane is the class of-1, and its signed discriminant is trivial.TauCeti.RegularFormClass.signedDiscr_add_hyperbolicClass: adding a hyperbolic plane leaves the signed discriminant unchanged.TauCeti.RegularFormClass.eq_hyperbolicClass_of_rank_eq_two_of_discr_eq_neg_one: a binary class of discriminant[-1]is the hyperbolic class.
References #
- T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter II, §2.
- O. T. O'Meara, Introduction to Quadratic Forms (1973), §58.
The discriminant of a diagonal presentation #
Isometric diagonal presentations have weight products in the same square class, which is what makes the discriminant an invariant of an isometry class.
A binary regular-form presentation whose weight product has square class [-1] presents a
hyperbolic plane.
The discriminant #
The discriminant of an isometry class of regular quadratic forms: the product of the weights of any diagonalization of the form, taken modulo squares.
Instances For
The discriminant of the class of a presentation is the square class of its weight product.
The rank-zero class has trivial discriminant, its weight product being empty.
The discriminant of an orthogonal sum is the sum of the discriminants:
d(q ⊥ r) = d(q) + d(r) in the additively written square-class group.
The discriminant as an additive homomorphism for the orthogonal sum.
Instances For
The discriminant of the orthogonal sum of n copies of a class is n times its
discriminant.
The multiplicative unit ⟨1⟩ has trivial discriminant.
The discriminant of a tensor product: d(q ⊗ r) = n • d(q) + m • d(r) for q of
rank m and r of rank n, in the additively written square-class group.
Scaling by a unit: d(⟨a⟩ ⊗ q) = m • squareClass a + d(q) for q of rank m,
where scaling by a is multiplication by the rank-one class ⟨a⟩.
Adjoining a line: d(⟨a⟩ ⊥ q) = squareClass a + d(q).
A class of rank one and trivial discriminant is the class ⟨1⟩: in rank one the discriminant
is a complete invariant.
A ternary form of trivial discriminant is a pure quaternion norm form: a class of rank
three and trivial discriminant is the class of ⟨-a, -b, ab⟩ for some units a and b.
The signed discriminant #
The signed discriminant d±(q) = m.choose 2 • squareClass (-1) + d(q) of a class of
rank m, in the additively written square-class group. The exponent is recorded as m.choose 2,
which equals m * (m - 1) / 2 by Nat.choose_two_right.
Instances For
The signed discriminant is the discriminant corrected by the sign of its rank. This is the only conversion between the two invariants that later arguments need.
The discriminant is the signed discriminant corrected by the same sign: the correction is its own inverse in the square-class group.
The signed discriminant of the class of a presentation.
In rank at most one the signed discriminant is the discriminant.
The rank-zero class has trivial signed discriminant.
The multiplicative unit ⟨1⟩ has trivial signed discriminant: in rank one the signed
discriminant agrees with the discriminant.
The signed discriminant of a rank-one class ⟨a⟩ is the class of a.
The signed discriminant of an orthogonal sum:
d±(q ⊥ r) = mn • squareClass (-1) + d±(q) + d±(r) for q of rank m and r of rank
n, in the additively written square-class group. The cross term is what the unsigned
discriminant misses.
The signed discriminant of a tensor product:
d±(q ⊗ r) = (mn).choose 2 • squareClass (-1) + n • d(q) + m • d(r) for q of rank m
and r of rank n, in the additively written square-class group.
Scaling by a unit: d±(⟨a⟩ ⊗ q) = m • squareClass a + d±(q) for q of rank
m, where scaling by a is multiplication by the rank-one class ⟨a⟩.
Scaling a class of even rank by a unit does not change its signed discriminant.
Regular forms and the standard examples #
The discriminant of a regular form is computed by any of its diagonalizations.
The discriminant of a regular weighted sum of squares is the square class of the product of its weights.
The discriminant is the Gram determinant modulo squares: the discriminant of a regular
form is the square class of the determinant QuadraticForm.discr b Q of its Gram matrix in any
basis b.
The signed discriminant of a regular form is computed by any of its diagonalizations.
The discriminant of the hyperbolic class is the class of -1.
A class of rank two whose discriminant is the class of -1 is the hyperbolic class: in rank
two the discriminant is a complete invariant of hyperbolicity.
The signed discriminant of the hyperbolic class is trivial. The unsigned discriminant is
the class of -1, which is nontrivial precisely when -1 is not a square.
Adding a hyperbolic plane leaves the signed discriminant unchanged. The cross term of
TauCeti.RegularFormClass.signedDiscr_add is an even multiple of the class of -1, so it
vanishes. The unsigned discriminant instead picks up the class of -1 each time.
Adding any number of hyperbolic planes leaves the signed discriminant unchanged.
A regular form over an extension L of K, whose discriminant is induced by the square class
of a unit d of K, is equivalent to a diagonal form whose coefficient product differs from the
image of d by a square.