Two-neighbors of the standard lattice without unit vectors

Let L be an integral lattice on ℚⁿ, with the dot product, which is a Kneser two-neighbor of the standard lattice Iₙ = ℤⁿ and contains none of the coordinate vectors eᵢ. Then:

• L ∩ ℤⁿ is the checkerboard lattice Dₙ of integral vectors with even coordinate sum;
• L = Dₙ ∪ (y + Dₙ) for a vector y whose coordinates all lie in ℤ + 1/2;
• 4 ∣ n, because y · y ∈ ℤ while 4 (y · y) = ∑ (2 yᵢ)² ≡ n (mod 4);
• if 8 ∣ n, then L is isometric to the spinor glue lattice Dₙ⁺, and in rank eight it is isometric to the E₈ root lattice.

Besides integrality, the argument only uses that L ∩ ℤⁿ has index two in both lattices. As neither eᵢ nor eⱼ lies in L, their sum does, so yᵢ + yⱼ is an integer for every y ∈ L; a vector y ∈ L ∖ ℤⁿ is therefore half-integral in every coordinate. Pairing with y then shows that a vector of L ∩ ℤⁿ has even coordinate sum, and index two gives the reverse inclusion. Finally y is congruent modulo Dₙ to the spinor (1/2, …, 1/2) or becomes so after changing the sign of one coordinate, and such a sign change preserves Dₙ and the dot product.

The same statements hold for a two-neighbor L of any lattice N given with an isometry Iₙ ≅ N, provided L has no vectors of norm one: moving both lattices to ℚⁿ along the isometry turns the vectors eᵢ into vectors of norm one. A positive definite unimodular lattice with a vector of norm one splits off I₁, and a two-neighbor along a vector of norm four acquires such a vector, so these statements identify a lattice without vectors of norm one from a neighbor isometric to Iₙ.

Main results

• TauCeti.IntegralLattice.exists_forall_mem_carrier_iff_of_isNeighbor_unitLattice: L = Dₙ ∪ (y + Dₙ) with y half-integral.
• TauCeti.IntegralLattice.carrier_inf_eq_checkerboardCarrier_of_isNeighbor_unitLattice: L ∩ ℤⁿ = Dₙ.
• TauCeti.IntegralLattice.four_dvd_of_isNeighbor_unitLattice: 4 ∣ n.
• TauCeti.IntegralLattice.nonempty_isometry_checkerboardPlusLattice_of_isNeighbor_unitLattice: L ≅ Dₙ⁺ when 8 ∣ n.
• TauCeti.IntegralLattice.nonempty_isometry_typeE₈RootLattice_of_isNeighbor_unitLattice: L ≅ E₈ in rank eight.
• TauCeti.IntegralLattice.four_dvd_of_isNeighbor_of_isometry_unitLattice and its companions nonempty_isometry_checkerboardPlusLattice_of_isNeighbor_of_isometry_unitLattice and nonempty_isometry_typeE₈RootLattice_of_isNeighbor_of_isometry_unitLattice: the same for a two-neighbor without vectors of norm one of a lattice isometric to Iₙ.

References

• M. Kneser, Klassenzahlen definiter quadratischer Formen, Arch. Math. 8 (1957), 241--250.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 16, §1, and Chapter 4, §7.3, for the lattices Dₙ⁺.

theorem TauCeti.IntegralLattice.carrier_inf_eq_checkerboardCarrier_of_isNeighbor_unitLattice {n : ℕ} {L : IntegralLattice (Fin n → ℚ)} (h : L.IsNeighbor (unitLattice (Fin n)) 2) (h₁ : ∀ (i : Fin n), Pi.single i 1 ∉ L.carrier) : L.carrier ⊓ (unitLattice (Fin n)).carrier = checkerboardCarrier n

The intersection of Iₙ with a two-neighbor without coordinate vectors is Dₙ.

