mathlib3 documentation

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:

Main result #

def zspan.fundamental_domain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι 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} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) {m : E} :
noncomputable def zspan.floor {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι 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} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι 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} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) (i : ι) :
@[simp]
theorem zspan.repr_ceil_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) (i : ι) :
@[simp]
theorem zspan.floor_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) (h : m submodule.span (set.range b)) :
@[simp]
theorem zspan.ceil_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) (h : m submodule.span (set.range b)) :
noncomputable def zspan.fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι 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} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) :
@[simp]
theorem zspan.repr_fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (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} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) :
@[simp]
theorem zspan.fract_zspan_add {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) {v : E} (h : v submodule.span (set.range b)) :
@[simp]
theorem zspan.fract_add_zspan {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m : E) {v : E} (h : v submodule.span (set.range b)) :
theorem zspan.fract_eq_self {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] {b : basis ι K E} [floor_ring K] [fintype ι] {x : E} :
theorem zspan.fract_eq_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] (m n : E) :
theorem zspan.norm_fract_le {E : Type u_1} {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [normed_add_comm_group E] [normed_space K E] (b : basis ι K E) [floor_ring K] [fintype ι] [has_solid_norm K] (m : E) :
@[simp]
theorem zspan.coe_floor_self {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [floor_ring K] [fintype ι] [unique ι] (k : K) :
@[simp]
theorem zspan.coe_fract_self {ι : Type u_2} {K : Type u_3} [normed_linear_ordered_field K] [floor_ring K] [fintype ι] [unique ι] (k : K) :