Cyclic finite quadratic modules

A ℚ/ℤ-valued quadratic map on ℤ/m is determined by its value on the generator 1, and a value a occurs exactly when m²a = 0 and 2ma = 0. This file makes that presentation available as a construction: given a : ℚ/ℤ satisfying those two torsion conditions, TauCeti.FiniteQuadraticModule.cyclic is the finite quadratic module on ZMod m with

q(k) = k²a,   b(j, k) = 2jk·a.

The construction is a quotient, not a formula in ZMod.val: the parameter defines the honest ℤ-bilinear map (x, y) ↦ xy·a on ℤ, its associated quadratic map x ↦ x²a has the kernel of the reduction ℤ → ℤ/m inside its radical exactly under the two torsion hypotheses, and QuadraticMap.liftOfSurjective descends it. The hypotheses are therefore not technical: m²a = 0 is the statement that the quadratic value of the generator is well defined modulo m, and 2ma = 0 the corresponding statement for the pairing. Neither implies the other: for m = 1 and a = 1/2 the second holds (2a = 0) and the first fails (a = 1/2), while for m = 3 and a = 1/9 the first holds (9a = 0) and the second fails (6a = 2/3). No witness of the latter kind has m = 2, where the two coefficients m² = 4 and 2m = 4 agree.

The companion TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator turns an additive equivalence ℤ/m ≃+ A matching the single generator value into an isometry onto A, which is how a cyclic discriminant form is identified. It needs no hypothesis beyond that one value, because an additive equivalence out of a cyclic group is determined by the image of the generator.

The rank-two analogue, presenting a form on the Klein four-group by its three nonzero values, is TauCeti.FiniteQuadraticModule.kleinFour in TauCeti.LinearAlgebra.FiniteBilinearModule.KleinFour.

Main declarations

• TauCeti.FiniteQuadraticModule.cyclicMap: the quadratic map on ZMod m whose generator has the prescribed value.
• TauCeti.FiniteQuadraticModule.cyclic: the resulting finite quadratic module.
• TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator: an additive equivalence matching the generator value is an isometry.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1 for discriminant forms and §1.8 for the cyclic forms written q_θ^{(p)} in the full-norm convention.
• W. Ebeling, Lattices and Codes, Chapter 1.

This is part of Layer 3 of TauCetiRoadmap/IntegralLattices/README.md.

The presenting quadratic map on ℤ

Reduction modulo m

The quadratic module

noncomputable def TauCeti.FiniteQuadraticModule.cyclicMap (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) : QuadraticMap ℤ (ZMod m) (AddCircle 1)

The quadratic map on ℤ/m sending the generator 1 to a.

Equations

• TauCeti.FiniteQuadraticModule.cyclicMap m a hq hp = (TauCeti.FiniteQuadraticModule.cyclicAux✝ a).liftOfSurjective (TauCeti.FiniteQuadraticModule.zmodProj✝ m) ⋯ ⋯

theorem TauCeti.FiniteQuadraticModule.cyclicMap_intCast (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) (k : ℤ) : (cyclicMap m a hq hp) ↑k = (k * k) • a

The value of cyclicMap on the reduction of an integer.

@[simp]

theorem TauCeti.FiniteQuadraticModule.cyclicMap_one (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) : (cyclicMap m a hq hp) 1 = a

theorem TauCeti.FiniteQuadraticModule.polar_cyclicMap_intCast (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) (j k : ℤ) : QuadraticMap.polar ⇑(cyclicMap m a hq hp) ↑j ↑k = (2 * (j * k)) • a

The pairing of two reductions of integers.

noncomputable def TauCeti.FiniteQuadraticModule.cyclic (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) [NeZero m] : FiniteQuadraticModule

The finite quadratic module on ℤ/m whose generator has value a.

Equations

• TauCeti.FiniteQuadraticModule.cyclic m a hq hp = TauCeti.FiniteQuadraticModule.ofQuadraticMap (TauCeti.FiniteQuadraticModule.cyclicMap m a hq hp)

@[simp]

theorem TauCeti.FiniteQuadraticModule.cyclic_quadratic (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) [NeZero m] (x : ZMod m) : (cyclic m a hq hp).quadratic x = (cyclicMap m a hq hp) x

@[simp]

theorem TauCeti.FiniteQuadraticModule.cyclic_pairing (m : ℕ) (a : AddCircle 1) (hq : (↑m * ↑m) • a = 0) (hp : (2 * ↑m) • a = 0) [NeZero m] (x y : ZMod m) : ((cyclic m a hq hp).pairing x) y = QuadraticMap.polar (⇑(cyclicMap m a hq hp)) x y

noncomputable def TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator (m : ℕ) {A : Type u_1} [AddCommGroup A] (q : QuadraticMap ℤ (ZMod m) (AddCircle 1)) (r : QuadraticMap ℤ A (AddCircle 1)) (e : ZMod m ≃+ A) (h : r (e 1) = q 1) : q.IsometryEquiv r

An additive equivalence from ℤ/m matching the generator value is an isometry.

No hypothesis beyond that single value is needed. Both forms are stated as bare quadratic maps so that the construction applies before either is packaged as a finite quadratic module.

Equations

• TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator m q r e h = { toLinearEquiv := e.toIntLinearEquiv, map_app' := ⋯ }

@[simp]

theorem TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator_toAddEquiv (m : ℕ) {A : Type u_1} [AddCommGroup A] (q : QuadraticMap ℤ (ZMod m) (AddCircle 1)) (r : QuadraticMap ℤ A (AddCircle 1)) (e : ZMod m ≃+ A) (h : r (e 1) = q 1) : (cyclicIsometryOfGenerator m q r e h).toAddEquiv = e

The underlying additive equivalence of cyclicIsometryOfGenerator is the given one.

@[simp]

theorem TauCeti.FiniteQuadraticModule.cyclicIsometryOfGenerator_apply (m : ℕ) {A : Type u_1} [AddCommGroup A] (q : QuadraticMap ℤ (ZMod m) (AddCircle 1)) (r : QuadraticMap ℤ A (AddCircle 1)) (e : ZMod m ≃+ A) (h : r (e 1) = q 1) (x : ZMod m) : (cyclicIsometryOfGenerator m q r e h) x = e x