The zero-sum coordinate model of the root lattice of type Aₙ

The classical coordinate model of the root lattice of type Aₙ is

Aₙ = {x ∈ ℤ^{n+1} | x₀ + x₁ + ⋯ + xₙ = 0}

with the standard dot product. It has rank n, so it is not a full lattice in ℚ^{n+1}. This file therefore places it in its rational span, the hyperplane of vectors of ℚ^{n+1} with coordinate sum zero, which is the kernel TauCeti.singleParityCheckCode ℚ (Fin (n + 1)) of the coordinate-sum map, and proves that this coordinate model is isometric to the simple-root model TauCeti.IntegralLattice.typeARootLattice n, whose Gram matrix is the Cartan matrix CartanMatrix.A n.

The Bourbaki simple roots are αᵢ = eᵢ - eᵢ₊₁ for 0 ≤ i < n, and their dot products are the entries of CartanMatrix.A n. The coefficients of a vector in this basis are read off by the partial sums: pairing αᵢ with the indicator vector of the coordinates 0, …, k gives 1 when i = k and 0 otherwise, while pairing it with the all-ones vector gives 0. Consequently

x = ∑ₖ (x₀ + ⋯ + xₖ) αₖ        whenever x₀ + ⋯ + xₙ = 0,

because the difference of the two sides has every partial sum equal to zero, and a vector all of whose partial sums vanish is zero. This identity shows at once that the simple roots form a rational basis of the hyperplane and that their integral span is exactly the set of integral vectors in it, since the partial sums of an integral vector are integers.

Main declarations

• TauCeti.IntegralLattice.zeroSumSimpleRoot: the simple root eᵢ - eᵢ₊₁.
• TauCeti.IntegralLattice.sum_smul_zeroSumSimpleRoot: the partial-sum expansion of a vector of coordinate sum zero in the simple roots.
• TauCeti.IntegralLattice.zeroSumBasis: the simple roots as a rational basis of the hyperplane.
• TauCeti.IntegralLattice.zeroSumLattice: the lattice Aₙ with the restricted dot product.
• TauCeti.IntegralLattice.mem_zeroSumLattice_carrier_iff: its carrier consists exactly of the integral vectors of coordinate sum zero.
• TauCeti.IntegralLattice.gramMatrix_zeroSumSimpleRootBasis: its Gram matrix in the simple roots is CartanMatrix.A n.
• TauCeti.IntegralLattice.typeAIsometryZeroSumLattice: the isometry from the simple-root model of Aₙ onto the coordinate model, carrying the i-th simple root to eᵢ - eᵢ₊₁.
• TauCeti.IntegralLattice.typeAIsometryZeroSumLattice_typeAFundamentalWeight_apply: it carries the first fundamental weight ω₁ to e₀ - (1 / (n + 1)) (1, …, 1).
• TauCeti.IntegralLattice.typeARootLattice_form_self_eq_dotProduct: it turns the norm of the simple-root model into the dot product of classical coordinates.
• TauCeti.IntegralLattice.exists_typeAIsometryZeroSumLattice_apply_eq_intCast_sub_of_mk_eq: the classical coordinates of a dual vector in the class k ω₁ lie in ℤ - k / (n + 1).
• TauCeti.IntegralLattice.isEven_zeroSumLattice, isPosDef_zeroSumLattice and determinant_zeroSumLattice: the coordinate model is even and positive definite, of determinant n + 1.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4–6, plate I.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §6.1.

The simple roots in classical coordinates

def TauCeti.IntegralLattice.zeroSumSimpleRoot (n : ℕ) (i : Fin n) : Fin (n + 1) → ℚ

The i-th Bourbaki simple root eᵢ - eᵢ₊₁ of type Aₙ in the classical coordinates of ℚ^{n+1}.

theorem TauCeti.IntegralLattice.zeroSumSimpleRoot_apply (n : ℕ) (i : Fin n) (j : Fin (n + 1)) : zeroSumSimpleRoot n i j = (if j = i.castSucc then 1 else 0) - if j = i.succ then 1 else 0

