Documentation

Project.IntegralLattice.Basic

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.

Instances
    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.

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

    Equations
    Instances For
      @[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

      A lattice is even if all norms are even.

      Equations
      Instances For
        def IntegralLattice.gramMatrix {Λ : Type u_2} {ι : Type u_3} [IntegralLattice Λ] (v : ιΛ) :
        Matrix ι ι
        Equations
        Instances For
          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
          Instances For

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

            Equations
            Instances For