Lattices

Let A be an R-algebra and V an A-module. Then an R-submodule M of V is a lattice, if M is finitely generated and spans V as an A-module.

The typical use case is A = K is the fraction field of an integral domain R and V = ι → K for some finite ι. The scalar multiple a lattice by a unit in K is again a lattice. This gives rise to a homothety relation.

When R is a DVR and ι = Fin 2, then by taking the quotient of the type of R-lattices in ι → K by the homothety relation, one obtains the vertices of what is called the Bruhat-Tits tree of GL 2 K.

Main definitions

• Submodule.IsLattice: An R-submodule M of V is a lattice, if it is finitely generated and its A-span is V.

Main properties

Let R be a PID and A = K its field of fractions.

• Submodule.IsLattice.free: Every lattice in V is R-free.
• Basis.extendOfIsLattice: Any R-basis of a lattice M in V defines a K-basis of V.
• Submodule.IsLattice.rank: The R-rank of a lattice in V is equal to the K-rank of V.
• Submodule.IsLattice.inf: The intersection of two lattices is a lattice.

Note

In the case R = ℤ and A = K a field, there is also IsZLattice where the finitely generated condition is replaced by having the discrete topology. This is for example used for complex tori.

class Submodule.IsLattice {R : Type u_1} [CommRing R] (A : outParam (Type u_2)) [CommRing A] [Algebra R A] {V : Type u_3} [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V] [Algebra R A] [IsScalarTower R A V] (M : Submodule R V) : Prop

An R-submodule M of V is a lattice if it is finitely generated and spans V as an A-module.

Note 1: A is marked as an outParam here. In practice this should not cause issues, since R and A are fixed, where typically A is the fraction field of R.

Note 2: In the case R = ℤ and A = K a field, there is also IsZLattice where the finitely generated condition is replaced by having the discrete topology.

• fg : M.FG
• span_eq_top : span A ↑M = ⊤

instance Submodule.IsLattice.finite {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] {V : Type u_3} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] (M : Submodule R V) [IsLattice A M] : Module.Finite R ↥M

Any R-lattice is finite.

instance Submodule.IsLattice.smul {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] {V : Type u_3} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] (M : Submodule R V) [IsLattice A M] (a : Aˣ) : IsLattice A (a • M)

The action of Aˣ on R-submodules of V preserves IsLattice.

theorem Submodule.IsLattice.of_le_of_isLattice_of_fg {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] {V : Type u_3} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] {M N : Submodule R V} (hle : M ≤ N) [IsLattice A M] (hfg : N.FG) : IsLattice A N

instance Submodule.IsLattice.sup {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] {V : Type u_3} [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] (M N : Submodule R V) [IsLattice A M] [IsLattice A N] : IsLattice A (M ⊔ N)

The supremum of two lattices is a lattice.

theorem Submodule.span_range_eq_top_of_injective_of_rank_le {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {M N : Type u} [IsDomain R] [IsFractionRing R K] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module K N] [IsScalarTower R K N] [Module.Finite K N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) (h : Module.rank K N ≤ Module.rank R M) : span K ↑(LinearMap.range f) = ⊤

noncomputable def Basis.extendOfIsLattice {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsFractionRing R K] {κ : Type u_4} {M : Submodule R V} [Submodule.IsLattice K M] (b : Basis κ R ↥M) : Basis κ K V

Any basis of an R-lattice in V defines a K-basis of V.

Equations

• Basis.extendOfIsLattice K b = Basis.mk ⋯ ⋯

@[simp]

theorem Basis.extendOfIsLattice_apply {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsFractionRing R K] {κ : Type u_4} {M : Submodule R V} [Submodule.IsLattice K M] (b : Basis κ R ↥M) (k : κ) : (extendOfIsLattice K b) k = ↑(b k)

theorem Submodule.IsLattice.of_rank_le {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsDomain R] [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V} (hfg : M.FG) (hr : Module.rank K V ≤ Module.rank R ↥M) : IsLattice K M

A finitely-generated R-submodule of V of rank at least the K-rank of V is a lattice.

instance Submodule.IsLattice.free {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsDomain R] [IsPrincipalIdealRing R] [NoZeroSMulDivisors R K] (M : Submodule R V) [IsLattice K M] : Module.Free R ↥M

Any lattice over a PID is a free R-module. Note that under our conditions, NoZeroSMulDivisors R K simply says that algebraMap R K is injective.

theorem Submodule.IsLattice.rank' {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsDomain R] [IsPrincipalIdealRing R] [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] : Module.rank R ↥M = Module.rank K V

Any lattice has R-rank equal to the K-rank of V.

theorem Submodule.IsLattice.rank_of_pi {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsDomain R] [IsPrincipalIdealRing R] {ι : Type u_4} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K)) [IsLattice K M] : Module.rank R ↥M = ↑(Fintype.card ι)

Any R-lattice in ι → K has #ι as R-rank.

theorem Submodule.IsLattice.finrank_of_pi {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsDomain R] [IsPrincipalIdealRing R] {ι : Type u_4} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K)) [IsLattice K M] : Module.finrank R ↥M = Fintype.card ι

Module.finrank version of IsLattice.rank.

instance Submodule.IsLattice.inf {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsDomain R] [IsPrincipalIdealRing R] [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V) [IsLattice K M] [IsLattice K N] : IsLattice K (M ⊓ N)

The intersection of two lattices is a lattice.