theorem TauCeti.IntegralLattice.zeroSumSimpleRoot_mem_singleParityCheckCode (n : ℕ) (i : Fin n) : zeroSumSimpleRoot n i ∈ singleParityCheckCode ℚ (Fin (n + 1))

Every simple root has coordinate sum zero.

theorem TauCeti.IntegralLattice.zeroSumSimpleRoot_dotProduct_zeroSumSimpleRoot (n : ℕ) (i j : Fin n) : zeroSumSimpleRoot n i ⬝ᵥ zeroSumSimpleRoot n j = ↑(CartanMatrix.A n i j)

The dot products of the simple roots are the entries of the Cartan matrix of type Aₙ.

Partial sums and the expansion in the simple roots

theorem TauCeti.IntegralLattice.sum_smul_zeroSumSimpleRoot (n : ℕ) {x : Fin (n + 1) → ℚ} (hx : x ∈ singleParityCheckCode ℚ (Fin (n + 1))) : ∑ k : Fin n, (∑ j ≤ k.castSucc, x j) • zeroSumSimpleRoot n k = x

The partial-sum expansion. A vector of ℚ^{n+1} with coordinate sum zero is the combination of the simple roots αₖ = eₖ - eₖ₊₁ whose coefficients are its partial sums x₀ + ⋯ + xₖ.

theorem TauCeti.IntegralLattice.linearIndependent_zeroSumSimpleRoot (n : ℕ) : LinearIndependent ℚ (zeroSumSimpleRoot n)

The simple roots eᵢ - eᵢ₊₁ are linearly independent over ℚ.

The simple roots as a basis of the hyperplane

noncomputable def TauCeti.IntegralLattice.zeroSumBasis (n : ℕ) : Module.Basis (Fin n) ℚ ↥(singleParityCheckCode ℚ (Fin (n + 1)))

The simple roots form a rational basis of the zero-sum hyperplane TauCeti.singleParityCheckCode ℚ (Fin (n + 1)).

@[simp]

theorem TauCeti.IntegralLattice.coe_zeroSumBasis_apply (n : ℕ) (i : Fin n) : ↑((zeroSumBasis n) i) = zeroSumSimpleRoot n i

The coordinate lattice

noncomputable def TauCeti.IntegralLattice.zeroSumForm (n : ℕ) : LinearMap.BilinForm ℚ ↥(singleParityCheckCode ℚ (Fin (n + 1)))

The dot product of ℚ^{n+1}, restricted to the zero-sum hyperplane.

@[simp]

theorem TauCeti.IntegralLattice.zeroSumForm_apply (n : ℕ) (x y : ↥(singleParityCheckCode ℚ (Fin (n + 1)))) : ((zeroSumForm n) x) y = ↑x ⬝ᵥ ↑y

noncomputable def TauCeti.IntegralLattice.zeroSumLattice (n : ℕ) : IntegralLattice ↥(singleParityCheckCode ℚ (Fin (n + 1)))

The coordinate model of the root lattice of type Aₙ: the integral vectors of ℚ^{n+1} with coordinate sum zero, with the standard dot product, as a lattice in the zero-sum hyperplane (TauCeti.IntegralLattice.mem_zeroSumLattice_carrier_iff). It is isometric to the simple-root model TauCeti.IntegralLattice.typeARootLattice n by TauCeti.IntegralLattice.typeAIsometryZeroSumLattice.

@[simp]

theorem TauCeti.IntegralLattice.zeroSumLattice_form (n : ℕ) : (zeroSumLattice n).form = zeroSumForm n

theorem TauCeti.IntegralLattice.zeroSumLattice_carrier (n : ℕ) : (zeroSumLattice n).carrier = Submodule.span ℤ (Set.range ⇑(zeroSumBasis n))

@[simp]

theorem TauCeti.IntegralLattice.mem_zeroSumLattice_carrier_iff (n : ℕ) (x : ↥(singleParityCheckCode ℚ (Fin (n + 1)))) : x ∈ (zeroSumLattice n).carrier ↔ ∀ (i : Fin (n + 1)), ∃ (m : ℤ), ↑x i = ↑m

