Documentation

TauCeti.LinearAlgebra.IntegralLattice.Even

Even integral lattices #

An integral lattice is even when the integral norm of every lattice vector is an even integer. This file characterizes evenness on generating sets, integral bases, and Gram matrices, and establishes non-existence results for odd or non-even norm vectors in even lattices. It also proves that evenness is invariant under integral-lattice isometry.

The basis characterization is the practical entry point: a lattice given by a Gram matrix is even exactly when every diagonal entry is even. In particular, off-diagonal entries impose no parity condition, because they occur twice in the norm of an integral linear combination.

Main definitions and results #

References #

Evenness #

source
def TauCeti.IntegralLattice.IsEven {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
Prop

An integral lattice is even when the norm of every lattice vector is an even integer.

Equations
Instances For
    source
    theorem TauCeti.IntegralLattice.even_integralNorm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
    Even (L.integralNorm x) ↔ ∃ (z : ℤ), L.norm ↑x = 2 * ↑z

    Pointwise equivalence between evenness of the integral norm and two-divisibility of the rational norm in ℚ.

    source
    theorem TauCeti.IntegralLattice.isEven_iff_forall_norm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsEven ↔ ∀ (x : ↥L.carrier), ∃ (z : ℤ), L.norm ↑x = 2 * ↑z

    Evenness is equivalently the existence of an integer halving every lattice-vector norm.

    source
    theorem TauCeti.IntegralLattice.IsEven.exists_norm_eq_two_mul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) (x : ↥L.carrier) :
    ∃ (z : ℤ), L.norm ↑x = 2 * ↑z

    The norm of a vector in an even lattice is twice an integer, as an equality in ℚ.

    source
    theorem TauCeti.IntegralLattice.even_integralNorm_add {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {x y : ↥L.carrier} (hx : Even (L.integralNorm x)) (hy : Even (L.integralNorm y)) :
    Even (L.integralNorm (x + y))

    The sum of two vectors with even integral norm again has even integral norm.

    source
    theorem TauCeti.IntegralLattice.even_integralNorm_zsmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {x : ↥L.carrier} (hx : Even (L.integralNorm x)) (a : ℤ) :
    Even (L.integralNorm (a • x))

    Every integer multiple of a vector with even integral norm has even integral norm.

    source
    theorem TauCeti.IntegralLattice.isEven_of_span {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {s : Set ↥L.carrier} (hs : Submodule.span ℤ s = ⊤) (h : ∀ x ∈ s, Even (L.integralNorm x)) :
    L.IsEven

    It is enough to check evenness on any ℤ-spanning subset of lattice vectors.

    source
    theorem TauCeti.IntegralLattice.isEven_iff_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} (L : IntegralLattice V) (b : Module.Basis ι ℤ ↥L.carrier) :
    L.IsEven ↔ ∀ (i : ι), Even (L.integralNorm (b i))

    It is enough to check evenness on the vectors of any integral basis.

    source
    theorem TauCeti.IntegralLattice.isEven_ofBasis_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) :
    (ofBasis b B hB hint).IsEven ↔ ∀ (i : ι), ∃ (z : ℤ), (B (b i)) (b i) = 2 * ↑z

    An ofBasis lattice is even exactly when every basis vector has an even self-pairing.

    source
    theorem TauCeti.IntegralLattice.isEven_ofGramMatrix_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) :
    (ofGramMatrix b G hG).IsEven ↔ ∀ (i : ι), Even (G i i)

    A lattice constructed from a Gram matrix is even exactly when every diagonal entry is even.

    source
    theorem TauCeti.IntegralLattice.isEven_iff_of_integralForm_equiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {M : Type u_1} [AddCommGroup M] [Module ℤ M] (B : LinearMap.BilinForm ℤ M) (e : M ≃ₗ[ℤ] ↥L.carrier) (hB : ∀ (x : M), (L.integralForm (e x)) (e x) = (B x) x) :
    L.IsEven ↔ ∀ (x : M), Even ((B x) x)

    An equivalence preserving self-pairings identifies lattice evenness with even self-pairings in an arbitrary integral module.

    source
    theorem TauCeti.IntegralLattice.Isometry.isEven_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
    L.IsEven ↔ M.IsEven

    Evenness is invariant under integral-lattice isometry.

    Prescribed norm properties for even lattices #

    source
    theorem TauCeti.IntegralLattice.IsEven.exists_eq_two_mul_of_mem_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsEven) {n : ℚ} {x : ↥L.carrier} (hx : x ∈ L.vectorsOfNorm n) :
    ∃ (z : ℤ), n = 2 * ↑z

    A norm represented by an even lattice is twice an integer.

    source
    theorem TauCeti.IntegralLattice.IsEven.vectorsOfNorm_eq_empty_of_not_even {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) {n : ℤ} (hn : ¬Even n) :
    L.vectorsOfNorm ↑n = ∅

    An even lattice has no vector of integer norm that is odd.

    source
    theorem TauCeti.IntegralLattice.IsEven.vectorsOfNorm_eq_empty_of_not_exists_two_mul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) {n : ℚ} (hn : ¬∃ (z : ℤ), n = 2 * ↑z) :
    L.vectorsOfNorm n = ∅

    An even lattice has no vector of a rational norm that is not twice an integer.