The standard finite bilinear and quadratic modules on ℤ/m

The cyclic group ℤ/m carries a canonical ℚ/ℤ-valued pairing

b(x, y) = xy / m,

obtained from the injection ZMod.toRatAddCircle of ℤ/m onto the m-torsion of ℚ/ℤ. It is symmetric and nondegenerate, and it is the discriminant pairing of the rank-one lattice whose Gram matrix is (m).

When m is even this pairing is the polar form of the quadratic map

q(x) = x² / (2m),

the half-norm of the same rank-one lattice. Evenness is exactly the condition for q to be well defined: replacing an integer lift a by a + km changes a² by 2akm + k²m², which divided by 2m is ak + k²m/2, an integer for all a and k precisely when m is even. The quadratic map is therefore constructed from the cyclic presentation TauCeti.FiniteQuadraticModule.cyclic, whose two torsion hypotheses hold for the generator value 1 / (2m) exactly when m is even and m ≠ 0.

These are the alphabets in which a code over ℤ/m becomes a subgroup of a discriminant module: the pairing of two words is the dot product of the words divided by m, and the quadratic value of a word is the sum of the squares of its coordinate lifts divided by 2m.

Main declarations

• TauCeti.FiniteBilinearModule.zmodStandard: the pairing xy / m on ℤ/m.
• TauCeti.FiniteBilinearModule.isNondegenerate_zmodStandard: that pairing is nondegenerate.
• TauCeti.FiniteQuadraticModule.zmodStandard: for even m, the quadratic map x² / (2m) on ℤ/m, whose polar pairing is the standard one.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1 and §1.8, where these are the cyclic discriminant forms of the rank-one lattices.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3.
• W. Ebeling, Lattices and Codes, §§1.2–1.3.

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.zmodStandard (m : ℕ) [NeZero m] : FiniteBilinearModule

The standard finite bilinear module on ℤ/m, with pairing b(x, y) = xy / m.

It is the discriminant form of the rank-one lattice with Gram matrix (m), and the alphabet in which an additive code over ℤ/m is a subgroup of a discriminant module.

Reducible, as TauCeti.FiniteBilinearModule.coordinatePower is, so that its carrier is the type ℤ/m itself and additive codes are directly subgroups of its coordinate powers.

@[simp]

theorem TauCeti.FiniteBilinearModule.zmodStandard_pairing (m : ℕ) [NeZero m] (x y : ZMod m) : ((zmodStandard m).pairing x) y = (ZMod.toRatAddCircle m) (x * y)

The standard pairing of two residues is the image of their product under the injection of ℤ/m into ℚ/ℤ.

theorem TauCeti.FiniteBilinearModule.zmodStandard_pairing_intCast (m : ℕ) [NeZero m] (j k : ℤ) : ((zmodStandard m).pairing ↑j) ↑k = ↑(↑j * ↑k / ↑m)

The standard pairing of two residues, computed on integer lifts.

theorem TauCeti.FiniteBilinearModule.zmodStandard_pairing_val (m : ℕ) [NeZero m] (x y : ZMod m) : ((zmodStandard m).pairing x) y = ↑(↑x.val * ↑y.val / ↑m)

The standard pairing of two residues, computed on canonical representatives.

@[simp]

theorem TauCeti.FiniteBilinearModule.zmodStandard_pairing_eq_zero_iff (m : ℕ) [NeZero m] (x y : ZMod m) : ((zmodStandard m).pairing x) y = 0 ↔ x * y = 0

Two residues are orthogonal for the standard pairing exactly when their product vanishes.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_zmodStandard (m : ℕ) [NeZero m] : (zmodStandard m).IsNondegenerate

The standard pairing on ℤ/m is nondegenerate: pairing with the generator 1 recovers the residue.

noncomputable def TauCeti.FiniteQuadraticModule.zmodStandardMap (m : ℕ) [NeZero m] (hm : Even m) : QuadraticMap ℤ (ZMod m) (AddCircle 1)

The quadratic map x ↦ x² / (2m) on ℤ/m, defined for even m.

Evenness is exactly what makes the value of the generator well defined modulo m: the two torsion conditions of the cyclic presentation ask that m²/(2m) = m/2 and 2m/(2m) = 1 be integers.

@[simp]

theorem TauCeti.FiniteQuadraticModule.zmodStandardMap_intCast (m : ℕ) [NeZero m] (hm : Even m) (k : ℤ) : (zmodStandardMap m hm) ↑k = ↑(↑k ^ 2 / (2 * ↑m))

The standard quadratic value on the reduction of an integer.

theorem TauCeti.FiniteQuadraticModule.zmodStandardMap_val (m : ℕ) [NeZero m] (hm : Even m) (x : ZMod m) : (zmodStandardMap m hm) x = ↑(↑x.val ^ 2 / (2 * ↑m))

The standard quadratic value on the canonical representative of a residue.

theorem TauCeti.FiniteQuadraticModule.polar_zmodStandardMap (m : ℕ) [NeZero m] (hm : Even m) (x y : ZMod m) : QuadraticMap.polar (⇑(zmodStandardMap m hm)) x y = ((FiniteBilinearModule.zmodStandard m).pairing x) y

The polar form of x² / (2m) is the standard pairing xy / m.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteQuadraticModule.zmodStandard (m : ℕ) [NeZero m] (hm : Even m) : FiniteQuadraticModule

The standard finite quadratic module on ℤ/m for even m, with quadratic map q(x) = x² / (2m).

Its underlying bilinear module is the standard one, so the pairing of residues is xy / m whether or not m is even. It is the discriminant form of the rank-one lattice with Gram matrix (m) in the half-norm convention q(x) = b(x, x) / 2.

Reducible, as the bilinear alphabet and the coordinate powers are, so that its carrier is the type ℤ/m itself.

@[simp]

theorem TauCeti.FiniteQuadraticModule.zmodStandard_quadratic (m : ℕ) [NeZero m] (hm : Even m) (x : ZMod m) : (zmodStandard m hm).quadratic x = (zmodStandardMap m hm) x

The quadratic map of the standard quadratic module is x ↦ x² / (2m).

@[simp]

theorem TauCeti.FiniteQuadraticModule.zmodStandard_toFiniteBilinearModule (m : ℕ) [NeZero m] (hm : Even m) : (zmodStandard m hm).toFiniteBilinearModule = FiniteBilinearModule.zmodStandard m

The polar bilinear module of the standard quadratic module is the standard bilinear module.

theorem TauCeti.FiniteQuadraticModule.isNondegenerate_zmodStandard (m : ℕ) [NeZero m] (hm : Even m) : (zmodStandard m hm).IsNondegenerate

The standard quadratic module on ℤ/m is nondegenerate.