Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.Dyadic.RankTwo.Basic

The rank-two dyadic generators u^{(2)}(2^k) and v^{(2)}(2^k) #

On (ℤ/2^k)² this file constructs the two finite quadratic modules

u:  q(x) = x₁x₂ / 2^k,            b(x, y) = (x₁y₂ + y₁x₂) / 2^k,
v:  q(x) = (x₁² + x₁x₂ + x₂²) / 2^k,  b(x, y) = (2x₁y₁ + x₁y₂ + y₁x₂ + 2x₂y₂) / 2^k.

For k ≥ 1 these are Nikulin's rank-two dyadic generators u^{(2)}(2^k) and v^{(2)}(2^k). In the half-norm convention they are, up to isometry, the discriminant forms of the 2-adic lattices with Gram matrices 2^k·A for A = !![0,1;1,0] and A = !![2,1;1,2]. The modules constructed here have pairing matrix A / 2^k in the coordinate basis, whereas the discriminant form of 2^k·A has pairing matrix A⁻¹ / 2^k in the dual basis. For A = !![0,1;1,0] these coincide. For A = !![2,1;1,2] they differ, but A⁻¹ is congruent to A over ℤ₂ (since det A = 3 is a 2-adic unit), so a change of basis is an isometry between them. Together with the cyclic generators q_θ^{(p)}(p^k) they generate every nondegenerate finite quadratic module under orthogonal sum; at p = 2 the two rank-two forms are needed because a 2-adic lattice of type II need not be diagonalizable.

The first coordinate axis of u is a quadratic Lagrangian, so u is metabolic.

Both forms are presented as compositions of a ℤ/2^k-valued quadratic map with the injection ZMod.toRatAddCircle of ℤ/2^k into ℚ/ℤ, so their values are honest residues and no lifting argument is needed. Both are nondegenerate for every k: for u pairing with the two coordinate vectors recovers the coordinates, and for v it recovers 2x₁ + x₂ and x₁ + 2x₂, which determine x because 3 is a unit modulo 2^k.

Main declarations #

References #

u^{(2)}(2^k) #

source
noncomputable def TauCeti.FiniteQuadraticModule.dyadicU (k : ℕ) :
FiniteQuadraticModule

The group (ℤ/2^k)² with quadratic form q(x) = x₁x₂ / 2^k and pairing b(x, y) = (x₁y₂ + y₁x₂) / 2^k. For k ≥ 1 this is Nikulin's dyadic generator u^{(2)}(2^k), the discriminant form of the 2-adic lattice with Gram matrix 2^k·!![0,1;1,0], the hyperbolic plane scaled by 2^k.

Instances For
    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.dyadicU_quadratic (k : ℕ) (x : ZMod (2 ^ k) × ZMod (2 ^ k)) :
    (dyadicU k).quadratic x = (ZMod.toRatAddCircle (2 ^ k)) (x.1 * x.2)

    The quadratic form of u^{(2)}(2^k) is x ↦ x₁x₂ / 2^k.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.dyadicU_pairing (k : ℕ) (x y : ZMod (2 ^ k) × ZMod (2 ^ k)) :
    ((dyadicU k).pairing x) y = (ZMod.toRatAddCircle (2 ^ k)) (x.1 * y.2 + y.1 * x.2)

    The pairing of u^{(2)}(2^k) is (x, y) ↦ (x₁y₂ + y₁x₂) / 2^k.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.natCard_dyadicU (k : ℕ) :
    Nat.card (dyadicU k).carrier = 2 ^ k * 2 ^ k

    u^{(2)}(2^k) has 2^k · 2^k elements. Its carrier is (ℤ/2^k)² by definition.

    source
    theorem TauCeti.FiniteQuadraticModule.dyadicU_one_quadratic_add_self_eq_zero (x : ZMod (2 ^ 1) × ZMod (2 ^ 1)) :
    (dyadicU 1).quadratic x + (dyadicU 1).quadratic x = 0

    The quadratic form of u^{(2)}(2) takes values in ½ℤ/ℤ.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.isNondegenerate_dyadicU (k : ℕ) :
    (dyadicU k).IsNondegenerate

    u^{(2)}(2^k) is nondegenerate: pairing with the two coordinate vectors recovers the two coordinates.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.isLagrangian_dyadicU_top_prod_bot (k : ℕ) :
    (dyadicU k).IsLagrangian (⊤.prod ⊥)

    The first coordinate axis of u^{(2)}(2^k) is a quadratic Lagrangian.

    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.isMetabolic_dyadicU (k : ℕ) :
    (dyadicU k).IsMetabolic

    The dyadic hyperbolic generators are metabolic, including the trivial module at k = 0.

    v^{(2)}(2^k) #

    source
    noncomputable def TauCeti.FiniteQuadraticModule.dyadicV (k : ℕ) :
    FiniteQuadraticModule

    The group (ℤ/2^k)² with quadratic form q(x) = (x₁² + x₁x₂ + x₂²) / 2^k and pairing b(x, y) = (2x₁y₁ + x₁y₂ + y₁x₂ + 2x₂y₂) / 2^k. For k ≥ 1 this is Nikulin's dyadic generator v^{(2)}(2^k), the discriminant form of the 2-adic lattice with Gram matrix 2^k·!![2,1;1,2].

    Instances For
      source
      @[simp]
      theorem TauCeti.FiniteQuadraticModule.dyadicV_quadratic (k : ℕ) (x : ZMod (2 ^ k) × ZMod (2 ^ k)) :
      (dyadicV k).quadratic x = (ZMod.toRatAddCircle (2 ^ k)) (x.1 ^ 2 + x.1 * x.2 + x.2 ^ 2)

      The quadratic form of v^{(2)}(2^k) is x ↦ (x₁² + x₁x₂ + x₂²) / 2^k.

      source
      @[simp]
      theorem TauCeti.FiniteQuadraticModule.dyadicV_pairing (k : ℕ) (x y : ZMod (2 ^ k) × ZMod (2 ^ k)) :
      ((dyadicV k).pairing x) y = (ZMod.toRatAddCircle (2 ^ k)) (2 * x.1 * y.1 + x.1 * y.2 + y.1 * x.2 + 2 * x.2 * y.2)

      The pairing of v^{(2)}(2^k) is (x, y) ↦ (2x₁y₁ + x₁y₂ + y₁x₂ + 2x₂y₂) / 2^k.

      source
      @[simp]
      theorem TauCeti.FiniteQuadraticModule.natCard_dyadicV (k : ℕ) :
      Nat.card (dyadicV k).carrier = 2 ^ k * 2 ^ k

      v^{(2)}(2^k) has 2^k · 2^k elements. Its carrier is (ℤ/2^k)² by definition.

      source
      theorem TauCeti.FiniteQuadraticModule.dyadicV_one_quadratic_add_self_eq_zero (x : ZMod (2 ^ 1) × ZMod (2 ^ 1)) :
      (dyadicV 1).quadratic x + (dyadicV 1).quadratic x = 0

      The quadratic form of v^{(2)}(2) takes values in ½ℤ/ℤ.

      source
      @[simp]
      theorem TauCeti.FiniteQuadraticModule.isNondegenerate_dyadicV (k : ℕ) :
      (dyadicV k).IsNondegenerate

      v^{(2)}(2^k) is nondegenerate: pairing with the two coordinate vectors recovers 2x₁ + x₂ and x₁ + 2x₂, which determine x because 3 is a unit modulo 2^k.