# mathlib3documentation

algebra.module.zlattice

# ℤ-lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

• For b a basis of E, then submodule.span ℤ (set.range b) is a ℤ-lattice of E.
• As an add_subgroup E with the additional properties: ∀ r : ℝ, (L ∩ metric.closed_ball 0 r).finite, that is L is discrete submodule.span ℝ (L : set E) = ⊤, that is L spans E over K.

## Main result #

• zspan.is_add_fundamental_domain: for a ℤ-lattice submodule.span ℤ (set.range b), proves that the set defined by zspan.fundamental_domain is a fundamental domain.
def zspan.fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) :
set E

The fundamental domain of the ℤ-lattice spanned by b. See zspan.is_add_fundamental_domain for the proof that it is the fundamental domain.

Equations
@[simp]
theorem zspan.mem_fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) {m : E} :
(i : ι), ((b.repr) m) i 1
noncomputable def zspan.floor {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (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
noncomputable def zspan.ceil {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (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
@[simp]
theorem zspan.repr_floor_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) (i : ι) :
((b.repr) m)) i = ((b.repr) m) i
@[simp]
theorem zspan.repr_ceil_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) (i : ι) :
((b.repr) 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} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) (h : m ) :
m) = m
@[simp]
theorem zspan.ceil_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) (h : m ) :
m) = m
noncomputable def zspan.fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) :
E

The map that sends a vector E to the fundamental domain of the lattice, see zspan.fract_mem_fundamental_domain.

Equations
theorem zspan.fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) :
m = m - m)
@[simp]
theorem zspan.repr_fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) (i : ι) :
((b.repr) m)) i = int.fract (((b.repr) m) i)
@[simp]
theorem zspan.fract_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) :
m) = m
@[simp]
theorem zspan.fract_zspan_add {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) {v : E} (h : v ) :
(v + m) = m
@[simp]
theorem zspan.fract_add_zspan {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) {v : E} (h : v ) :
(m + v) = m
theorem zspan.fract_eq_self {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] {b : K E} [floor_ring K] [fintype ι] {x : E} :
x = x
theorem zspan.fract_mem_fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (x : E) :
theorem zspan.fract_eq_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m n : E) :
m = n -m + n
theorem zspan.norm_fract_le {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (m : E) :
m finset.univ.sum (λ (i : ι), b i)
@[simp]
theorem zspan.coe_floor_self {ι : Type u_2} {K : Type u_3} [floor_ring K] [fintype ι] [unique ι] (k : K) :
@[simp]
theorem zspan.coe_fract_self {ι : Type u_2} {K : Type u_3} [floor_ring K] [fintype ι] [unique ι] (k : K) :
k =
theorem zspan.fundamental_domain_bounded {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [finite ι]  :
theorem zspan.vadd_mem_fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [fintype ι] (y : (set.range b))) (x : E) :
y = - x
theorem zspan.exist_unique_vadd_mem_fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [ E] (b : K E) [floor_ring K] [finite ι] (x : E) :
∃! (v : (set.range b))),
@[measurability]
theorem zspan.fundamental_domain_measurable_set {E : Type u_1} {ι : Type u_2} [ E] (b : E) [finite ι] :
@[protected]
theorem zspan.is_add_fundamental_domain {E : Type u_1} {ι : Type u_2} [ E] (b : E) [finite ι] (μ : measure_theory.measure E) :

For a ℤ-lattice submodule.span ℤ (set.range b), proves that the set defined by zspan.fundamental_domain is a fundamental domain.