Shortest vectors in the discriminant cosets of Aₙ

The discriminant group of the root lattice Aₙ is cyclic of order n + 1, generated by the class of the first fundamental weight ω₁; the class [k] = k ω₁ is the Conway–Sloane glue label k of an Aₙ component. This file computes the minimum norm of every class:

min {⟨x, x⟩ | x ∈ Aₙ^∨, x + Aₙ = k ω₁ + Aₙ} = k (n + 1 - k) / (n + 1)      (0 ≤ k ≤ n + 1).

The computation takes place in the classical coordinates Aₙ = {y ∈ ℤ^{n+1} | ∑ yⱼ = 0}, in which ω₁ is e₀ - (1 / (n + 1)) (1, …, 1). A vector of the class k ω₁ is then a vector y of coordinate sum zero with yⱼ = mⱼ - k / (n + 1) for integers mⱼ, and the coordinate sum forces ∑ mⱼ = k. Expanding the squares gives the exact identity

∑ yⱼ² = k (n + 1 - k) / (n + 1) + ∑ mⱼ (mⱼ - 1),

whose error term is a sum of the nonnegative integers mⱼ (mⱼ - 1). So the displayed value is a lower bound, and it is attained exactly when every mⱼ is 0 or 1: the minimal vectors of the class are the vectors with k coordinates equal to (n + 1 - k) / (n + 1) and the remaining n + 1 - k coordinates equal to -k / (n + 1).

The minima are stated as IsLeast over the norms of the actual dual-lattice vectors in each discriminant class, so they record attainment as well as the lower bound. They are the shortest-norm values attached to the glue labels of an Aₙ component, the input for bounding the norm of a glue vector in an orthogonal sum of root lattices.

Main results

• TauCeti.IntegralLattice.dotProduct_self_eq_mul_sub_div_add_sum: the exact norm identity ∑ xⱼ² = k (n + 1 - k) / (n + 1) + ∑ mⱼ (mⱼ - 1) in classical coordinates.
• TauCeti.IntegralLattice.mul_sub_div_le_dotProduct_self: a vector of ℚ^{n+1} of coordinate sum zero with coordinates in ℤ - k / (n + 1) has norm at least k (n + 1 - k) / (n + 1).
• TauCeti.IntegralLattice.dotProduct_self_eq_mul_sub_div_iff: equality holds exactly when all coordinates are -k / (n + 1) or 1 - k / (n + 1).
• TauCeti.IntegralLattice.exists_mk_eq_nsmul_typeAFundamentalWeightClass_and_apply_eq: the class k ω₁ contains a dual vector with these minimal classical coordinates.
• TauCeti.IntegralLattice.isLeast_form_self_nsmul_typeAFundamentalWeightClass: the minimum norm of the class k ω₁ is k (n + 1 - k) / (n + 1) for k ≤ n + 1.
• TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquiv: the same minimum, indexed by the label a : ZMod (n + 1) of the class.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §6.1 and Chapter 16, §1.

The coset bound in classical coordinates

theorem TauCeti.IntegralLattice.dotProduct_self_eq_mul_sub_div_add_sum {n : ℕ} {k : ℤ} {x : Fin (n + 1) → ℚ} (hx : ∑ j : Fin (n + 1), x j = 0) {m : Fin (n + 1) → ℤ} (hm : ∀ (j : Fin (n + 1)), x j = ↑(m j) - ↑k / (↑n + 1)) : x ⬝ᵥ x = ↑k * (↑n + 1 - ↑k) / (↑n + 1) + ∑ j : Fin (n + 1), ↑(m j) * (↑(m j) - 1)

The norm identity of the cosets of Aₙ. If x has coordinate sum zero and xⱼ = mⱼ - k / (n + 1) with integers mⱼ, then ∑ xⱼ² = k (n + 1 - k) / (n + 1) + ∑ mⱼ (mⱼ - 1).

