The content of a lattice

The content c_L of a lattice L is the greatest common divisor of the half-norms ‖x‖² / 2 of the vectors x ∈ L. It governs the level of the Fricke partner √N • L^∨ of an even lattice of level N, which is N / gcd (N, c_L).

Like the level ZLattice.level, the content is defined directly on the real model, for every ℤ-submodule of a seminormed group, so it needs no integrality hypothesis to state: it is the nonnegative generator of the ideal of ℤ spanned by the half-norms of the vectors of even squared norm. For an even lattice every vector qualifies. The content is the half-norm counterpart of the norm ideal TauCeti.IntegralLattice.normIdeal of a rational lattice, the ideal spanned by the full norms.

Main definitions

• ZLattice.content L: the nonnegative generator of the ideal of ℤ spanned by the half-norms ‖x‖² / 2 of the vectors x ∈ L of even squared norm.

Main statements

• ZLattice.span_natCast_content: the content generates the ideal spanned by the half-norms.
• ZLattice.dvd_content_iff: d divides the content exactly when it divides every half-norm.
• ZLattice.dvd_mul_content: if n divides k times every half-norm, it divides k times the content.
• ZLattice.content_comap: the content is invariant under linear isometry equivalences.
• ZLattice.content_span_two: the lattice 2 ℤ ⊆ ℝ has content 2.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 3.

noncomputable def ZLattice.content {E : Type u_1} [SeminormedAddCommGroup E] (L : Submodule ℤ E) : ℕ

The content of a lattice L: the nonnegative generator of the ideal of ℤ spanned by the half-norms ‖x‖² / 2 of the vectors x ∈ L whose squared norm is an even integer. For an even lattice every vector qualifies, and the content is the greatest common divisor of all half-norms of L (dvd_content_iff).

theorem ZLattice.span_natCast_content {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} : Ideal.span {↑(content L)} = Ideal.span {m : ℤ | ∃ x ∈ L, ‖x‖ ^ 2 = 2 * ↑m}

The content of L generates the ideal of ℤ spanned by the half-norms ‖x‖² / 2 of the vectors x ∈ L of even squared norm.

theorem ZLattice.natCast_content_mem_span {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} : ↑(content L) ∈ Ideal.span {m : ℤ | ∃ x ∈ L, ‖x‖ ^ 2 = 2 * ↑m}

The content is an integer combination of half-norms: it lies in the ideal they span.

theorem ZLattice.dvd_content_iff {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} {d : ℤ} : d ∣ ↑(content L) ↔ ∀ x ∈ L, ∀ (m : ℤ), ‖x‖ ^ 2 = 2 * ↑m → d ∣ m

d divides the content of L exactly when d divides every half-norm ‖x‖² / 2 of a vector x ∈ L of even squared norm.

theorem ZLattice.content_dvd {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} {x : E} (hx : x ∈ L) {m : ℤ} (hm : ‖x‖ ^ 2 = 2 * ↑m) : ↑(content L) ∣ m

The content of L divides every half-norm ‖x‖² / 2 of a vector x ∈ L of even squared norm.

theorem ZLattice.dvd_mul_content {E : Type u_1} [SeminormedAddCommGroup E] {L : Submodule ℤ E} {n k : ℤ} (h : ∀ x ∈ L, ∀ (m : ℤ), ‖x‖ ^ 2 = 2 * ↑m → n ∣ k * m) : n ∣ k * ↑(content L)

If n divides k times every half-norm ‖x‖² / 2 of a vector x ∈ L of even squared norm, then it divides k times the content.

@[simp]

theorem ZLattice.content_comap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {L : Submodule ℤ E} (e : F ≃ₗᵢ[ℝ] E) : content (ZLattice.comap ℝ L ↑e.toLinearEquiv) = content L

The content is invariant under linear isometry equivalences.

An example

theorem ZLattice.content_span_two : content (ℤ ∙ 2) = 2

The lattice 2 ℤ ⊆ ℝ has content 2: its half-norms are the integers 2 k².