Scaling a lattice

For a ℤ-submodule L of a real vector space E and c : ℝ, the scaled lattice c • L is the image of L under multiplication by c, Mathlib's pointwise action of ℝ on Submodule ℤ E. This file records how the dual, the covolume, the determinant and the integrality, evenness and unimodularity of a lattice in a real inner product space behave under scaling.

For c ≠ 0 the lattice c • L is the pullback of L along the linear automorphism c⁻¹ • · (ZLattice.smul_eq_comap), so a full lattice scales to a full lattice, with dual (c • L)^∨ = c⁻¹ • L^∨, covolume |c|ⁿ covolume L and determinant c²ⁿ det L in dimension n. A negative scalar gives the same lattice as its absolute value (Submodule.neg_smul_eq_smul).

Scaling is not an invariance of any of the three predicates. The lattice c • L is integral exactly when c² ⟪x, y⟫ ∈ ℤ for all x, y ∈ L (ZLattice.isIntegral_smul_iff), and even exactly when c² ‖x‖² ∈ 2ℤ for all x ∈ L (ZLattice.isEven_smul_iff). In particular, scaling by √m for a natural number m preserves integrality: √m • L is integral when L is, and even when L is even or when L is integral and m is even, with det (√m • L) = mⁿ det L. Thus √2 • E₈ is even and integral.

In positive dimension, scaling an integral lattice by |c| > 1 never produces a unimodular lattice, since its determinant is c²ⁿ det L ≥ c²ⁿ > 1; in particular √m • L is not unimodular for m > 1, so √2 • E₈ is not unimodular. A unimodular lattice scaled by |c| ≠ 1 is never unimodular. Positive dimension is needed: the zero lattice of the zero space is even, unimodular and fixed by every scaling. Scaling down can create unimodularity, (1/√2) • (√2 ℤ) = ℤ, so the first statement does not extend to |c| < 1.

Main statements

• ZLattice.smul_eq_comap: for c ≠ 0, c • L is the pullback of L along c⁻¹ • ·.
• ZLattice.basisSmul: for c ≠ 0, a ℤ-basis b of L gives the ℤ-basis c • b of c • L.
• ZLattice.exists_forall_ne_zero_lt_norm: scaling up the integer span of a basis gives full lattices all of whose nonzero vectors are longer than a prescribed bound.
• ZLattice.exists_forall_add_mem_eq_zero_of_isBounded: a bounded set meets none of its translates by the nonzero vectors of such a lattice.
• ZLattice.dual_smul: (c • L)^∨ = c⁻¹ • L^∨ for c ≠ 0.
• ZLattice.covolume_smul, ZLattice.det_smul: covolume (c • L) = |c|ⁿ covolume L and det (c • L) = c²ⁿ det L (for c = 0 in positive dimension both sides vanish).
• ZLattice.covolume_natCast_smul: covolume (c • L) = cⁿ covolume L for a natural number c.
• ZLattice.isIntegral_smul_iff, ZLattice.isEven_smul_iff: the exact criteria for c • L to be integral or even.
• ZLattice.IsIntegral.sqrt_smul, ZLattice.IsEven.sqrt_smul, ZLattice.IsIntegral.isEven_sqrt_smul: √m • L is integral when L is, and even when L is even or when L is integral and m is even.
• ZLattice.det_sqrt_smul, ZLattice.IsIntegral.card_discriminantGroup_sqrt_smul: det (√m • L) = mⁿ det L (and |A_{√m • L}| = mⁿ |A_L| for integral L and m ≠ 0), and ZLattice.det_sqrt_smul_span_orthonormalBasis: det (√m • ℤⁿ) = mⁿ.
• ZLattice.IsIntegral.not_isUnimodular_smul, ZLattice.IsIntegral.not_isUnimodular_sqrt_smul, ZLattice.IsUnimodular.not_isUnimodular_smul: in positive dimension, scaling an integral lattice by |c| > 1, or a unimodular lattice by |c| ≠ 1, does not give a unimodular lattice.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 1.
• J. H. Conway, N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Springer, 1999, Chapter 2, §2.