theorem TauCeti.IntegralLattice.mul_sub_div_le_dotProduct_self {n : ℕ} {k : ℤ} {x : Fin (n + 1) → ℚ} (hx : ∑ j : Fin (n + 1), x j = 0) (hint : ∀ (j : Fin (n + 1)), ∃ (m : ℤ), x j = ↑m - ↑k / (↑n + 1)) : ↑k * (↑n + 1 - ↑k) / (↑n + 1) ≤ x ⬝ᵥ x

The coset bound for Aₙ in classical coordinates. A vector of ℚ^{n+1} with coordinate sum zero whose coordinates all lie in ℤ - k / (n + 1) has norm at least k (n + 1 - k) / (n + 1).

theorem TauCeti.IntegralLattice.dotProduct_self_eq_mul_sub_div_iff {n : ℕ} {k : ℤ} {x : Fin (n + 1) → ℚ} (hx : ∑ j : Fin (n + 1), x j = 0) (hint : ∀ (j : Fin (n + 1)), ∃ (m : ℤ), x j = ↑m - ↑k / (↑n + 1)) : x ⬝ᵥ x = ↑k * (↑n + 1 - ↑k) / (↑n + 1) ↔ ∀ (j : Fin (n + 1)), x j = -(↑k / (↑n + 1)) ∨ x j = 1 - ↑k / (↑n + 1)

The vectors attaining the coset bound for Aₙ. A vector of ℚ^{n+1} with coordinate sum zero whose coordinates all lie in ℤ - k / (n + 1) has norm k (n + 1 - k) / (n + 1) exactly when each of its coordinates is -k / (n + 1) or 1 - k / (n + 1).

The discriminant classes of the root lattice

theorem TauCeti.IntegralLattice.exists_mk_eq_nsmul_typeAFundamentalWeightClass_and_apply_eq {n k : ℕ} (hk : k ≤ n + 1) : ∃ (x : ↥(typeARootLattice n).dualCarrier), Submodule.Quotient.mk x = k • typeAFundamentalWeightClass n ∧ ∀ (j : Fin (n + 1)), ↑((typeAIsometryZeroSumLattice n) ↑x) j = (if ↑j < k then 1 else 0) - ↑k / (↑n + 1)

A minimal vector of the discriminant class k ω₁ of Aₙ. For 0 ≤ k ≤ n + 1, the class k ω₁ contains a dual vector whose classical coordinates are 1 - k / (n + 1) in the first k places and -k / (n + 1) in the others.

theorem TauCeti.IntegralLattice.isLeast_form_self_nsmul_typeAFundamentalWeightClass {n k : ℕ} (hk : k ≤ n + 1) : IsLeast {q : ℚ | ∃ (x : ↥(typeARootLattice n).dualCarrier), Submodule.Quotient.mk x = k • typeAFundamentalWeightClass n ∧ ((typeARootLattice n).form ↑x) ↑x = q} (↑k * (↑n + 1 - ↑k) / (↑n + 1))

The minimum norm of the discriminant class k ω₁ of Aₙ is k (n + 1 - k) / (n + 1), for 0 ≤ k ≤ n + 1. It is attained by the dual vector whose classical coordinates are (n + 1 - k) / (n + 1) in the first k places and -k / (n + 1) in the others, and it bounds the norm of every dual vector of the class.

theorem TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquiv {n : ℕ} (a : ZMod (n + 1)) : IsLeast {q : ℚ | ∃ (x : ↥(typeARootLattice n).dualCarrier), Submodule.Quotient.mk x = (typeADiscriminantGroupEquiv n) a ∧ ((typeARootLattice n).form ↑x) ↑x = q} (↑a.val * (↑n + 1 - ↑a.val) / (↑n + 1))

The minimum norm of the discriminant class labelled a : ZMod (n + 1). The class typeADiscriminantGroupEquiv n a = a.val • ω₁ of Aₙ has minimum norm a.val (n + 1 - a.val) / (n + 1), the shortest norm of the Conway–Sloane glue label [a] of an Aₙ component.