ℤ-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

def Zspan.fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (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

• Zspan.fundamentalDomain b = {m | ∀ (i : ι), ↑(↑b.repr m) i ∈ Set.Ico 0 1}

@[simp]

theorem Zspan.mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {m : E} : m ∈ Zspan.fundamentalDomain b ↔ ∀ (i : ι), ↑(↑b.repr m) i ∈ Set.Ico 0 1

theorem Zspan.map_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) : ↑f '' Zspan.fundamentalDomain b = Zspan.fundamentalDomain (Basis.map b f)

@[simp]

theorem Zspan.fundamentalDomain_reindex {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {ι' : Type u_4} (e : ι ≃ ι') : Zspan.fundamentalDomain (Basis.reindex b e) = Zspan.fundamentalDomain b

theorem Zspan.fundamentalDomain_pi_basisFun {ι : Type u_2} [Fintype ι] : Zspan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.pi Set.univ fun x => Set.Ico 0 1

def Zspan.floor {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) : { x // x ∈ Submodule.span ℤ (Set.range ↑b) }

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

• Zspan.floor b m = Finset.sum Finset.univ fun i => ⌊↑(↑b.repr m) i⌋ • ↑(Basis.restrictScalars ℤ b) i

def Zspan.ceil {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) : { x // x ∈ Submodule.span ℤ (Set.range ↑b) }

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

• Zspan.ceil b m = Finset.sum Finset.univ fun i => ⌈↑(↑b.repr m) i⌉ • ↑(Basis.restrictScalars ℤ b) i

@[simp]

theorem Zspan.repr_floor_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (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} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (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} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) (h : m ∈ Submodule.span ℤ (Set.range ↑b)) : ↑(Zspan.floor b m) = m

@[simp]

theorem Zspan.ceil_eq_self_of_mem {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) (h : m ∈ Submodule.span ℤ (Set.range ↑b)) : ↑(Zspan.ceil b m) = m

def Zspan.fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (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

• Zspan.fract b m = m - ↑(Zspan.floor b m)

theorem Zspan.fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) : Zspan.fract b m = m - ↑(Zspan.floor b m)

@[simp]

theorem Zspan.repr_fract_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing 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} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) : Zspan.fract b (Zspan.fract b m) = Zspan.fract b m

@[simp]

theorem Zspan.fract_zspan_add {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) {v : E} (h : v ∈ Submodule.span ℤ (Set.range ↑b)) : Zspan.fract b (v + m) = Zspan.fract b m

@[simp]

theorem Zspan.fract_add_zspan {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) {v : E} (h : v ∈ Submodule.span ℤ (Set.range ↑b)) : Zspan.fract b (m + v) = Zspan.fract b m

theorem Zspan.fract_eq_self {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] {b : Basis ι K E} [FloorRing K] [Fintype ι] {x : E} : Zspan.fract b x = x ↔ x ∈ Zspan.fundamentalDomain b

theorem Zspan.fract_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : E) : Zspan.fract b x ∈ Zspan.fundamentalDomain b

def Zspan.fractRestrict {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : E) : ↑(Zspan.fundamentalDomain b)

The map fract with codomain restricted to fundamentalDomain.

Equations

• Zspan.fractRestrict b x = { val := Zspan.fract b x, property := (_ : Zspan.fract b x ∈ Zspan.fundamentalDomain b) }

theorem Zspan.fractRestrict_surjective {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] : Function.Surjective (Zspan.fractRestrict b)

@[simp]

theorem Zspan.fractRestrict_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : E) : ↑(Zspan.fractRestrict b x) = Zspan.fract b x

theorem Zspan.fract_eq_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (m : E) (n : E) : Zspan.fract b m = Zspan.fract b n ↔ -m + n ∈ Submodule.span ℤ (Set.range ↑b)

theorem Zspan.norm_fract_le {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] [HasSolidNorm K] (m : E) : ‖Zspan.fract b m‖ ≤ Finset.sum Finset.univ fun i => ‖↑b i‖

@[simp]

theorem Zspan.coe_floor_self {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [FloorRing K] [Fintype ι] [Unique ι] (k : K) : ↑(Zspan.floor (Basis.singleton ι K) k) = ↑⌊k⌋

@[simp]

theorem Zspan.coe_fract_self {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [FloorRing K] [Fintype ι] [Unique ι] (k : K) : Zspan.fract (Basis.singleton ι K) k = Int.fract k

theorem Zspan.fundamentalDomain_isBounded {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Finite ι] [HasSolidNorm K] : Bornology.IsBounded (Zspan.fundamentalDomain b)

theorem Zspan.vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (y : { x // x ∈ Submodule.span ℤ (Set.range ↑b) }) (x : E) : y +ᵥ x ∈ Zspan.fundamentalDomain b ↔ y = -Zspan.floor b x

theorem Zspan.exist_unique_vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Finite ι] (x : E) : ∃! v, v +ᵥ x ∈ Zspan.fundamentalDomain b

def Zspan.quotientEquiv {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] : E ⧸ Submodule.span ℤ (Set.range ↑b) ≃ ↑(Zspan.fundamentalDomain b)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Zspan.quotientEquiv_apply_mk {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : E) : ↑(Zspan.quotientEquiv b) (Submodule.Quotient.mk x) = Zspan.fractRestrict b x

@[simp]

theorem Zspan.quotientEquiv.symm_apply {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : ↑(Zspan.fundamentalDomain b)) : ↑(Zspan.quotientEquiv b).symm x = Submodule.Quotient.mk ↑x

theorem Zspan.fundamentalDomain_measurableSet {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] : MeasurableSet (Zspan.fundamentalDomain b)

theorem Zspan.isAddFundamentalDomain {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain { x // x ∈ Submodule.toAddSubgroup (Submodule.span ℤ (Set.range ↑b)) } (Zspan.fundamentalDomain b)

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

theorem Zspan.measure_fundamentalDomain {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [MeasureTheory.Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) : ↑↑μ (Zspan.fundamentalDomain b) = ENNReal.ofReal |Matrix.det (Basis.toMatrix b₀ ↑b)| * ↑↑μ (Zspan.fundamentalDomain b₀)

@[simp]

theorem Zspan.volume_fundamentalDomain {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) : ↑↑MeasureTheory.volume (Zspan.fundamentalDomain b) = ENNReal.ofReal |Matrix.det (↑Matrix.of ↑b)|

theorem Zlattice.FG (K : Type u_1) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {L : AddSubgroup E} [DiscreteTopology { x // x ∈ L }] (hs : Submodule.span K ↑L = ⊤) : AddSubgroup.FG L

theorem Zlattice.module_finite (K : Type u_1) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {L : AddSubgroup E} [DiscreteTopology { x // x ∈ L }] (hs : Submodule.span K ↑L = ⊤) : Module.Finite ℤ { x // x ∈ L }

theorem Zlattice.module_free (K : Type u_1) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {L : AddSubgroup E} [DiscreteTopology { x // x ∈ L }] (hs : Submodule.span K ↑L = ⊤) : Module.Free ℤ { x // x ∈ L }

theorem Zlattice.rank (K : Type u_1) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {L : AddSubgroup E} [DiscreteTopology { x // x ∈ L }] (hs : Submodule.span K ↑L = ⊤) : FiniteDimensional.finrank ℤ { x // x ∈ L } = FiniteDimensional.finrank K E