ℤ-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 ofE
, thenL = Submodule.span ℤ (Set.range b)
is a ℤ-lattice ofE
- As an
ℤ-submodule
ofE
with the additional properties:DiscreteTopology L
, that isL
is discreteSubmodule.span ℝ (L : Set E) = ⊤
, that isL
spansE
overK
.
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 ℤ-latticeSubmodule.span ℤ (Set.range b)
, proves that the set defined byZSpan.fundamentalDomain
is a fundamental domain.ZLattice.module_free
: aℤ
-submodule ofE
that is discrete and spansE
overK
is a freeℤ
-moduleZLattice.rank
: aℤ
-submodule ofE
that is discrete and spansE
overK
is free ofℤ
-rank equal to theK
-rank ofE
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.
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
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
Instances For
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
Instances For
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
The map fract
with codomain restricted to fundamentalDomain
.
Equations
- ZSpan.fractRestrict b x = ⟨ZSpan.fract b x, ⋯⟩
Instances For
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
For a ℤ-lattice Submodule.span ℤ (Set.range b)
, proves that the set defined
by ZSpan.fundamentalDomain
is a fundamental domain.
A version of ZSpan.isAddFundamentalDomain
for AddSubgroup
.
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 spaceE
overK
.
Instances
L
spans the full space E
over K
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any ℤ
-basis of L
is also a K
-basis of E
.
Equations
- Basis.ofZLatticeBasis K L b = basisOfTopLeSpanOfCardEqFinrank (⇑L.subtype ∘ ⇑b) ⋯ ⋯
Instances For
Equations
- ⋯ = ⋯