Spinor glue lattices Dₙ⁺

For positive n divisible by eight, adjoining the spinor vector s = (1/2, …, 1/2) to the checkerboard lattice constructs the positive definite even unimodular lattice Dₙ⁺. Its carrier is literally Dₙ ∪ (s + Dₙ). In positive rank the order-two spinor subgroup is quadratic-isotropic and Lagrangian; the general gluing theorem therefore proves unimodularity. In particular, the construction supplies D₁₆⁺, while at rank eight it is the coordinate model of E₈. The rank-zero lattice is included as well.

Beyond rank eight the spinor coset has minimal norm n / 4 > 2, so every root of Dₙ⁺ lies in Dₙ and the roots do not span Dₙ⁺; at rank eight the spinor coset contains roots of E₈.

The subgroup and intermediate carrier are defined in every rank. The two-coset description needs even rank, and the index-two description needs even positive rank; quadratic isotropy needs exactly divisibility by eight.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, §4.8.1.
• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Proposition 1.4.1.
• W. Ebeling, Lattices and Codes, Chapter 3.

noncomputable def TauCeti.IntegralLattice.checkerboardSpinorSubgroup (n : ℕ) : AddSubgroup (checkerboardLattice n).DiscriminantGroup

The subgroup generated by the spinor class in the discriminant group of Dₙ.

theorem TauCeti.IntegralLattice.checkerboardSpinorSubgroup_def (n : ℕ) : checkerboardSpinorSubgroup n = AddSubgroup.zmultiples (checkerboardSpinorClass n)

The spinor subgroup is the cyclic subgroup generated by the spinor class.

@[simp]

theorem TauCeti.IntegralLattice.mem_checkerboardSpinorSubgroup_iff (n : ℕ) (hn : Even n) (x : (checkerboardLattice n).DiscriminantGroup) : x ∈ checkerboardSpinorSubgroup n ↔ x = 0 ∨ x = checkerboardSpinorClass n

In even rank the spinor subgroup consists of zero and the spinor class.

theorem TauCeti.IntegralLattice.natCard_checkerboardSpinorSubgroup (n : ℕ) [NeZero n] (hn : Even n) : Nat.card ↥(checkerboardSpinorSubgroup n) = 2

The spinor subgroup has order two in even positive rank.

noncomputable def TauCeti.IntegralLattice.checkerboardPlusCarrier (n : ℕ) : ↑(checkerboardLattice n).IntermediateCarrier

The inverse image of the spinor subgroup in the dual of the checkerboard lattice.

@[simp]

theorem TauCeti.IntegralLattice.mem_checkerboardPlusCarrier_iff (n : ℕ) (hn : Even n) (x : Fin n → ℚ) : x ∈ ↑(checkerboardPlusCarrier n) ↔ x ∈ (checkerboardLattice n).carrier ∨ x - checkerboardSpinor n ∈ (checkerboardLattice n).carrier

In even rank, the spinor enlargement is the union of Dₙ and its spinor coset.

theorem TauCeti.IntegralLattice.mem_checkerboardPlusCarrier_iff_of_sub_mem (n : ℕ) (hn : Even n) {g : Fin n → ℚ} (hg : g - checkerboardSpinor n ∈ checkerboardCarrier n) (x : Fin n → ℚ) : x ∈ ↑(checkerboardPlusCarrier n) ↔ x ∈ checkerboardCarrier n ∨ x - g ∈ checkerboardCarrier n

In even rank, the spinor enlargement is the union of Dₙ and g + Dₙ, for any g congruent to the spinor modulo Dₙ.

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_checkerboardPlusCarrier (n : ℕ) : (checkerboardLattice n).discriminantSubgroup (checkerboardPlusCarrier n) = checkerboardSpinorSubgroup n

The subgroup recovered from the spinor enlargement is the spinor subgroup.

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_checkerboardSpinorClass_eq_zero_iff (n : ℕ) : ((checkerboardLattice n).discriminantQuadraticMap ⋯) (checkerboardSpinorClass n) = 0 ↔ 8 ∣ n

The spinor class is quadratic-isotropic exactly in ranks divisible by eight.

@[simp]

theorem TauCeti.IntegralLattice.isIsotropic_checkerboardSpinorSubgroup_iff (n : ℕ) : ((checkerboardLattice n).discriminantQuadraticModule ⋯).IsIsotropic (checkerboardSpinorSubgroup n) ↔ 8 ∣ n

