Documentation

TauCeti.LinearAlgebra.IntegralLattice.PosDef.RepresentationNumber

Shells and representation numbers of an integral lattice #

The shell of norm n of an integral lattice L is the set S_n(L) of lattice vectors of norm n, and the representation number r_L(n) is its cardinality:

r_L(n) = #S_n(L) = #{x ∈ L | B(x, x) = n}.

The shells are the sets TauCeti.IntegralLattice.vectorsOfNorm, defined for every lattice and every rational n. For a positive definite lattice every shell is finite, so its representation numbers are genuine counts; the representation number is defined for every lattice, and takes the value 0 on an infinite shell.

This file records the basic behaviour of these counts: the zero shell of an anisotropic lattice, in particular of a positive definite one, is {0}, so r_L(0) = 1; negative norms are not represented by a positive semidefinite lattice; in rank zero the zero shell is {0} and every other shell is empty, so r_L(0) = 1 and r_L(n) = 0 for n ≠ 0; and an isometry carries shells onto shells, so representation numbers are isometry invariants.

Representation numbers are the counts that the theta series of a positive definite lattice expands; that identification is not made here.

Main declarations #

References #

source
noncomputable def TauCeti.IntegralLattice.representationNumber {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (n : ℚ) :
ℕ

The representation number r_L(n) of an integral lattice: the number of lattice vectors of norm n. For a positive definite lattice every shell is finite, so this is a genuine count; on an infinite shell it is 0.

Equations
Instances For
    source
    theorem TauCeti.IntegralLattice.representationNumber_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (n : ℚ) :
    L.representationNumber n = (L.vectorsOfNorm n).ncard

    The representation number is the cardinality of the shell.

    Shells of an anisotropic lattice #

    source
    theorem TauCeti.IntegralLattice.vectorsOfNorm_zero_of_anisotropic {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : QuadraticMap.Anisotropic L.norm) :
    L.vectorsOfNorm 0 = {0}

    The norm-zero shell of an anisotropic lattice consists of the zero vector alone. For a positive definite lattice hL, the hypothesis is hL.anisotropic.

    source
    theorem TauCeti.IntegralLattice.representationNumber_zero_of_anisotropic {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : QuadraticMap.Anisotropic L.norm) :
    L.representationNumber 0 = 1

    An anisotropic lattice represents 0 exactly once: r_L(0) = 1.

    source
    theorem TauCeti.IntegralLattice.IsPosDef.representationNumber_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) {n : ℚ} :
    L.representationNumber n = 0 ↔ L.vectorsOfNorm n = ∅

    For a positive definite lattice, whose shells are finite, the representation number of n vanishes exactly when no lattice vector has norm n.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.vectorsOfNorm_eq_empty_of_neg {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) {n : ℚ} (hn : n < 0) :
    L.vectorsOfNorm n = ∅

    A positive semidefinite lattice has no vector of negative norm.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.representationNumber_eq_zero_of_neg {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) {n : ℚ} (hn : n < 0) :
    L.representationNumber n = 0

    A positive semidefinite lattice represents no negative number.

    Shells in rank zero #

    source
    @[simp]
    theorem TauCeti.IntegralLattice.vectorsOfNorm_zero_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] :
    L.vectorsOfNorm 0 = {0}

    In rank zero the norm-zero shell is {0}.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.vectorsOfNorm_eq_empty_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] {n : ℚ} (hn : n ≠ 0) :
    L.vectorsOfNorm n = ∅

    In rank zero every shell of nonzero norm is empty.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.representationNumber_zero_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] :
    L.representationNumber 0 = 1

    In rank zero 0 is represented exactly once: r_L(0) = 1.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.representationNumber_eq_zero_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] {n : ℚ} (hn : n ≠ 0) :
    L.representationNumber n = 0

    In rank zero no nonzero number is represented: r_L(n) = 0 for n ≠ 0.

    Isometry invariance #

    source
    theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_image_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (n : ℚ) :
    ⇑e.carrierEquiv '' L.vectorsOfNorm n = M.vectorsOfNorm n

    An isometry carries each shell of the source onto the shell of the same norm of the target.

    source
    theorem TauCeti.IntegralLattice.Isometry.representationNumber_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (n : ℚ) :
    L.representationNumber n = M.representationNumber n

    Representation numbers are isometry invariants.