Quotients by full lattices: compactness, circle coordinates and L / cL #
Let L : Submodule ℤ E be a full lattice, IsZLattice ℝ L, in a finite-dimensional real normed
space E. The orbit space AddAction.orbitRel.Quotient L E of translation by L, with the
additive group structure of E ⧸ L (Submodule.orbitRelQuotientAddEquiv), is the image of a
compact fundamental parallelepiped of the lattice, so it is compact. For a complex vector space
E this is the compactness of the complex torus E / L.
A lattice basis also supplies circle coordinates on the quotient: reduce its real coordinates
modulo one. The resulting Module.Basis.quotientLatticeEquiv is an isomorphism of topological
additive groups onto a product of additive circles.
If L ∩ V is a full lattice in a subspace V, the map V / (L ∩ V) → E / L induced by the
inclusion is a closed embedding, so the compact torus V / (L ∩ V) is identified with a closed
subgroup of E / L.
For a linear map f : E → E' carrying L into a subgroup L' of E', the inclusion of ker f
induces a map from ker f / (L ∩ ker f) into the kernel f⁻¹(L') / L of the induced map
E / L → E' / L'.
For c : ℕ, the lattice cL is (c : ℝ) • L, read in L through Submodule.submoduleOf. The
quotient L / cL has c ^ n elements when L has rank n, so it is finite for c ≠ 0, and
for c ≠ 0 a ℤ-basis of L identifies it with (ℤ / c)^n by reducing coordinates modulo c.
Main results #
Submodule.instCompactSpaceOrbitRelQuotient: the translation orbit space is compact.QuotientAddGroup.instCompactSpaceOfIsZLattice,Submodule.instCompactSpaceQuotientToAddSubgroup: the additive quotient is compact.Module.Basis.latticeCircleCoordinates: the continuous homomorphism of circle coordinates.Module.Basis.quotientLatticeEquiv: the quotient is a product of additive circles.Module.Basis.orbitRelQuotientLatticeEquiv: the same circle coordinates on the orbit space.Submodule.isClosedEmbedding_orbitRelQuotientMap_subtype: ifL ∩ Vis a full lattice inV, thenV / (L ∩ V) → E / Lis a closed embedding.Submodule.orbitRelQuotientToKerOrbitRelQuotientMap: for a linear mapfcarryingLintoL', the mapker f / (L ∩ ker f) → f⁻¹(L') / Linto the kernel of the induced mapE / L → E' / L', induced by the inclusion ofker f.ZLattice.card_quotient_smul_submoduleOf:L / cLhasc ^ nelements for a full latticeLof rankn; it is finite forc ≠ 0.Module.Basis.quotientSmulEquivPiZMod: forc ≠ 0, the coordinates modulocin aℤ-basis ofLidentifyL / cLwith(ℤ / c)^n.
References #
- Christina Birkenhake and Herbert Lange, Complex Abelian Varieties, second edition, Grundlehren der mathematischen Wissenschaften 302, Springer, 2004, Chapter 1, Section 1.1.
The quotient of a finite-dimensional real normed space by a full lattice is compact: it is the image of a compact fundamental parallelepiped of the lattice.
The additive quotient of a finite-dimensional real normed space by a full lattice is compact.
The additive quotient of a finite-dimensional real normed space by the additive subgroup of a
full lattice L : Submodule ℤ E is compact.
Real coordinates in a lattice basis, reduced modulo one.
Instances For
The vectors with integral lattice coordinates are exactly the lattice.
Every tuple of circle coordinates is realized by a vector.
A lattice basis identifies the quotient by the lattice with a product of additive circles.
The i-th coordinate of a vector is its i-th real basis coordinate modulo one.
Instances For
The inverse circle-coordinate map sends reduced real coordinates to their linear combination in the lattice basis, modulo the lattice.
A lattice basis identifies the orbit space E / L of translation by the lattice with a product
of additive circles: Module.Basis.quotientLatticeEquiv, read on the orbit space through
Submodule.orbitRelQuotientContinuousAddEquiv.
Instances For
The i-th circle coordinate of the orbit of x is the i-th real basis coordinate of x
modulo one.
The inverse circle coordinates send reduced real coordinates to the orbit of their linear combination in the lattice basis.
Subtori #
If L ∩ V is a full lattice in a subspace V, then the map of quotients
V / (L ∩ V) → E / L induced by the inclusion of V is a closed embedding: the compact torus
V / (L ∩ V) is identified with its image, a closed subgroup of E / L.
The kernel inclusion #
For a linear map f : E → E' carrying the subgroup L ≤ E into L' ≤ E', the map
ker f / (L ∩ ker f) → f⁻¹(L') / L induced by the inclusion of ker f: the map of orbit spaces
induced by (LinearMap.ker f).subtype, with its codomain restricted to the kernel f⁻¹(L') / L
of the map E / L → E' / L' induced by f.
When f is a continuous real or complex linear map of finite-dimensional spaces, L is a full
lattice and L' is discrete, its domain is the torus ker f / (L ∩ ker f) and its image is the
identity component of the kernel (Submodule.range_orbitRelQuotientMap_ker_subtype).
Instances For
Followed by the inclusion of the kernel into E / L,
Submodule.orbitRelQuotientToKerOrbitRelQuotientMap is the map of quotients induced by the
inclusion of ker f.
The orbit of x ∈ ker f in ker f / (L ∩ ker f) is sent to the orbit of x in E / L.
The quotient L / cL #
A vector of L lies in cL = (c : ℝ) • L exactly when it is c times a vector of L.
For c : ℕ, the lattice cL = (c : ℝ) • L is contained in L.
The lattice cL is the image of multiplication by c on L, the submodule that Mathlib's
ModN L c quotients by.
For a ℤ-basis b of L and c ≠ 0, reduction modulo c of the coordinates in b
identifies L / cL with (ℤ / c)^ι. This is the coordinate map of the basis ModN.basis b of
L / cL over ℤ / c.
Instances For
The class of v ∈ L has the coordinates of v in b, reduced modulo c.
The class in L / cL with coordinates x modulo c in b is the class of
∑ i, (x i).val • b i, the combination of b with the least natural representatives of the
coordinates.
The quotient L / cL of a full lattice of rank n has c ^ n elements. For c = 0 this
reads Nat.card L = 0 ^ n: the lattice is infinite unless n = 0.
The finite quotient L / cL as a Fintype, so that finite sums over it, such as the Gauss
sums of a lattice, elaborate for a full lattice and c ≠ 0.