The lattice induced on the kernel of a lattice-preserving map

Let L be a full lattice in a finite-dimensional real normed space E, and let f : E → E' be a linear map, over a normed field K such as ℝ or ℂ, which carries L into a discrete subgroup L' of E'. Then L ∩ ker f is a full lattice in the subspace ker f.

For complex tori this is the lattice of the identity component of the kernel: when f is complex linear, the kernel f⁻¹(L') / L of the induced homomorphism E / L → E' / L' has identity component the complex torus ker f / (L ∩ ker f), and this file supplies its full lattice. That identity component is the image of ker f / (L ∩ ker f) → E / L (Submodule.range_orbitRelQuotientMap_ker_subtype), and this map is a closed embedding (Submodule.isClosedEmbedding_orbitRelQuotientMap_subtype) once L ∩ ker f is a full lattice.

The hypothesis on f cannot be dropped: an irrational line through the lattice ℤ² in ℝ² is the kernel of a linear form, and it meets the lattice only in 0.

Main results

• ZLattice.isZLattice_comap_ker_subtype: if f(L) ⊆ L' with L' discrete, then L ∩ ker f is a full lattice in ker f.

References

• Christina Birkenhake and Herbert Lange, Complex Abelian Varieties, second edition, Grundlehren der mathematischen Wissenschaften 302, Springer, 2004, Chapter 1.

theorem ZLattice.isZLattice_comap_ker_subtype {K : Type u_1} [NormedField K] [NormedSpace ℝ K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace K E] [IsScalarTower ℝ K E] [FiniteDimensional ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedSpace K E'] [IsScalarTower ℝ K E'] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {L' : Submodule ℤ E'} [DiscreteTopology ↥L'] (f : E →ₗ[K] E') (hf : Submodule.map (↑ℤ f) L ≤ L') : IsZLattice ℝ (ZLattice.comap K L f.ker.subtype)

If a linear map f carries a full lattice L into a discrete subgroup L', then L ∩ ker f is a full lattice in the subspace ker f. Taking L' = f(L), it suffices that f(L) be discrete. For complex linear f this is the lattice of the complex torus ker f / (L ∩ ker f).