The hyperbolic form on a module and its dual #
The polar form of QuadraticForm.dualProd K M pairs the two coordinate summands by evaluation.
It is nondegenerate whenever the linear functionals on M separate points, with no assumption
on the characteristic of K or the dimension of M.
The polar form of the hyperbolic form #
@[simp]
theorem
TauCeti.polar_dualProd
{K : Type u_1}
{M : Type u_2}
[CommRing K]
[AddCommGroup M]
[Module K M]
(p q : Module.Dual K M × M)
:
The polar form of the hyperbolic quadratic form Q (f, m) = f m pairs each coordinate
summand with the other and neither with itself.
theorem
TauCeti.nondegenerate_dualProd
{K : Type u_1}
{M : Type u_2}
[CommRing K]
[AddCommGroup M]
[Module K M]
(hM : Function.Injective ⇑(Module.Dual.eval K M))
:
The hyperbolic form is nondegenerate whenever the functionals on M separate points.