An integral lattice is a finitely generated free abelian group
of finite rank n
with a bilinear form that takes integer values.
- add : Λ → Λ → Λ
- zero : Λ
- neg : Λ → Λ
- sub : Λ → Λ → Λ
- free : Module.Free ℤ Λ
- finite : Module.Finite ℤ Λ
Instances
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) ⋯) ⋯
Instances For
@[simp]
Inner product with zero vector is always zero.
@[simp]
A lattice is even if all norms are even.
Equations
- IntegralLattice.IsEven Λ = ∀ (x : Λ), Even (inner ℤ x x)
Instances For
Equations
- IntegralLattice.gramMatrix v = Matrix.of fun (i j : ι) => inner ℤ (v i) (v j)
Instances For
The determinant of a lattice is defined as the determinant of the Gram matrix of its basis.
Equations
Instances For
A lattice is unimodular if its determinant is equal to 1.