# ℤ-lattices #

Let E be a finite dimensional vector space over a NormedLinearOrderedField K with a solid norm that is also a FloorRing, e.g. ℝ. A (full) ℤ-lattice L of E is a discrete subgroup of E such that L spans E over K.

A ℤ-lattice L can be defined in two ways:

• For b a basis of E, then L = Submodule.span ℤ (Set.range b) is a ℤ-lattice of E
• As an AddSubgroup E with the additional properties:
• DiscreteTopology L, that is L is discrete
• Submodule.span ℝ (L : Set E) = ⊤, that is L spans E over K.

Results about the first point of view are in the Zspan namespace and results about the second point of view are in the Zlattice namespace.

## Main results #

• Zspan.isAddFundamentalDomain: for a ℤ-lattice Submodule.span ℤ (Set.range b), proves that the set defined by Zspan.fundamentalDomain is a fundamental domain.
• Zlattice.module_free: an AddSubgroup of E that is discrete and spans E over K is a free ℤ-module
• Zlattice.rank: an AddSubgroup of E that is discrete and spans E over K is a free ℤ-module of ℤ-rank equal to the K-rank of E
theorem Zspan.span_top {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) :
def Zspan.fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) :
Set E

The fundamental domain of the ℤ-lattice spanned by b. See Zspan.isAddFundamentalDomain for the proof that it is a fundamental domain.

Equations
• = {m : E | ∀ (i : ι), (b.repr m) i Set.Ico 0 1}
Instances For
@[simp]
theorem Zspan.mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) {m : E} :
∀ (i : ι), (b.repr m) i Set.Ico 0 1
theorem Zspan.map_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) {F : Type u_4} [] (f : E ≃ₗ[K] F) :
@[simp]
theorem Zspan.fundamentalDomain_reindex {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) {ι' : Type u_4} (e : ι ι') :
Zspan.fundamentalDomain (b.reindex e) =
theorem Zspan.fundamentalDomain_pi_basisFun {ι : Type u_2} [] :
= Set.univ.pi fun (x : ι) => Set.Ico 0 1
def Zspan.floor {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) :

The map that sends a vector of E to the element of the ℤ-lattice spanned by b obtained by rounding down its coordinates on the basis b.

Equations
Instances For
def Zspan.ceil {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) :

The map that sends a vector of E to the element of the ℤ-lattice spanned by b obtained by rounding up its coordinates on the basis b.

Equations
Instances For
@[simp]
theorem Zspan.repr_floor_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (i : ι) :
(b.repr (Zspan.floor b m)) i = (b.repr m) i
@[simp]
theorem Zspan.repr_ceil_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (i : ι) :
(b.repr (Zspan.ceil b m)) i = (b.repr m) i
@[simp]
theorem Zspan.floor_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (h : m ) :
(Zspan.floor b m) = m
@[simp]
theorem Zspan.ceil_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (h : m ) :
(Zspan.ceil b m) = m
def Zspan.fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) :
E

The map that sends a vector E to the fundamentalDomain of the lattice, see Zspan.fract_mem_fundamentalDomain, and fractRestrict for the map with the codomain restricted to fundamentalDomain.

Equations
Instances For
theorem Zspan.fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) :
= m - (Zspan.floor b m)
@[simp]
theorem Zspan.repr_fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (i : ι) :
(b.repr (Zspan.fract b m)) i = Int.fract ((b.repr m) i)
@[simp]
theorem Zspan.fract_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) :
@[simp]
theorem Zspan.fract_zspan_add {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) {v : E} (h : v ) :
Zspan.fract b (v + m) =
@[simp]
theorem Zspan.fract_add_zspan {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) {v : E} (h : v ) :
Zspan.fract b (m + v) =
theorem Zspan.fract_eq_self {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] {b : Basis ι K E} [] [] {x : E} :
= x
theorem Zspan.fract_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : E) :
def Zspan.fractRestrict {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : E) :

The map fract with codomain restricted to fundamentalDomain.

