The orthogonal direct sum of two lattices #
For ℤ-submodules L of a real inner product space E and M of a real inner product space
F, the orthogonal direct sum L ⊕ M is the submodule L × M of the L² product
WithLp 2 (E × F), whose inner product is ⟪(x, y), (x', y')⟫ = ⟪x, x'⟫ + ⟪y, y'⟫
(ZLattice.orthSum).
The dual of an orthogonal direct sum is the orthogonal direct sum of the duals
(ZLattice.dual_orthSum). Consequently L ⊕ M is integral, even or unimodular exactly when both
L and M are; in particular each of the three predicates is preserved by orthogonal direct sums.
When L and M are full lattices in finite-dimensional spaces, so is L ⊕ M: the sum of the
ℤ-spans of two ℝ-bases is the ℤ-span of the product basis (ZLattice.orthSum_span_basis).
The Gram matrix of the product basis is block diagonal, so covolumes and determinants multiply:
covolume (L ⊕ M) = covolume L * covolume M and det (L ⊕ M) = det L * det M.
Since ‖(x, y)‖² = ‖x‖² + ‖y‖², a vector of L ⊕ M of squared norm t is a pair of vectors of
L and M of squared norms s and t - s, where s ≤ t runs over the finitely many squared
norms represented by L. The representation numbers of L ⊕ M are therefore the convolution
r_{L ⊕ M}(t) = ∑_s r_L(s) * r_M(t - s) of those of the summands; for even L this is the finite
sum r_{L ⊕ M}(2m) = ∑_{i ≤ m} r_L(2i) * r_M(2(m - i)), and for integral L the sum
r_{L ⊕ M}(n) = ∑_{i ≤ n} r_L(i) * r_M(n - i).
Orthogonal direct sums build integral, even or unimodular lattices of large rank from small ones,
for instance the even unimodular lattice E₈ ⊕ E₈ of rank 16.
Main definitions #
ZLattice.orthSum L M: the orthogonal direct sum ofLandM, inWithLp 2 (E × F).ZLattice.orthSumEquivProd L M: the identification ofL ⊕ MwithL × Masℤ-modules.ZLattice.quotientSmulOrthSumEquiv L M c: the identification of(L ⊕ M) / c (L ⊕ M)with(L / cL) × (M / cM).ZLattice.dualOrthSumEquiv L M,ZLattice.discriminantGroupOrthSumEquiv L M: theℤ-linear identifications(L ⊕ M)^∨ ≃ₗ[ℤ] L^∨ × M^∨andA_{L ⊕ M} ≃ₗ[ℤ] A_L × A_M.
Main statements #
ZLattice.dual_orthSum:(L ⊕ M)^∨ = L^∨ ⊕ M^∨.ZLattice.card_discriminantGroup_orthSum: the order of the discriminant group ofL ⊕ Mis the product of the orders of the discriminant groups ofLandM.ZLattice.isIntegral_orthSum_iff,ZLattice.isEven_orthSum_iff,ZLattice.isUnimodular_orthSum_iff:L ⊕ Mis integral, even or unimodular if and only if bothLandMare.ZLattice.representationNumber_orthSum,ZLattice.representationNumber_orthSum_eq_sum: the representation numbers ofL ⊕ Mare the convolution of those ofLandM, summed over the squared normss ≤ trepresented byL, or over any finite set containing them.ZLattice.IsEven.representationNumber_orthSum,ZLattice.IsIntegral.representationNumber_orthSum: the convolution as a sum overFinset.rangefor even and for integralL.ZLattice.covolume_orthSum,ZLattice.det_orthSum: covolumes and determinants of full lattices multiply under orthogonal direct sums.
References #
- W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 1.
- J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 2, §2.3.
The orthogonal direct sum of lattices L ⊆ E and M ⊆ F: the vectors of the L² product
WithLp 2 (E × F) whose components lie in L and in M (mem_orthSum).
Instances For
A vector lies in the orthogonal direct sum exactly when its two components lie in the summands.
As a ℤ-module, the orthogonal direct sum L ⊕ M is the product L × M: a vector of L ⊕ M
corresponds to the pair of its components.
Instances For
The quotient (L ⊕ M) / c (L ⊕ M) #
The quotient (L ⊕ M) / c (L ⊕ M) is (L / cL) × (M / cM): the class of a vector of L ⊕ M
corresponds to the pair of classes of its components.
Instances For
The class of x ∈ L ⊕ M corresponds to the pair of classes of the components of x.
The dual of an orthogonal direct sum is the orthogonal direct sum of the duals.
As a ℤ-module, the dual of an orthogonal direct sum L ⊕ M is L^∨ × M^∨.
Instances For
The first component of dualOrthSumEquiv L M x is the first component of x.
The second component of dualOrthSumEquiv L M x is the second component of x.
(dualOrthSumEquiv L M).symm embeds (p.1, p.2) into WithLp 2 (E × F).
The discriminant group of an orthogonal direct sum L ⊕ M is the product of the discriminant
groups of L and M.
Instances For
The class of x ∈ (L ⊕ M)^∨ corresponds to the pair of classes of its components.
The order of the discriminant group of L ⊕ M is the product of the orders of the discriminant
groups of L and M.
Integral, even and unimodular orthogonal direct sums #
An orthogonal direct sum is integral if and only if both summands are.
An orthogonal direct sum is unimodular if and only if both summands are.
Representation numbers of an orthogonal direct sum #
The shell of squared norm t of L ⊕ M is the union, over the squared norms s ≤ t
represented by L, of the pairs of a vector of L of squared norm s and a vector of M of
squared norm t - s. Any set S containing those squared norms may index the union.
The representation numbers of an orthogonal direct sum are the convolution of those of the
summands: r_{L ⊕ M}(t) = ∑_{s ∈ S} r_L(s) * r_M(t - s) for any finite set S of real numbers
containing the squared norms s ≤ t represented by L.
The representation numbers of an orthogonal direct sum are the convolution of those of the
summands, summed over the finite set of squared norms s ≤ t represented by L:
r_{L ⊕ M}(t) = ∑_{s ≤ t represented by L} r_L(s) * r_M(t - s).
For an even lattice L, the representation numbers of L ⊕ M at even integers are the
convolution r_{L ⊕ M}(2m) = ∑_{i ≤ m} r_L(2i) * r_M(2(m - i)).
For an integral lattice L, the representation numbers of L ⊕ M at natural numbers are the
convolution r_{L ⊕ M}(n) = ∑_{i ≤ n} r_L(i) * r_M(n - i).
Full lattices #
The orthogonal direct sum of the ℤ-spans of two bases is the ℤ-span of their product
basis of WithLp 2 (E × F).
The covolume of an orthogonal direct sum of full lattices is the product of the covolumes.
The determinant of an orthogonal direct sum of full lattices is the product of the determinants.