Alternating quadratic modules on the Klein four-group

A nondegenerate finite quadratic module on a Klein four-group whose polar pairing is alternating is isometric to one of the two rank-two dyadic generators of exponent two: u¹ = u⁽²⁾(2) or v¹ = v⁽²⁾(2). This is the first rank-two case in the dyadic generator decomposition. It is also the point at which the two rank-two families become necessary: neither alternating form has a nondegenerate cyclic subgroup.

Choose any two distinct nonzero generators x, y. Nondegeneracy and alternation force b(x, y) = 1/2. Each of q(x) and q(y) is either 0 or 1/2. If both are 1/2, all three nonzero vectors have value 1/2, giving v¹. Otherwise a shear of the chosen basis makes both basis vectors isotropic, giving u¹.

Main declaration

• TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicU_or_dyadicV_of_isAddKleinFour: classification of the nondegenerate alternating quadratic modules on a Klein four-group.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Proposition 1.8.1.
• C. T. C. Wall, Quadratic forms on finite groups, and related topics, Topology 2 (1963), 281–298.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicU_or_dyadicV_of_isAddKleinFour (A : FiniteQuadraticModule) [IsAddKleinFour A.carrier] (hA : A.IsNondegenerate) (hAlt : ∀ (x : A.carrier), (A.pairing x) x = 0) : Nonempty ((dyadicU 1).Isometry A) ∨ Nonempty ((dyadicV 1).Isometry A)

The alternating quadratic modules on the Klein four-group are u¹ and v¹.

If A is nondegenerate, has underlying additive group a Klein four-group, and satisfies b(x, x) = 0 for every x, then A is isometric to u⁽²⁾(2) or to v⁽²⁾(2).