The spinor subgroup is quadratic-isotropic exactly in ranks divisible by eight.

theorem TauCeti.IntegralLattice.isEven_checkerboardPlusCarrier (n : ℕ) (hn : 8 ∣ n) : IntermediateCarrier.IsEven (checkerboardPlusCarrier n)

In ranks divisible by eight, the spinor enlargement is even.

theorem TauCeti.IntegralLattice.isLagrangian_checkerboardSpinorSubgroup (n : ℕ) (hn : 8 ∣ n) : ((checkerboardLattice n).discriminantQuadraticModule ⋯).IsLagrangian (checkerboardSpinorSubgroup n)

In ranks divisible by eight, the spinor subgroup is Lagrangian.

noncomputable def TauCeti.IntegralLattice.checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : IntegralLattice (Fin n → ℚ)

The positive definite even unimodular spinor glue lattice Dₙ⁺, for 8 ∣ n.

theorem TauCeti.IntegralLattice.toIntegralLattice_eq_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) (h : IntermediateCarrier.IsEven ((checkerboardLattice n).intermediateCarrierOfDiscriminantSubgroup (checkerboardSpinorSubgroup n))) : ⋯.toIntegralLattice = checkerboardPlusLattice n hn

The general intermediate-carrier construction recovers Dₙ⁺.

@[simp]

theorem TauCeti.IntegralLattice.checkerboardPlusLattice_carrier (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).carrier = ↑(checkerboardPlusCarrier n)

The carrier of Dₙ⁺ is the inverse image of the spinor subgroup.

@[simp]

theorem TauCeti.IntegralLattice.ofIsotropicSubgroup_checkerboardSpinorSubgroup (n : ℕ) (hn : 8 ∣ n) : (checkerboardLattice n).ofIsotropicSubgroup ⋯ (checkerboardSpinorSubgroup n) ⋯ = checkerboardPlusLattice n hn

Isotropic gluing along the spinor subgroup recovers the concrete spinor enlargement.

@[simp]

theorem TauCeti.IntegralLattice.checkerboardPlusLattice_form (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).form = (checkerboardLattice n).form

The form of Dₙ⁺ is the standard dot product inherited from Dₙ.

instance TauCeti.IntegralLattice.instIsNondegenerateCheckerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).IsNondegenerate

The spinor glue lattice is nondegenerate.

theorem TauCeti.IntegralLattice.isEven_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).IsEven

The spinor glue lattice is even.

theorem TauCeti.IntegralLattice.index_checkerboardPlusCarrier (n : ℕ) [NeZero n] (hn : Even n) : IntermediateCarrier.index (checkerboardPlusCarrier n) = 2

The spinor enlargement has index two in even positive rank.

theorem TauCeti.IntegralLattice.isPosDef_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).IsPosDef

The spinor glue lattice is positive definite.

theorem TauCeti.IntegralLattice.isUnimodular_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).IsUnimodular

The spinor glue lattice is unimodular, by gluing along a Lagrangian.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : (checkerboardPlusLattice n hn).discriminant = 1

The spinor glue lattice has discriminant one.

theorem TauCeti.IntegralLattice.mem_checkerboardLattice_carrier_of_mem_vectorsOfNorm_two (n : ℕ) (hn : 8 ∣ n) (hn8 : 8 < n) {x : ↥(checkerboardPlusLattice n hn).carrier} (hx : x ∈ (checkerboardPlusLattice n hn).vectorsOfNorm 2) : ↑x ∈ (checkerboardLattice n).carrier

Beyond rank eight, the roots of Dₙ⁺ lie in Dₙ. A vector of the spinor coset has every coordinate in ℤ + 1/2, hence norm at least n / 4 > 2. At n = 8 the spinor coset does contain roots, those of the coordinate model of E₈.

theorem TauCeti.IntegralLattice.span_vectorsOfNorm_two_checkerboardPlusLattice_ne_top (n : ℕ) (hn : 8 ∣ n) (hn8 : 8 < n) : Submodule.span ℤ ((checkerboardPlusLattice n hn).vectorsOfNorm 2) ≠ ⊤

Beyond rank eight, the roots of Dₙ⁺ do not span it. They span at most Dₙ, which misses the spinor vector.

@[simp]

theorem TauCeti.IntegralLattice.finrank_checkerboardPlusLattice (n : ℕ) (hn : 8 ∣ n) : Module.finrank ℤ ↥(checkerboardPlusLattice n hn).carrier = n

The rank of Dₙ⁺ is n.