The carrier of the coordinate model consists of the integral vectors with coordinate sum zero. Membership in the hyperplane is the coordinate-sum condition, and the simple roots span its integral vectors over ℤ because the partial sums of an integral vector are integers.

noncomputable def TauCeti.IntegralLattice.zeroSumSimpleRootBasis (n : ℕ) : Module.Basis (Fin n) ℤ ↥(zeroSumLattice n).carrier

The simple roots eᵢ - eᵢ₊₁, as a ℤ-basis of the coordinate model.

@[simp]

theorem TauCeti.IntegralLattice.coe_zeroSumSimpleRootBasis_apply (n : ℕ) (i : Fin n) : ↑↑((zeroSumSimpleRootBasis n) i) = zeroSumSimpleRoot n i

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_zeroSumSimpleRootBasis (n : ℕ) : (zeroSumLattice n).gramMatrix (zeroSumSimpleRootBasis n) = CartanMatrix.A n

The Gram matrix of the coordinate model in the simple roots is the Cartan matrix of type Aₙ.

The isometry with the simple-root model

noncomputable def TauCeti.IntegralLattice.typeAIsometryZeroSumLattice (n : ℕ) : (typeARootLattice n).Isometry (zeroSumLattice n)

The simple-root model of the root lattice of type Aₙ is isometric to the coordinate model {x ∈ ℤ^{n+1} | ∑ xᵢ = 0}, by the isometry carrying the i-th simple root to eᵢ - eᵢ₊₁.

@[simp]

theorem TauCeti.IntegralLattice.typeAIsometryZeroSumLattice_typeASimpleRoot (n : ℕ) (i : Fin n) : ↑((typeAIsometryZeroSumLattice n) (typeASimpleRoot n i)) = zeroSumSimpleRoot n i

The isometry typeAIsometryZeroSumLattice carries the i-th simple root of the simple-root model to eᵢ - eᵢ₊₁.

@[simp]

theorem TauCeti.IntegralLattice.typeAIsometryZeroSumLattice_typeAFundamentalWeight_apply (n : ℕ) (j : Fin (n + 1)) : ↑((typeAIsometryZeroSumLattice n) (typeAFundamentalWeight n)) j = (if j = 0 then 1 else 0) - 1 / (↑n + 1)

The first fundamental weight in classical coordinates. The isometry typeAIsometryZeroSumLattice carries ω₁ to e₀ - (1 / (n + 1)) (1, …, 1).

theorem TauCeti.IntegralLattice.typeARootLattice_form_self_eq_dotProduct {n : ℕ} (x : Fin n → ℚ) : ((typeARootLattice n).form x) x = ↑((typeAIsometryZeroSumLattice n) x) ⬝ᵥ ↑((typeAIsometryZeroSumLattice n) x)

The norm of a vector of the ambient space of the simple-root model of Aₙ is the dot product of its classical coordinates with themselves.

theorem TauCeti.IntegralLattice.exists_typeAIsometryZeroSumLattice_apply_eq_intCast_sub_of_mk_eq {n : ℕ} {k : ℤ} (x : ↥(typeARootLattice n).dualCarrier) (hx : Submodule.Quotient.mk x = k • typeAFundamentalWeightClass n) (j : Fin (n + 1)) : ∃ (m : ℤ), ↑((typeAIsometryZeroSumLattice n) ↑x) j = ↑m - ↑k / (↑n + 1)

The classical coordinates of the class k ω₁. The classical coordinates of a dual vector of Aₙ in the discriminant class k ω₁ all lie in ℤ - k / (n + 1).

Invariants of the coordinate model

theorem TauCeti.IntegralLattice.isEven_zeroSumLattice (n : ℕ) : (zeroSumLattice n).IsEven

The coordinate model of Aₙ is even.

theorem TauCeti.IntegralLattice.isPosDef_zeroSumLattice (n : ℕ) : (zeroSumLattice n).IsPosDef

The coordinate model of Aₙ is positive definite.

@[simp]

theorem TauCeti.IntegralLattice.determinant_zeroSumLattice (n : ℕ) : (zeroSumLattice n).determinant = ↑n + 1

The determinant of the coordinate model of Aₙ is n + 1.