Commit 2024-12-09 13:51 b202b867

feat: non-degeneracy of root pairing form without assuming ordered scalars (#19767) The motivation, and headline item is the new lemma RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic which establishes non-degeneracy of the root form without assuming ordered scalars, at the cost of requiring the crystallographic assumption and field coefficients. Since we also want to keep the old lemma (renamed to) RootPairing.rootForm_restrict_nondegenerate_of_ordered which establishes the same result over an ordered ring, we need to do some work in order to unify things as much as possible. With this in mind I have:

• Turned RootPairing.IsCrystallographic into a typeclass
• Introduced RootPairing.IsAnisotropic (which I've just made up but seems to be a good way to unify things; I also considered the idea that the pairing should take values in an ordered subring but decided this was inferior) In order to prove the new results, a certain amount of API for bilinear forms needed to be added. This also enabled me to golf some of the proofs of the existing non-degeneracy result (for order scalars). I also included a small amount of golfing / moving, and to standardise on LinearMap.ker P.RootForm rather than LinearMap.ker P.Polarisation (since it interfaced better with the bilinear form API). As compensation I added the convenience lemma RootPairing.ker_polarization_eq_ker_rootForm.