Real models of the root lattices A₂, D₄ and E₈

The root lattices A₂ = typeARootLattice 2, D₄ = checkerboardLattice 4 and E₈ = typeE₈RootLattice are positive definite even rational lattices, so they have real models (TauCeti.IntegralLattice.realModel), even full lattices in Euclidean spaces of dimension 2, 4 and 8. This file computes the level, the order of the discriminant group, the signed discriminant ZLattice.signedDiscr, and the conductor of the Kronecker character (D_L / ·) of these real models from the rational lattices, through the comparison of the two models (TauCeti.IntegralLattice.level_realModel, TauCeti.IntegralLattice.natCard_discriminantGroup_realModel, TauCeti.IntegralLattice.signedDiscr_realModel):

• A₂ has level 3, determinant 3 and signed discriminant D = -3, whose Kronecker character (-3 / ·) is primitive of conductor 3;
• D₄ has level 2, determinant 4 and signed discriminant D = 4 = 2², so its Kronecker character (4 / ·) is trivial of conductor 1;
• E₈ has level 1, determinant 1 and signed discriminant D = 1.

The scaled lattice √2 • E₈ is even of level 2 and signed discriminant 256 = 16², and its Fricke partner √2 • (√2 • E₈)^∨ is E₈ again, of level 1 and signed discriminant 1. So the level of the Fricke partner of an even lattice of level N can be a proper divisor of N, while both √2 • E₈ and E₈ have trivial Kronecker character of conductor 1.

Main statements

• TauCeti.IntegralLattice.level_realModel_typeARootLattice_two, TauCeti.IntegralLattice.natCard_discriminantGroup_realModel_typeARootLattice_two, TauCeti.IntegralLattice.signedDiscr_realModel_typeARootLattice_two, TauCeti.IntegralLattice.conductor_kroneckerChar_signedDiscr_realModel_typeARootLattice_two: the real model of A₂ has level 3, discriminant group of order 3, signed discriminant -3, and Kronecker conductor 3.
• TauCeti.IntegralLattice.level_realModel_checkerboardLattice_four, TauCeti.IntegralLattice.natCard_discriminantGroup_realModel_checkerboardLattice_four, TauCeti.IntegralLattice.signedDiscr_realModel_checkerboardLattice_four, TauCeti.IntegralLattice.kroneckerChar_signedDiscr_realModel_checkerboardLattice_four: the real model of D₄ has level 2, discriminant group of order 4, signed discriminant 4, and trivial Kronecker character (conductor 1).
• TauCeti.IntegralLattice.signedDiscr_realModel_typeE₈RootLattice, TauCeti.IntegralLattice.level_sqrt_two_smul_realModel_typeE₈RootLattice, TauCeti.IntegralLattice.signedDiscr_sqrt_two_smul_realModel_typeE₈RootLattice, TauCeti.IntegralLattice.level_sqrt_level_smul_dual_sqrt_two_smul_realModel_typeE₈RootLattice: E₈ has signed discriminant 1, √2 • E₈ has level 2, signed discriminant 256 and trivial Kronecker character, and its Fricke partner has level 1.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Springer, 1999, Chapter 4.
• W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 3.

A₂

theorem TauCeti.IntegralLattice.level_realModel_typeARootLattice_two : ZLattice.level ((typeARootLattice 2).realModel ⋯) = 3

The real model of the root lattice A₂ has level 3.

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_realModel_typeARootLattice_two : Nat.card (ZLattice.DiscriminantGroup ((typeARootLattice 2).realModel ⋯)) = 3

The discriminant group of the real model of the root lattice A₂ has order 3, which is its determinant.

theorem TauCeti.IntegralLattice.signedDiscr_realModel_typeARootLattice_two : ZLattice.signedDiscr ((typeARootLattice 2).realModel ⋯) = -3

The real model of the root lattice A₂ has signed discriminant -3.