Equations
• = ⟨,
Instances For
theorem Zspan.fractRestrict_surjective {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] :
@[simp]
theorem Zspan.fractRestrict_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : E) :
=
theorem Zspan.fract_eq_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (m : E) (n : E) :
= -m + n
theorem Zspan.norm_fract_le {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] [] (m : E) :
i : ι, b i
@[simp]
theorem Zspan.coe_floor_self {ι : Type u_2} {K : Type u_3} [] [] [] (k : K) :
@[simp]
theorem Zspan.coe_fract_self {ι : Type u_2} {K : Type u_3} [] [] [] (k : K) :
theorem Zspan.fundamentalDomain_isBounded {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] [] :
theorem Zspan.vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (y : (Submodule.span (Set.range b))) (x : E) :
y = -
theorem Zspan.exist_unique_vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : E) :
∃! v : (Submodule.span (Set.range b)),
def Zspan.quotientEquiv {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] :
E

The map Zspan.fractRestrict defines an equiv map between E ⧸ span ℤ (Set.range b) and Zspan.fundamentalDomain b.

Equations
Instances For
@[simp]
theorem Zspan.quotientEquiv_apply_mk {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : E) :
@[simp]
theorem Zspan.quotientEquiv.symm_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [] (b : Basis ι K E) [] [] (x : ) :
.symm x =
theorem Zspan.fundamentalDomain_subset_parallelepiped {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] :
theorem Zspan.fundamentalDomain_measurableSet {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] [] :
theorem Zspan.isAddFundamentalDomain {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] [] (μ : ) :

For a ℤ-lattice Submodule.span ℤ (Set.range b), proves that the set defined by Zspan.fundamentalDomain is a fundamental domain.

theorem Zspan.measure_fundamentalDomain_ne_zero {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] [] [] {μ : } [μ.IsAddHaarMeasure] :
0
theorem Zspan.measure_fundamentalDomain {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] [] [] (μ : ) [] [μ.IsAddHaarMeasure] (b₀ : Basis ι E) :
= ENNReal.ofReal |b₀.det b| * μ
@[simp]
theorem Zspan.volume_fundamentalDomain {ι : Type u_2} [] [] (b : Basis ι (ι)) :
MeasureTheory.volume = ENNReal.ofReal |(Matrix.of b).det|
theorem Zspan.fundamentalDomain_ae_parallelepiped {E : Type u_1} {ι : Type u_2} [] (b : Basis ι E) [] [] (μ : ) [] [μ.IsAddHaarMeasure] :
class IsZlattice (K : Type u_1) [] {E : Type u_2} [] (L : ) [] :

An L : Addsubgroup E where E is a vector space over a normed field K is a ℤ-lattice if it is discrete and spans E over K.

• span_top : =

L spans the full space E over K.

Instances
theorem IsZlattice.span_top {K : Type u_1} [] {E : Type u_2} [] {L : } [] [self : ] :

L spans the full space E over K.

theorem Zspan.isZlattice {E : Type u_1} {ι : Type u_2} [] [] (b : Basis ι E) :
theorem Zlattice.FG (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] [hs : ] :
L.FG
theorem Zlattice.module_finite (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] [] :
instance instModuleFinite_of_discrete_addSubgroup {E : Type u_3} [] [] (L : ) [] :
Equations
• =
theorem Zlattice.module_free (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] [] :
instance instModuleFree_of_discrete_addSubgroup {E : Type u_3} [] [] (L : ) [] :
Equations
• =
theorem Zlattice.rank (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] [hs : ] :
def Basis.ofZlatticeBasis (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] {ι : Type u_3} [hs : ] (b : Basis ι L) :
Basis ι K E

Any ℤ-basis of L is also a K-basis of E.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Basis.ofZlatticeBasis_apply (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] {ι : Type u_3} [hs : ] (b : Basis ι L) (i : ι) :
i = (b i)
@[simp]
theorem Basis.ofZlatticeBasis_repr_apply (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] {ι : Type u_3} [hs : ] (b : Basis ι L) (x : L) (i : ι) :
(.repr x) i = ((b.repr x) i)
theorem Basis.ofZlatticeBasis_span (K : Type u_1) [] [] {E : Type u_2} [] [] [] (L : ) [] {ι : Type u_3} [hs : ] (b : Basis ι L) :