Source note

The statements and proofs of this file adapt the Tau Ceti formalization in TauCeti PR #20860 by @tauceti-ai-for-science.

Evenness

theorem ZLattice.isEven_smul_iff {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) (c : ℝ) : IsEven (c • L) ↔ ∀ x ∈ L, ∃ (m : ℤ), c ^ 2 * ‖x‖ ^ 2 = 2 * ↑m

The scaled lattice c • L is even exactly when c² ‖x‖² ∈ 2ℤ for every x ∈ L.

theorem ZLattice.IsEven.sqrt_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} (h : IsEven L) (m : ℕ) : IsEven (√↑m • L)

Scaling an even lattice by the square root of a natural number gives an even lattice.

Scaling as a change of variables

theorem ZLattice.smul_eq_comap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {c : ℝ} (hc : c ≠ 0) : c • L = ZLattice.comap ℝ L ↑↑(ContinuousLinearEquiv.smulLeft (Units.mk0 c hc)⁻¹)

For c ≠ 0, the scaled lattice c • L is the pullback of L along the linear automorphism x ↦ c⁻¹ • x.

instance ZLattice.instDiscreteTopologySubtypeMemSubmoduleIntHSMulRealOfNeZero_tauCeti {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (c : ℝ) [NeZero c] : DiscreteTopology ↥(c • L)

Scaling a discrete lattice by a nonzero scalar gives a discrete lattice.

instance ZLattice.instIsZLatticeRealHSMulSubmoduleInt_tauCeti {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (c : ℝ) [NeZero c] : IsZLattice ℝ (c • L)

Scaling a full lattice by a nonzero scalar gives a full lattice.

noncomputable def ZLattice.basisSmul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {ι : Type u_2} (b : Module.Basis ι ℤ ↥L) {c : ℝ} (hc : c ≠ 0) : Module.Basis ι ℤ ↥(c • L)

For c ≠ 0, a ℤ-basis b of L scales to the ℤ-basis c • b of c • L.

@[simp]

theorem ZLattice.coe_basisSmul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {ι : Type u_2} (b : Module.Basis ι ℤ ↥L) {c : ℝ} (hc : c ≠ 0) (i : ι) : ↑((basisSmul b hc) i) = c • ↑(b i)

The i-th vector of the scaled basis basisSmul b hc is c • b i.

Lattices with long nonzero vectors

theorem ZLattice.exists_forall_ne_zero_lt_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (R : ℝ) : ∃ (L : Submodule ℤ E) (x : DiscreteTopology ↥L) (_ : IsZLattice ℝ L), ∀ ℓ ∈ L, ℓ ≠ 0 → R < ‖ℓ‖

A finite-dimensional real normed space has full lattices whose nonzero vectors are all longer than any prescribed R.

theorem ZLattice.exists_forall_add_mem_eq_zero_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ (L : Submodule ℤ E) (x : DiscreteTopology ↥L) (_ : IsZLattice ℝ L), ∀ x ∈ s, ∀ ℓ ∈ L, x + ℓ ∈ s → ℓ = 0

A bounded subset s of a finite-dimensional real normed space meets none of its translates by the nonzero vectors of some full lattice L.

@[simp]

theorem ZLattice.covolume_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {c : ℝ} (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] : covolume (c • L) μ = |c| ^ Module.finrank ℝ E * covolume L μ

Scaling a full lattice by c multiplies its covolume by |c|ⁿ, where n is the dimension of the space, for any Haar measure. For c = 0 in positive dimension both sides vanish: the zero lattice has the whole space as a fundamental domain, of infinite measure.

theorem ZLattice.covolume_natCast_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (c : ℕ) (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] : covolume (↑c • L) μ = ↑c ^ Module.finrank ℝ E * covolume L μ

Scaling a full lattice by a natural number c multiplies its covolume by cⁿ, where n is the dimension of the space, for any Haar measure.

Duality, integrality and the determinant

@[simp]

theorem ZLattice.dual_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) {c : ℝ} (hc : c ≠ 0) : dual (c • L) = c⁻¹ • dual L

The dual of the scaled lattice c • L is c⁻¹ • L^∨, for c ≠ 0.

theorem ZLattice.isIntegral_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (c : ℝ) : IsIntegral (c • L) ↔ ∀ x ∈ L, ∀ y ∈ L, ∃ (m : ℤ), c ^ 2 * inner ℝ x y = ↑m

The scaled lattice c • L is integral exactly when c² ⟪x, y⟫ ∈ ℤ for all x, y ∈ L.

theorem ZLattice.IsIntegral.sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsIntegral L) (m : ℕ) : IsIntegral (√↑m • L)

