ℤ-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 a ℤ-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 and definitions

• 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
• ZLattice.comap: for e : E → F a linear map and L : Submodule ℤ E, define the pullback of L by e. If L is a IsZLattice and e is a continuous linear equiv, then it is also a IsZLattice, see instIsZLatticeComap.

Note

There is also Submodule.IsLattice which has slightly different applications. There no topology is needed and the discrete condition is replaced by finitely generated.

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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) : Submodule.span K ↑(Submodule.span ℤ (Set.range ⇑b)) = ⊤

theorem ZSpan.map {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {F : Type u_4} [AddCommGroup F] [Module K F] (f : E ≃ₗ[K] F) : Submodule.map (LinearEquiv.restrictScalars ℤ f) (Submodule.span ℤ (Set.range ⇑b)) = Submodule.span ℤ (Set.range ⇑(b.map f))

theorem ZSpan.smul {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {c : K} (hc : c ≠ 0) : c • Submodule.span ℤ (Set.range ⇑b) = Submodule.span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

def ZSpan.fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] : 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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] {m : E} : m ∈ 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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) : ⇑f '' fundamentalDomain b = fundamentalDomain (b.map f)

@[simp]

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

theorem ZSpan.fundamentalDomain_pi_basisFun {ι : Type u_2} [Fintype ι] : 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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [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 = ∑ i : ι, ⌊(b.repr m) i⌋ • (Basis.restrictScalars ℤ b) i

def ZSpan.ceil {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [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 = ∑ 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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (i : ι) : (b.repr ↑(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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (i : ι) : (b.repr ↑(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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (h : m ∈ Submodule.span ℤ (Set.range ⇑b)) : ↑(floor b m) = m

@[simp]

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

def ZSpan.fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) : fract b m = m - ↑(floor b m)

@[simp]

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

@[simp]

theorem ZSpan.fract_zSpan_add {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) {v : E} (h : v ∈ Submodule.span ℤ (Set.range ⇑b)) : fract b (v + m) = fract b m

@[simp]

theorem ZSpan.fract_add_ZSpan {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) {v : E} (h : v ∈ Submodule.span ℤ (Set.range ⇑b)) : fract b (m + v) = fract b m

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

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

def ZSpan.fractRestrict {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (x : E) : ↑(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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] : Function.Surjective (fractRestrict b)

@[simp]

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

theorem ZSpan.fract_eq_fract {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m n : E) : fract b m = 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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] [HasSolidNorm K] (m : E) : ‖fract b m‖ ≤ ∑ i : ι, ‖b i‖

@[simp]

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

@[simp]

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

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

theorem ZSpan.vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (y : ↥(Submodule.span ℤ (Set.range ⇑b))) (x : E) : y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

theorem ZSpan.exist_unique_vadd_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Finite ι] (x : E) : ∃! v : ↥(Submodule.span ℤ (Set.range ⇑b)), v +ᵥ x ∈ fundamentalDomain b

def ZSpan.quotientEquiv {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] : E ⧸ Submodule.span ℤ (Set.range ⇑b) ≃ ↑(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} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (x : E) : (quotientEquiv b) (Submodule.Quotient.mk x) = fractRestrict b x

@[simp]

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

theorem ZSpan.discreteTopology_pi_basisFun {ι : Type u_2} [Finite ι] : DiscreteTopology ↥(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 ι] : fundamentalDomain b ⊆ parallelepiped ⇑b

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

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

theorem ZSpan.setFinite_inter {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.IsBounded s) : (s ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite

theorem ZSpan.fundamentalDomain_measurableSet {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] : MeasurableSet (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 (↥(Submodule.span ℤ (Set.range ⇑b))) (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 (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup) (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] : μ (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) : μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (fundamentalDomain b₀)

theorem ZSpan.measureReal_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) : μ.real (fundamentalDomain b) = |b₀.det ⇑b| * μ.real (fundamentalDomain b₀)

@[simp]

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

@[simp]

theorem ZSpan.volume_real_fundamentalDomain {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) : MeasureTheory.volume.real (fundamentalDomain b) = |(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] : 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 ↥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.

instance instIsZLatticeRealSpan {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] (b : Basis ι ℝ E) : IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑b))

@[deprecated instIsZLatticeRealSpan (since := "2025-05-08")]

theorem ZSpan.isZLattice {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] (b : Basis ι ℝ E) : IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑b))

Alias of instIsZLatticeRealSpan.

theorem Zlattice.FG (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [hs : IsZLattice K L] : L.FG

theorem ZLattice.module_finite (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] : Module.Finite ℤ ↥L

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

theorem ZLattice.module_free (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] : Module.Free ℤ ↥L

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

theorem ZLattice.rank (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [hs : IsZLattice K L] : Module.finrank ℤ ↥L = Module.finrank K E

def Basis.ofZLatticeBasis (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ 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

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

@[simp]

theorem Basis.ofZLatticeBasis_apply (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ ↥L) (i : ι) : (ofZLatticeBasis K L b) i = ↑(b i)

@[simp]

theorem Basis.ofZLatticeBasis_repr_apply (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ((ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)

theorem Basis.ofZLatticeBasis_span (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι ℤ ↥L) : Submodule.span ℤ (Set.range ⇑(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 ↥L] [IsZLattice ℝ L] [Finite ι] (b : Basis ι ℤ ↥L) [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain (↥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 ↥L] [IsZLattice ℝ L] : Countable ↥L

theorem Real.finrank_eq_int_finrank_of_discrete {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : DiscreteTopology ↥(Submodule.span ℤ s)) : Set.finrank ℝ s = Set.finrank ℤ s

Assume that the set s spans over ℤ a discrete set. Then its ℝ-rank is equal to its ℤ-rank.

def ZLattice.comap (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F →ₗ[K] E) : Submodule ℤ F

Let e : E → F a linear map, the map that sends a L : Submodule ℤ E to the Submodule ℤ F that is the pullback of L by e. If IsZLattice L and e is a continuous linear equiv, then it is a IsZLattice of E, see instIsZLatticeComap.

Equations

• ZLattice.comap K L e = Submodule.comap (↑ℤ e) L

@[simp]

theorem ZLattice.coe_comap (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F →ₗ[K] E) : ↑(ZLattice.comap K L e) = ⇑e ⁻¹' ↑L

theorem ZLattice.comap_refl (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : Submodule ℤ E) : ZLattice.comap K L 1 = L

theorem ZLattice.comap_discreteTopology (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) [hL : DiscreteTopology ↥L] {e : F →ₗ[K] E} (he₁ : Continuous ⇑e) (he₂ : Function.Injective ⇑e) : DiscreteTopology ↥(ZLattice.comap K L e)

instance instDiscreteTopologySubtypeMemSubmoduleIntComap (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (e : F ≃L[K] E) : DiscreteTopology ↥(ZLattice.comap K L ↑e.toLinearEquiv)

theorem ZLattice.comap_span_top (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (hL : Submodule.span K ↑L = ⊤) {e : F →ₗ[K] E} (he : ↑L ⊆ ↑(LinearMap.range e)) : Submodule.span K ↑(ZLattice.comap K L e) = ⊤

instance instIsZLatticeComap (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] (e : F ≃L[K] E) : IsZLattice K (ZLattice.comap K L ↑e.toLinearEquiv)

theorem ZLattice.comap_comp (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace K G] (e : F →ₗ[K] E) (e' : G →ₗ[K] F) : ZLattice.comap K (ZLattice.comap K L e) e' = ZLattice.comap K L (e ∘ₗ e')

def ZLattice.comap_equiv (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) : ↥L ≃ₗ[ℤ] ↥(ZLattice.comap K L ↑e)

If e is a linear equivalence, it induces a ℤ-linear equivalence between L and ZLattice.comap K L e.

Equations

• ZLattice.comap_equiv K L e = LinearEquiv.ofBijective ((↑ℤ ↑e.symm).restrict ⋯) ⋯

@[simp]

theorem ZLattice.comap_equiv_apply (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) (x : ↥L) : ↑((comap_equiv K L e) x) = e.symm ↑x

def Basis.ofZLatticeComap (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) : Basis ι ℤ ↥(ZLattice.comap K L ↑e)

The basis of ZLattice.comap K L e given by the image of a basis b of L by e.symm.

Equations

• Basis.ofZLatticeComap K L e b = b.map (ZLattice.comap_equiv K L e)

@[simp]

theorem Basis.ofZLatticeComap_apply (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) (i : ι) : ↑((ofZLatticeComap K L e b) i) = e.symm ↑(b i)

@[simp]

theorem Basis.ofZLatticeComap_repr_apply (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ((ofZLatticeComap K L e b).repr ((ZLattice.comap_equiv K L e) x)) i = (b.repr x) i

theorem Basis.ofZLatticeBasis_comap (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace K F] [FiniteDimensional K F] [ProperSpace F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] (e : F ≃L[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) : ofZLatticeBasis K (ZLattice.comap K L ↑e.toLinearEquiv) (ofZLatticeComap K L e.toLinearEquiv b) = (ofZLatticeBasis K L b).map e.symm.toLinearEquiv