ℤ-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 a
ℤ-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 and definitions #
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
ZLattice.comap
: fore : E → F
a linear map andL : Submodule ℤ E
, define the pullback ofL
bye
. IfL
is aIsZLattice
ande
is a continuous linear equiv, then it is also aIsZLattice
, seeinstIsZLatticeComap
.
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
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
Any ℤ
-basis of L
is also a K
-basis of E
.
Equations
- Basis.ofZLatticeBasis K L b = basisOfTopLeSpanOfCardEqFinrank (⇑L.subtype ∘ ⇑b) ⋯ ⋯
Instances For
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
Instances For
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 ⋯) ⋯
Instances For
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)