theorem TauCeti.IntegralLattice.exists_forall_mem_carrier_iff_of_isNeighbor_unitLattice {n : ℕ} {L : IntegralLattice (Fin n → ℚ)} (h : L.IsNeighbor (unitLattice (Fin n)) 2) (h₁ : ∀ (i : Fin n), Pi.single i 1 ∉ L.carrier) : ∃ (y : Fin n → ℚ), (∀ (i : Fin n), ∃ (k : ℤ), y i = ↑k + 1 / 2) ∧ ∀ (x : Fin n → ℚ), x ∈ L.carrier ↔ x ∈ checkerboardCarrier n ∨ x - y ∈ checkerboardCarrier n

The two-neighbors of Iₙ without coordinate vectors. If L is a Kneser two-neighbor of the standard lattice ℤⁿ containing no coordinate vector eᵢ, then L = Dₙ ∪ (y + Dₙ) for a vector y whose coordinates all lie in ℤ + 1/2.

theorem TauCeti.IntegralLattice.four_dvd_of_isNeighbor_unitLattice {n : ℕ} {L : IntegralLattice (Fin n → ℚ)} (h : L.IsNeighbor (unitLattice (Fin n)) 2) (h₁ : ∀ (i : Fin n), Pi.single i 1 ∉ L.carrier) : 4 ∣ n

A two-neighbor of Iₙ without coordinate vectors has rank divisible by four. The glue vector y has half-integral coordinates, so y · y = ∑ (kᵢ² + kᵢ) + n / 4 must be an integer.

The isometry with Dₙ⁺

theorem TauCeti.IntegralLattice.nonempty_isometry_checkerboardPlusLattice_of_isNeighbor_unitLattice {n : ℕ} {L : IntegralLattice (Fin n → ℚ)} (h : L.IsNeighbor (unitLattice (Fin n)) 2) (h₁ : ∀ (i : Fin n), Pi.single i 1 ∉ L.carrier) (hn : 8 ∣ n) : Nonempty ((checkerboardPlusLattice n hn).Isometry L)

A two-neighbor of Iₙ without coordinate vectors is Dₙ⁺, for 8 ∣ n. Its glue vector is congruent modulo Dₙ either to the spinor (1/2, …, 1/2) or, after changing the sign of one coordinate, to it.

theorem TauCeti.IntegralLattice.nonempty_isometry_typeE₈RootLattice_of_isNeighbor_unitLattice {L : IntegralLattice (Fin 8 → ℚ)} (h : L.IsNeighbor (unitLattice (Fin 8)) 2) (h₁ : ∀ (i : Fin 8), Pi.single i 1 ∉ L.carrier) : Nonempty (typeE₈RootLattice.Isometry L)

A two-neighbor of I₈ without coordinate vectors is E₈.

Two-neighbors of a lattice isometric to Iₙ

theorem TauCeti.IntegralLattice.four_dvd_of_isNeighbor_of_isometry_unitLattice {n : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L N : IntegralLattice V} (e : (unitLattice (Fin n)).Isometry N) (h : L.IsNeighbor N 2) (h₁ : L.vectorsOfNorm 1 = ∅) : 4 ∣ n

A two-neighbor of Iₙ without vectors of norm one has rank divisible by four. Here Iₙ is any lattice N given with an isometry from the standard lattice.

theorem TauCeti.IntegralLattice.nonempty_isometry_checkerboardPlusLattice_of_isNeighbor_of_isometry_unitLattice {n : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L N : IntegralLattice V} (e : (unitLattice (Fin n)).Isometry N) (h : L.IsNeighbor N 2) (h₁ : L.vectorsOfNorm 1 = ∅) (hn : 8 ∣ n) : Nonempty ((checkerboardPlusLattice n hn).Isometry L)

A two-neighbor of Iₙ without vectors of norm one is Dₙ⁺, for 8 ∣ n. Here Iₙ is any lattice N given with an isometry from the standard lattice.

theorem TauCeti.IntegralLattice.nonempty_isometry_typeE₈RootLattice_of_isNeighbor_of_isometry_unitLattice {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L N : IntegralLattice V} (e : (unitLattice (Fin 8)).Isometry N) (h : L.IsNeighbor N 2) (h₁ : L.vectorsOfNorm 1 = ∅) : Nonempty (typeE₈RootLattice.Isometry L)

A two-neighbor of I₈ without vectors of norm one is E₈. Here I₈ is any lattice N given with an isometry from the standard lattice.