theorem TauCeti.IntegralLattice.conductor_kroneckerChar_signedDiscr_realModel_typeARootLattice_two (R : Type u_1) [CommRing R] [NeZero 2] : (kroneckerChar R (ZLattice.signedDiscr ((typeARootLattice 2).realModel ⋯)) ⋯ ⋯).conductor = 3

Over any commutative ring with 2 ≠ 0, the Kronecker character (-3 / ·) of the real model of A₂ is primitive of conductor 3.

D₄

theorem TauCeti.IntegralLattice.level_realModel_checkerboardLattice_four : ZLattice.level ((checkerboardLattice 4).realModel ⋯) = 2

The real model of the root lattice D₄ has level 2.

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_realModel_checkerboardLattice_four : Nat.card (ZLattice.DiscriminantGroup ((checkerboardLattice 4).realModel ⋯)) = 4

The discriminant group of the real model of the root lattice D₄ has order 4, which is its determinant.

theorem TauCeti.IntegralLattice.signedDiscr_realModel_checkerboardLattice_four : ZLattice.signedDiscr ((checkerboardLattice 4).realModel ⋯) = 4

The real model of the root lattice D₄ has signed discriminant 4.

theorem TauCeti.IntegralLattice.kroneckerChar_signedDiscr_realModel_checkerboardLattice_four (R : Type u_1) [CommRing R] : kroneckerChar R (ZLattice.signedDiscr ((checkerboardLattice 4).realModel ⋯)) ⋯ ⋯ = 1

Because D_{D₄} = 4 = 2² is a square, the Kronecker character of the real model of D₄ is the trivial character modulo 4.

theorem TauCeti.IntegralLattice.conductor_kroneckerChar_signedDiscr_realModel_checkerboardLattice_four (R : Type u_1) [CommRing R] : (kroneckerChar R (ZLattice.signedDiscr ((checkerboardLattice 4).realModel ⋯)) ⋯ ⋯).conductor = 1

The Kronecker character of the real model of D₄ has conductor 1.

E₈ and √2 • E₈

theorem TauCeti.IntegralLattice.signedDiscr_realModel_typeE₈RootLattice : ZLattice.signedDiscr (typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice) = 1

The real model of the even unimodular root lattice E₈ has signed discriminant 1.

theorem TauCeti.IntegralLattice.level_sqrt_two_smul_realModel_typeE₈RootLattice : ZLattice.level (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice) = 2

The real model of the root lattice E₈, scaled by √2, has level 2.

theorem TauCeti.IntegralLattice.signedDiscr_sqrt_two_smul_realModel_typeE₈RootLattice : ZLattice.signedDiscr (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice) = 256

The real model of E₈ scaled by √2 has signed discriminant 256 = 16².

theorem TauCeti.IntegralLattice.kroneckerChar_signedDiscr_sqrt_two_smul_realModel_typeE₈RootLattice (R : Type u_1) [CommRing R] : kroneckerChar R (ZLattice.signedDiscr (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice)) ⋯ ⋯ = 1

Because D_{√2 • E₈} = 256 = 16² is a square, the Kronecker character of √2 • E₈ is the trivial character modulo 256.

theorem TauCeti.IntegralLattice.conductor_kroneckerChar_signedDiscr_sqrt_two_smul_realModel_typeE₈RootLattice (R : Type u_1) [CommRing R] : (kroneckerChar R (ZLattice.signedDiscr (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice)) ⋯ ⋯).conductor = 1

The Kronecker character of √2 • E₈ has conductor 1.

theorem TauCeti.IntegralLattice.level_sqrt_level_smul_dual_sqrt_two_smul_realModel_typeE₈RootLattice : ZLattice.level (√↑(ZLattice.level (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice)) • ZLattice.dual (√2 • typeE₈RootLattice.realModel isPosDef_typeE₈RootLattice)) = 1

The Fricke partner √2 • (√2 • E₈)^∨ of the even lattice √2 • E₈ of level 2 has level 1, a proper divisor of 2: it is E₈ itself.