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

source

theorem Zspan.span_top {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) :

Submodule.span K ↑(Submodule.span ℤ (Set.range ⇑b)) = ⊤

source

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 : E | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1}

Instances For

source

@[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

source

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)

source

@[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

source

theorem Zspan.fundamentalDomain_pi_basisFun {ι : Type u_2} [Fintype ι] :

Zspan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.pi Set.univ fun (x : ι) => Set.Ico 0 1

source

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) :

↥(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

Instances For

source

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) :

↥(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

Instances For

source

@[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⌋

source

@[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⌉

source

@[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

source

@[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

source

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) :

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)

Instances For

source

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)

source

@[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)

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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 := ⋯ }

Instances For

source

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)

source

@[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

source

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)

source

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‖

source

@[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⌋

source

@[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

source

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)

source

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 : ↥(Submodule.span ℤ (Set.range ⇑b))) (x : E) :

y +ᵥ x ∈ Zspan.fundamentalDomain b ↔ y = -Zspan.floor b x

source

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 : ↥(Submodule.span ℤ (Set.range ⇑b))), v +ᵥ x ∈ Zspan.fundamentalDomain b

source

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

Zspan.quotientEquiv b = Equiv.ofBijective (fun (q : E ⧸ Submodule.span ℤ (Set.range ⇑b)) => Quotient.liftOn q (Zspan.fractRestrict b) ⋯) ⋯

Instances For

source

@[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

source

@[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

source

theorem Zspan.discreteTopology_pi_basisFun {ι : Type u_2} [Finite ι] :

DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

source

instance Zspan.instDiscreteTopologySubtypeMemSubmoduleIntInstSemiringIntToAddCommMonoidToAddCommGroupIntModuleInstMembershipSetLikeSpanRangeCoeBasisRealSemiringToModuleNormedFieldToSeminormedAddCommGroupInstFunLikeInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpace {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] :

DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑b))

Equations

⋯ = ⋯

source

instance Zspan.instDiscreteTopologySubtypeMemAddSubgroupToAddGroupToAddCommGroupInstMembershipInstSetLikeAddSubgroupToAddSubgroupIntInstRingIntIntModuleSpanInstSemiringIntToAddCommMonoidRangeCoeBasisRealSemiringToModuleNormedFieldToSeminormedAddCommGroupInstFunLikeInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpace {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] :

DiscreteTopology ↥(Submodule.toAddSubgroup (Submodule.span ℤ (Set.range ⇑b)))

Equations

⋯ = ⋯

source

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)

source

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 (↥(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.

source

theorem Zspan.measure_fundamentalDomain_ne_zero {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.Measure.IsAddHaarMeasure μ] :

↑↑μ (Zspan.fundamentalDomain b) ≠ 0

source

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 |(Basis.det b₀) ⇑b| * ↑↑μ (Zspan.fundamentalDomain b₀)

source

@[simp]

theorem Zspan.volume_fundamentalDomain {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) :

↑↑MeasureTheory.volume (Zspan.fundamentalDomain b) = ENNReal.ofReal |Matrix.det (Matrix.of ⇑b)|

source

class IsZlattice (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : AddSubgroup E) [DiscreteTopology ↥L] :

Prop

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 : Submodule.span K ↑L = ⊤
L spans the full space E over K.

Instances

source

theorem Zspan.isZlattice {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] (b : Basis ι ℝ E) :

IsZlattice ℝ (Submodule.toAddSubgroup (Submodule.span ℤ (Set.range ⇑b)))

source

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 ↥L] [hs : IsZlattice K L] :

AddSubgroup.FG L

source

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 ↥L] [IsZlattice K L] :

Module.Finite ℤ ↥L

source

instance instModuleFinite_of_discrete_addSubgroup {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : AddSubgroup E) [DiscreteTopology ↥L] :

Module.Finite ℤ ↥L

Equations

⋯ = ⋯

source

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 ↥L] [IsZlattice K L] :

Module.Free ℤ ↥L

source

instance instModuleFree__of_discrete_addSubgroup {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : AddSubgroup E) [DiscreteTopology ↥L] :

Module.Free ℤ ↥L

Equations

⋯ = ⋯

source

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 ↥L] [hs : IsZlattice K L] :

FiniteDimensional.finrank ℤ ↥L = FiniteDimensional.finrank K E

source

def Basis.ofZlatticeBasis (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 ↥L] {ι : Type u_3} [hs : IsZlattice K L] (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

source

@[simp]

theorem Basis.ofZlatticeBasis_apply (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 ↥L] {ι : Type u_3} [hs : IsZlattice K L] (b : Basis ι ℤ ↥L) (i : ι) :

(Basis.ofZlatticeBasis K L b) i = ↑(b i)

source

@[simp]

theorem Basis.ofZlatticeBasis_repr_apply (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 ↥L] {ι : Type u_3} [hs : IsZlattice K L] (b : Basis ι ℤ ↥L) (x : ↥L) (i : ι) :

((Basis.ofZlatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

source

theorem Basis.ofZlatticeBasis_span (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 ↥L] {ι : Type u_3} [hs : IsZlattice K L] (b : Basis ι ℤ ↥L) :

Submodule.toAddSubgroup (Submodule.span ℤ (Set.range ⇑(Basis.ofZlatticeBasis K L b))) = L

Documentation

Mathlib.Algebra.Module.Zlattice

ℤ-lattices #

Main results #