class E8Lattice (Λ : Type u_1) extends IntegralLattice Λ : Type u_1

The E8 lattice is the unique even, unimodular integral lattice of rank 8

• inner : Λ → Λ → ℤ
• add : Λ → Λ → Λ
• add_assoc (a b c : Λ) : a + b + c = a + (b + c)
• zero : Λ
• zero_add (a : Λ) : 0 + a = a
• add_zero (a : Λ) : a + 0 = a
• nsmul : ℕ → Λ → Λ
• nsmul_zero (x : Λ) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : Λ) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : Λ → Λ
• sub : Λ → Λ → Λ
• sub_eq_add_neg (a b : Λ) : a - b = a + -b
• zsmul : ℤ → Λ → Λ
• zsmul_zero' (a : Λ) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : Λ) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : Λ) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : Λ) : -a + a = 0
• add_comm (a b : Λ) : a + b = b + a
• free : Module.Free ℤ Λ
• finite : Module.Finite ℤ Λ
• add_inner (x y z : Λ) : inner ℤ (x + y) z = inner ℤ x z + inner ℤ y z
• inner_sym (x y : Λ) : inner ℤ x y = inner ℤ y x
• inner_self (x : Λ) : inner ℤ x x ≥ 0
• inner_self_eq_zero (x : Λ) : inner ℤ x x = 0 → x = 0
• even : IntegralLattice.IsEven Λ
• unimodular : IntegralLattice.IsUnimodular Λ
• rank_eq_8 : Module.finrank ℤ Λ = 8

theorem E8Lattice.unique (Λ₁ : Type u_2) (Λ₂ : Type u_3) [E8Lattice Λ₁] [E8Lattice Λ₂] : Nonempty (Λ₁ ≃ₗ Λ₂)

def E8Lattice.B : LinearMap.BilinForm ℤ (Fin 8 → ℤ)

Equations

• E8Lattice.B = Matrix.toBilin' CartanMatrix.E₈

def E8Lattice.intMatrixToRat {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℤ) : Matrix (Fin m) (Fin n) ℚ

Equations

• E8Lattice.intMatrixToRat A = A.map Int.cast

theorem E8Lattice.intDetToRat {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : ↑A.det = (intMatrixToRat A).det

def E8Lattice.M0 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M0 = E8Lattice.intMatrixToRat CartanMatrix.E₈

def E8Lattice.M1 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M1 = E8Lattice.M0.updateRow 2 (E8Lattice.M0 2 + (1 / 2) • E8Lattice.M0 0)

def E8Lattice.M2 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M2 = E8Lattice.M1.updateRow 3 (E8Lattice.M1 3 + (1 / 2) • E8Lattice.M1 1)

def E8Lattice.M3 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M3 = E8Lattice.M2.updateRow 3 (E8Lattice.M2 3 + (2 / 3) • E8Lattice.M2 2)

def E8Lattice.M4 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M4 = E8Lattice.M3.updateRow 4 (E8Lattice.M3 4 + (6 / 5) • E8Lattice.M3 3)

def E8Lattice.M5 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M5 = E8Lattice.M4.updateRow 5 (E8Lattice.M4 5 + (5 / 4) • E8Lattice.M4 4)

def E8Lattice.M6 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M6 = E8Lattice.M5.updateRow 6 (E8Lattice.M5 6 + (4 / 3) • E8Lattice.M5 5)

def E8Lattice.M7 : Matrix (Fin 8) (Fin 8) ℚ

Equations

• E8Lattice.M7 = E8Lattice.M6.updateRow 7 (E8Lattice.M6 7 + (3 / 2) • E8Lattice.M6 6)

theorem E8Lattice.M7_upperTrianglar : M7.BlockTriangular id

theorem E8Lattice.M7_det : M7.det = 1

theorem E8Lattice.E8_det : ↑CartanMatrix.E₈.det = 1

theorem E8Lattice.inner_self_calc (x : Fin 8 → ℤ) : (B x) x = 2 * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 + x 4 ^ 2 + x 5 ^ 2 + x 6 ^ 2 + x 7 ^ 2 - (x 0 * x 2 + x 1 * x 3 + x 2 * x 3 + x 3 * x 4 + x 4 * x 5 + x 5 * x 6 + x 6 * x 7))

theorem E8Lattice.inner_self_comp_sq (x : Fin 8 → ℤ) : ↑((B x) x) = (√2 * ↑(x 0) - √(1 / 2) * ↑(x 2)) ^ 2 + (√2 * ↑(x 1) - √(1 / 2) * ↑(x 3)) ^ 2 + (√(3 / 2) * ↑(x 2) - √(2 / 3) * ↑(x 3)) ^ 2 + (√(5 / 6) * ↑(x 3) - √(6 / 5) * ↑(x 4)) ^ 2 + (√(4 / 5) * ↑(x 4) - √(5 / 4) * ↑(x 5)) ^ 2 + (√(3 / 4) * ↑(x 5) - √(4 / 3) * ↑(x 6)) ^ 2 + (√(2 / 3) * ↑(x 6) - √(3 / 2) * ↑(x 7)) ^ 2 + 1 / 2 * ↑(x 7) ^ 2

theorem E8Lattice.AddInner (x y z : Fin 8 → ℤ) : (B (x + y)) z = (B x) z + (B y) z

theorem E8Lattice.InnerSym (x y : Fin 8 → ℤ) : (B x) y = (B y) x

theorem E8Lattice.InnerSelf (x : Fin 8 → ℤ) : (B x) x ≥ 0

theorem E8Lattice.InnerEven (x : Fin 8 → ℤ) : Even ((B x) x)

theorem E8Lattice.InnerSelfEqZero (x : Fin 8 → ℤ) : (B x) x = 0 → x = 0

instance E8Lattice.exampleE8 : E8Lattice (Fin 8 → ℤ)

Equations

• One or more equations did not get rendered due to their size.

theorem E8Lattice.exists_E8 : ∃ (Λ : Type u), Nonempty (E8Lattice Λ)

theorem E8Lattice.exists_E8' : ∃ (Λ : Type), Nonempty (E8Lattice Λ)

instance E8Lattice.instFiniteElemSetOfEqIntInnerCast (Λ : Type u_1) [E8Lattice Λ] (n : ℕ) : Finite ↑{x : Λ | inner ℤ x x = ↑n}

instance E8Lattice.instFiniteSubtypeEqIntInnerCast (Λ : Type u_1) [E8Lattice Λ] (n : ℕ) : Finite { x : Λ // inner ℤ x x = ↑n }

theorem E8Lattice.card_norm_2 (Λ : Type u_1) [E8Lattice Λ] : Nat.card ↑{x : Λ | inner ℤ x x = 2} = 240