Comparing quadratic refinements of finite bilinear modules

Two nondegenerate finite quadratic modules are isometric exactly when their polar bilinear modules are isometric and their Gauss-sum invariants agree. This is Nikulin's Theorem 1.11.3.

Given a bilinear isometry f, the discrepancy q_B(f x) - q_A(x) is an additive character killed by two. Nondegeneracy represents it as b_A(a, x) for a vector a killed by two. Translation by a compares the Gauss sums, so equality of their invariants forces q_A(a) = 0. The additive involution that fixes x when b_A(a, x) = 0 and sends it to x + a otherwise then corrects f to a quadratic isometry. The given bilinear isometry need not itself preserve the quadratic maps.

Main declarations

• TauCeti.FiniteQuadraticModule.isometryOfBilinearIsometry: correct a bilinear isometry between nondegenerate quadratic modules with equal Gauss-sum invariants.
• TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_bilinear_isometry_and_gaussSign_eq: the classification comparison theorem.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Theorem 1.11.3.
• F. Deloup and G. Massuyeau, Quadratic functions on torsion groups, Journal of Pure and Applied Algebra 198 (2005), 105–121, Corollary 4.2 and Lemma 4.3. The proof here follows their isotropic two-torsion correction, in the homogeneous case.

noncomputable def TauCeti.FiniteQuadraticModule.isometryOfBilinearIsometry {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (hA : A.IsNondegenerate) (f : A.Isometry B.toFiniteBilinearModule) (h : A.gaussSign = B.gaussSign) : A.Isometry B

Correct a bilinear isometry to a quadratic isometry. For a nondegenerate source, equal Gauss-sum invariants ensure that an isotropic two-torsion involution corrects the discrepancy. The target is nondegenerate because its polar form is isometric to the source's.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_bilinear_isometry_and_gaussSign_eq {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (hA : A.IsNondegenerate) : Nonempty (A.Isometry B) ↔ Nonempty (A.Isometry B.toFiniteBilinearModule) ∧ A.gaussSign = B.gaussSign

Nikulin's comparison theorem. Two nondegenerate finite quadratic modules are isometric exactly when their polar bilinear modules are isometric and their Gauss-sum invariants agree.