Scaling an integral lattice by the square root of a natural number gives an integral lattice.

theorem ZLattice.IsIntegral.isEven_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsIntegral L) {m : ℕ} (hm : Even m) : IsEven (√↑m • L)

Scaling an integral lattice by the square root of an even natural number gives an even lattice.

@[simp]

theorem ZLattice.det_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {c : ℝ} : det (c • L) = c ^ (2 * Module.finrank ℝ E) * det L

Scaling a full lattice by c multiplies its determinant by c²ⁿ, where n is the dimension of the space.

theorem ZLattice.det_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] {m : ℕ} : det (√↑m • L) = ↑m ^ Module.finrank ℝ E * det L

Scaling a full lattice by √m, for a natural number m, multiplies its determinant by mⁿ, where n is the dimension of the space.

theorem ZLattice.det_sqrt_smul_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) {m : ℕ} : det (√↑m • Submodule.span ℤ (Set.range ⇑b)) = ↑m ^ Module.finrank ℝ E

For an orthonormal basis b and a natural number m, the scaled cubic lattice √m • ℤ b has determinant mⁿ, where n is the dimension of the space. For instance √2 ℤ² has determinant 4.

theorem ZLattice.natCard_discriminantGroup_sqrt_smul_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) {m : ℕ} (hm : m ≠ 0) : Nat.card (DiscriminantGroup (√↑m • Submodule.span ℤ (Set.range ⇑b))) = m ^ Module.finrank ℝ E

For an orthonormal basis b and a nonzero natural number m, the discriminant group of the scaled cubic lattice √m • ℤ b has order det (√m • ℤ b) = mⁿ, where n is the dimension of the space. For instance the discriminant group (ℤ/2)² of √2 ℤ² has order 4.

theorem ZLattice.IsIntegral.card_discriminantGroup_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) {m : ℕ} (hm : m ≠ 0) : Nat.card (DiscriminantGroup (√↑m • L)) = m ^ Module.finrank ℝ E * Nat.card (DiscriminantGroup L)

Scaling an integral full lattice L of rank n by √m (m ≠ 0) multiplies the order of its discriminant group by mⁿ.

theorem ZLattice.IsIntegral.not_isUnimodular_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] (h : IsIntegral L) {c : ℝ} (hc : 1 < |c|) : ¬IsUnimodular (c • L)

In positive dimension, scaling a full integral lattice by c with 1 < |c| never gives a unimodular lattice: the determinant becomes c²ⁿ det L > 1.

theorem ZLattice.IsIntegral.not_isUnimodular_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] (h : IsIntegral L) {m : ℕ} (hm : 1 < m) : ¬IsUnimodular (√↑m • L)

In positive dimension, scaling a full integral lattice by √m for a natural number m > 1 never gives a unimodular lattice. For instance √2 • E₈ is even and integral but not unimodular.

theorem ZLattice.IsUnimodular.not_isUnimodular_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] (h : IsUnimodular L) {c : ℝ} (hc : |c| ≠ 1) : ¬IsUnimodular (c • L)

In positive dimension, scaling a unimodular lattice by c with |c| ≠ 1 never gives a unimodular lattice.