ℤ-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ℤ-submodule of 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: a ℤ-submodule of E that is discrete and spans E over K is a free ℤ-module
• ZLattice.rank: a ℤ-submodule of E that is discrete and spans E over K is free of ℤ-rank equal to the K-rank of E

Implementation Notes

A ZLattice could be defined either as a AddSubgroup E or a Submodule ℤ E. However, the module aspect appears to be the more useful one (especially in computations involving basis) and is also consistent with the ZSpan construction of ℤ-lattices.

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)) = ⊤

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}

@[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 (b.map 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 (b.reindex e) = ZSpan.fundamentalDomain b

theorem ZSpan.fundamentalDomain_pi_basisFun {ι : Type u_2} [Fintype ι] : ZSpan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi 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 : E // 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 = ∑ 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 : E // 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 = ∑ 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 = ⟨ZSpan.fract b x, ⋯⟩

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‖ ≤ ∑ 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 : E // 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 : { x : E // x ∈ Submodule.span ℤ (Set.range ⇑b) }, 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

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

@[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.discreteTopology_pi_basisFun {ι : Type u_2} [Finite ι] : DiscreteTopology { x : ι → ℝ // x ∈ Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) }

theorem ZSpan.fundamentalDomain_subset_parallelepiped {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] : ZSpan.fundamentalDomain b ⊆ parallelepiped ⇑b

instance ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] : DiscreteTopology { x : E // x ∈ Submodule.span ℤ (Set.range ⇑b) }

Equations

• ⋯ = ⋯

instance ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] : DiscreteTopology { x : E // x ∈ (Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup }

Equations

• ⋯ = ⋯

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 : E // x ∈ 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.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 : E // x ∈ (Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup } (ZSpan.fundamentalDomain b) μ

A version of ZSpan.isAddFundamentalDomain for AddSubgroup.

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} [μ.IsAddHaarMeasure] : μ (ZSpan.fundamentalDomain b) ≠ 0

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] [μ.IsAddHaarMeasure] (b₀ : Basis ι ℝ E) : μ (ZSpan.fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (ZSpan.fundamentalDomain b₀)

@[simp]

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

theorem ZSpan.fundamentalDomain_ae_parallelepiped {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [μ.IsAddHaarMeasure] : ZSpan.fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b

class IsZLattice (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] : Prop

L : Submodule ℤ 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.

theorem IsZLattice.span_top {K : Type u_1} [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] {L : Submodule ℤ E} [DiscreteTopology { x : E // x ∈ L }] [self : IsZLattice K L] : Submodule.span K ↑L = ⊤

L spans the full space E over K.

theorem ZSpan.isZLattice {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] (b : Basis ι ℝ E) : IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] [hs : IsZLattice K L] : L.FG

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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] [IsZLattice K L] : Module.Finite ℤ { x : E // x ∈ L }

instance instModuleFinite_of_discrete_submodule {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] : Module.Finite ℤ { x : E // x ∈ L }

Equations

• ⋯ = ⋯

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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] [IsZLattice K L] : Module.Free ℤ { x : E // x ∈ L }

instance instModuleFree_of_discrete_submodule {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] : Module.Free ℤ { x : E // x ∈ L }

Equations

• ⋯ = ⋯

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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] [hs : IsZLattice K L] : FiniteDimensional.finrank ℤ { x : E // x ∈ L } = FiniteDimensional.finrank K E

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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ { x : E // x ∈ L }) : Basis ι K E

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

Equations

• Basis.ofZLatticeBasis K L b = basisOfTopLeSpanOfCardEqFinrank (⇑L.subtype ∘ ⇑b) ⋯ ⋯

@[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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ { x : E // x ∈ L }) (i : ι) : (Basis.ofZLatticeBasis K L b) i = ↑(b i)

@[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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ { x : E // x ∈ L }) (x : { x : E // x ∈ L }) (i : ι) : ((Basis.ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

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 : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ { x : E // x ∈ L }) : Submodule.span ℤ (Set.range ⇑(Basis.ofZLatticeBasis K L b)) = L

theorem ZLattice.isAddFundamentalDomain {ι : Type u_3} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology { x : E // x ∈ L }] [IsZLattice ℝ L] [Finite ι] (b : Basis ι ℤ { x : E // x ∈ L }) [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain { x : E // x ∈ L } (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ

instance instCountable_of_discrete_submodule {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology { x : E // x ∈ L }] [IsZLattice ℝ L] : Countable { x : E // x ∈ L }

Equations

• ⋯ = ⋯