class IntegralLattice (Λ : Type u_1) extends Inner ℤ Λ, AddCommGroup Λ : Type u_1

An integral lattice is a finitely generated free abelian group of finite rank n with a bilinear form that takes integer values.

• 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

theorem IntegralLattice.inner_add {Λ : Type u_1} [IntegralLattice Λ] (x y z : Λ) : inner ℤ x (y + z) = inner ℤ x y + inner ℤ x z

Inner product is also additive in the second argument by symmetry.

def IntegralLattice.InnerBilin {Λ : Type u_1} [IntegralLattice Λ] : Λ →+ Λ →+ ℤ

Bilinear form of the inner product on an integral lattice as additive monoid homomorphism.

Equations

• IntegralLattice.InnerBilin = AddMonoidHom.mk' (fun (x : Λ) => AddMonoidHom.mk' (fun (y : Λ) => inner ℤ x y) ⋯) ⋯

@[simp]

theorem IntegralLattice.inner_zero {Λ : Type u_1} [IntegralLattice Λ] (x : Λ) : inner ℤ x 0 = 0

Inner product with zero vector is always zero.

@[simp]

theorem IntegralLattice.zero_inner {Λ : Type u_1} [IntegralLattice Λ] (y : Λ) : inner ℤ 0 y = 0

def IntegralLattice.IsEven (Λ : Type u_1) [IntegralLattice Λ] : Prop

A lattice is even if all norms are even.

Equations

• IntegralLattice.IsEven Λ = ∀ (x : Λ), Even (inner ℤ x x)

def IntegralLattice.gramMatrix {Λ : Type u_2} {ι : Type u_3} [IntegralLattice Λ] (v : ι → Λ) : Matrix ι ι ℤ

Equations

• IntegralLattice.gramMatrix v = Matrix.of fun (i j : ι) => inner ℤ (v i) (v j)

noncomputable def IntegralLattice.determinant (Λ : Type u_1) [IntegralLattice Λ] : ℤ

The determinant of a lattice is defined as the determinant of the Gram matrix of its basis.

Equations

• IntegralLattice.determinant Λ = (IntegralLattice.gramMatrix ⇑(Module.Free.chooseBasis ℤ Λ)).det

def IntegralLattice.IsUnimodular (Λ : Type u_1) [IntegralLattice Λ] : Prop

A lattice is unimodular if its determinant is equal to 1.

Equations

• IntegralLattice.IsUnimodular Λ = (IntegralLattice.determinant Λ = 1)