Duality and discriminants of rank-one lattices

For a ≠ 0, the dual of ⟨a⟩ is (1/a)ℤ, and its discriminant group is cyclic of order |a|, generated by g = 1/a + ℤ. Its pairing is b(kg,lg) = kl/a mod ℤ. When a is even, the half-norm quadratic form is q(kg) = k²/(2a) mod ℤ. The level is 2|a|, for odd as well as even a and for either sign.

The quadratic form requires an explicit evenness proof; the pairing, duality, and level calculations do not. The degenerate zero parameter is excluded from these finite-group calculations.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.

theorem TauCeti.IntegralLattice.mem_rankOne_dualCarrier_iff (a : ℤ) [NeZero a] (x : ℚ) : x ∈ (rankOne a).dualCarrier ↔ ∃ (k : ℤ), x = ↑k / ↑a

The dual of ⟨a⟩ consists of the integer multiples of 1/a.

theorem TauCeti.IntegralLattice.rankOne_dualCarrier_eq_span (a : ℤ) [NeZero a] : (rankOne a).dualCarrier = ℤ ∙ 1 / ↑a

The dual of ⟨a⟩ is generated by 1/a as an integral submodule of ℚ.

noncomputable def TauCeti.IntegralLattice.rankOneDualGen (a : ℤ) [NeZero a] : ↥(rankOne a).dualCarrier

The distinguished dual vector 1/a.

@[simp]

theorem TauCeti.IntegralLattice.coe_rankOneDualGen (a : ℤ) [NeZero a] : ↑(rankOneDualGen a) = 1 / ↑a

The rational value of the distinguished dual vector.

theorem TauCeti.IntegralLattice.coe_zsmul_rankOneDualGen (a : ℤ) [NeZero a] (k : ℤ) : ↑(k • rankOneDualGen a) = ↑k / ↑a

Integer multiples of the dual generator have value k/a.

theorem TauCeti.IntegralLattice.exists_zsmul_rankOneDualGen (a : ℤ) [NeZero a] (x : ↥(rankOne a).dualCarrier) : ∃ (k : ℤ), x = k • rankOneDualGen a

Every dual vector is an integer multiple of the distinguished generator.

noncomputable def TauCeti.IntegralLattice.rankOneDualEquiv (a : ℤ) [NeZero a] : ℤ ≃ₗ[ℤ] ↥(rankOne a).dualCarrier

The dual of ⟨a⟩ is free of rank one on 1/a.

@[simp]

theorem TauCeti.IntegralLattice.coe_rankOneDualEquiv (a : ℤ) [NeZero a] (k : ℤ) : ↑((rankOneDualEquiv a) k) = ↑k / ↑a

The dual equivalence sends k to k/a.

@[simp]

theorem TauCeti.IntegralLattice.rankOneDualEquiv_one (a : ℤ) [NeZero a] : (rankOneDualEquiv a) 1 = rankOneDualGen a

The dual equivalence sends 1 to the distinguished generator.

theorem TauCeti.IntegralLattice.comap_rankOneDualEquiv_carrierInDual (a : ℤ) [NeZero a] : Submodule.comap (↑(rankOneDualEquiv a)) (rankOne a).carrierInDual = Ideal.span {a}

Under the dual equivalence, the original lattice is the ideal generated by a.

noncomputable def TauCeti.IntegralLattice.rankOneClass (a : ℤ) [NeZero a] : (rankOne a).DiscriminantGroup

The distinguished class g = 1/a + ℤ in the discriminant group.

theorem TauCeti.IntegralLattice.zsmul_rankOneClass (a : ℤ) [NeZero a] (k : ℤ) : k • rankOneClass a = Submodule.Quotient.mk (k • rankOneDualGen a)

Multiples of the distinguished class are represented by multiples of the dual generator.

theorem TauCeti.IntegralLattice.span_rankOneClass_eq_top (a : ℤ) [NeZero a] : ℤ ∙ rankOneClass a = ⊤

The distinguished class generates the discriminant group.

noncomputable def TauCeti.IntegralLattice.rankOneDiscriminantEquiv (a : ℤ) [NeZero a] : (rankOne a).DiscriminantGroup ≃+ ZMod a.natAbs

The discriminant group of ⟨a⟩ is cyclic of order |a|.

@[simp]

theorem TauCeti.IntegralLattice.rankOneDiscriminantEquiv_rankOneClass (a : ℤ) [NeZero a] : (rankOneDiscriminantEquiv a) (rankOneClass a) = 1

The cyclic identification sends the distinguished class to 1.

@[simp]

theorem TauCeti.IntegralLattice.rankOneDiscriminantEquiv_zsmul_rankOneClass (a : ℤ) [NeZero a] (k : ℤ) : (rankOneDiscriminantEquiv a) (k • rankOneClass a) = ↑k

The cyclic identification sends kg to the residue of k.

theorem TauCeti.IntegralLattice.natCard_rankOne_discriminantGroup (a : ℤ) [NeZero a] : Nat.card (rankOne a).DiscriminantGroup = a.natAbs

The discriminant group of ⟨a⟩ has |a| elements.

theorem TauCeti.IntegralLattice.discriminantPairing_zsmul_rankOneClass (a : ℤ) [NeZero a] (k l : ℤ) : ((rankOne a).discriminantPairing (k • rankOneClass a)) (l • rankOneClass a) = ↑(↑k * ↑l / ↑a)

The discriminant pairing on arbitrary multiples of the generator.

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_rankOneClass_self (a : ℤ) [NeZero a] : ((rankOne a).discriminantPairing (rankOneClass a)) (rankOneClass a) = ↑(1 / ↑a)

The pairing on the generator is 1/a mod ℤ.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_zsmul_rankOneClass (a : ℤ) [NeZero a] (ha : Even a) (k : ℤ) : ((rankOne a).discriminantQuadraticMap ⋯) (k • rankOneClass a) = ↑(↑k ^ 2 / (2 * ↑a))

For even a, the half-norm quadratic form has value k²/(2a) at kg.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_rankOneClass (a : ℤ) [NeZero a] (ha : Even a) : ((rankOne a).discriminantQuadraticMap ⋯) (rankOneClass a) = ↑(1 / (2 * ↑a))

For even a, the quadratic value of the generator is 1/(2a) mod ℤ.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_level (a : ℤ) [NeZero a] : (rankOne a).level = 2 * a.natAbs

The rank-one lattice has level 2|a|, regardless of parity or sign.