Levels of the type A root lattices

The level of Aₙ is 2 (n + 1) / gcd(n, 2): it is n + 1 for even n and 2 (n + 1) for odd n. The formula includes the rank-zero lattice, of level one. These are levels of the even bilinear lattices, so they annihilate the half-norm discriminant quadratic form, not merely its polar pairing.

The calculation uses IntegralLattice.IsEven.level_eq_den and the first fundamental weight's quadratic value computed in TypeA.Basic.

References

• W. Ebeling, Lattices and Codes, Chapters 1 and 3.

@[simp]

theorem TauCeti.IntegralLattice.level_typeARootLattice (n : ℕ) : (typeARootLattice n).level = 2 * (n + 1) / n.gcd 2

The level of Aₙ is 2 (n + 1) / gcd(n, 2), including A₀.

theorem TauCeti.IntegralLattice.level_typeARootLattice_of_even {n : ℕ} (hn : Even n) : (typeARootLattice n).level = n + 1

In even rank, the level of Aₙ is n + 1, including rank zero.

theorem TauCeti.IntegralLattice.level_typeARootLattice_of_odd {n : ℕ} (hn : Odd n) : (typeARootLattice n).level = 2 * (n + 1)

In odd rank, the level of Aₙ is 2 (n + 1).