Documentation

Mathlib.Algebra.Module.ZLattice.Basic

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

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 #

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) :
theorem ZSpan.smul {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField 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} [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
Instances For
    @[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) :
    @[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 : ι ι') :
    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) :

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

      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
      Instances For
        @[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
        Instances For
          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) :
          @[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)) :
          @[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)) :
          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} :
          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) :

          The map fract with codomain restricted to fundamentalDomain.

          Equations
          Instances For
            @[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) :
            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 n : E) :
            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) :
            @[simp]
            theorem ZSpan.coe_fract_self {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [FloorRing K] [Fintype ι] [Unique ι] (k : K) :
            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) :

            The map ZSpan.fractRestrict defines an equiv map between E ⧸ span ℤ (Set.range b) and ZSpan.fundamentalDomain b.

            Equations
            Instances For
              @[simp]
              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

              For a ℤ-lattice Submodule.span ℤ (Set.range b), proves that the set defined by ZSpan.fundamentalDomain is a fundamental domain.

              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] :
              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) :
              @[simp]
              theorem ZSpan.volume_fundamentalDomain {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι (ι)) :
              MeasureTheory.volume (ZSpan.fundamentalDomain b) = ENNReal.ofReal |(Matrix.of b).det|
              class IsZLattice (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : Submodule E) [DiscreteTopology L] :

              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.

              Instances
                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 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
                Instances For
                  @[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 L] {ι : Type u_3} [hs : IsZLattice K L] (b : Basis ι 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 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)
                  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) :

                  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
                  Instances For
                    @[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) :
                    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) :
                    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)) :
                    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
                    Instances For
                      @[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) :
                      ((ZLattice.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
                      Instances For
                        @[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 : ι) :
                        ((Basis.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 : ι) :
                        ((Basis.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) [NormedLinearOrderedField 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) :
                        Basis.ofZLatticeBasis K (ZLattice.comap K L e.toLinearEquiv) (Basis.ofZLatticeComap K L e.toLinearEquiv b) = (Basis.ofZLatticeBasis K L b).map e.symm.toLinearEquiv