Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.OddCyclic.Basic

The odd cyclic generators q_θ^{(p)}(p^k) #

For an odd natural number m and an integer θ, this file constructs the cyclic group ℤ/m with pairing and quadratic form

b(x, y) = θxy / m,   q(x) = θ(m + 1)x² / (2m).

Since m is odd, (m + 1) / 2 is an integer inverse of 2 modulo m, so 2q(x) = b(x, x) and q takes values in the m-torsion of ℚ/ℤ. It is the only quadratic form on ℤ/m with polar form b, because two such forms differ by an additive map d with 2d = 0, and 2 is invertible on a group of odd order. The naive half-norm θx² / (2m) is not well defined modulo m when θ is odd, and the factor m + 1 repairs it without changing the pairing.

For an odd prime p, k ≥ 1 and θ prime to p, the module on ℤ/p^k is Nikulin's odd cyclic generator q_θ^{(p)}(p^k), the discriminant form of the rank-one p-adic lattice with Gram matrix (θ·p^k). (The natural generator of that discriminant group has pairing value θ⁻¹/p^k, and θ⁻¹ = θ·(θ⁻¹)² lies in the square class of θ.) Nikulin's classification of nondegenerate finite quadratic modules writes the odd-primary part of every such module as an orthogonal sum of these. The form is nondegenerate exactly when θ is prime to m.

Main declarations #

References #

source
noncomputable def TauCeti.FiniteQuadraticModule.oddCyclic (m : ℕ) (hm : Odd m) (θ : ℤ) :
FiniteQuadraticModule

The cyclic group ℤ/m, for odd m, with pairing b(x, y) = θxy / m and quadratic form q(x) = θ(m + 1)x² / (2m), the unique quadratic form with polar b. For m = p^k with p an odd prime, k ≥ 1 and θ prime to p, this is Nikulin's odd cyclic generator q_θ^{(p)}(p^k), the discriminant form of the rank-one p-adic lattice with Gram matrix (θ·p^k). It is nondegenerate exactly when θ is prime to m.

Instances For
    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.natCard_oddCyclic (m : ℕ) (hm : Odd m) (θ : ℤ) :
    Nat.card (oddCyclic m hm θ).carrier = m

    The order of oddCyclic m hm θ is m: its carrier is ZMod m by definition.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.oddCyclic_quadratic_intCast (m : ℕ) (hm : Odd m) (θ j : ℤ) :
    (oddCyclic m hm θ).quadratic ↑j = ↑(↑θ * (↑m + 1) * ↑j ^ 2 / (2 * ↑m))

    The quadratic form of oddCyclic m hm θ on the reduction of an integer j is θ(m + 1)j² / (2m).

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.oddCyclic_pairing_intCast (m : ℕ) (hm : Odd m) (θ i j : ℤ) :
    ((oddCyclic m hm θ).pairing ↑i) ↑j = ↑(↑θ * ↑i * ↑j / ↑m)

    The pairing of oddCyclic m hm θ on the reductions of integers i and j is θij / m.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.oddCyclic_pairing (m : ℕ) (hm : Odd m) (θ : ℤ) (x y : ZMod m) :
    ((oddCyclic m hm θ).pairing x) y = (ZMod.toRatAddCircle m) (↑θ * x * y)

    The odd cyclic pairing is multiplication of residue classes followed by the rational-circle character.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.oddCyclic_quadratic (m : ℕ) (hm : Odd m) (θ : ℤ) (x : ZMod m) :
    (oddCyclic m hm θ).quadratic x = (ZMod.toRatAddCircle m) (↑θ * ↑((m + 1) / 2) * x ^ 2)

    The odd cyclic quadratic form is the rational-circle character of θx²/2, with division by 2 performed using its integer inverse (m + 1) / 2 modulo m.

    source
    theorem TauCeti.FiniteQuadraticModule.pow_nsmul_oddCyclic_quadratic {p : ℕ} (hp : Odd p) (j e : ℕ) (θ : ℤ) (x : ZMod (p ^ (j + e))) :
    p ^ j • (oddCyclic (p ^ (j + e)) ⋯ θ).quadratic x = (oddCyclic (p ^ e) ⋯ θ).quadratic ((ZMod.castHom ⋯ (ZMod (p ^ e))) x)

    Scaling the form of q_θ^{(p)}(p^{j+e}) by p^j is the form of q_θ^{(p)}(p^e) read through the reduction modulo p^e.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.isNondegenerate_oddCyclic_iff (m : ℕ) (hm : Odd m) (θ : ℤ) :
    (oddCyclic m hm θ).IsNondegenerate ↔ IsCoprime (↑m) θ

    oddCyclic m hm θ is nondegenerate exactly when θ is prime to m. If d > 1 divides both, the nonzero element m / d lies in the radical.