The Canonical Lattice ℤ^n in Euclidean Space

In this file, we explore the properties of the canonical lattice ℤⁿ in Euclidean space ℝⁿ. This allows us to talk about properties like the self-dual property, which only makes sense in settings where we have an inner-product (or some bilinear form) to work with.

Main Definition

1. Zn_Submodule_Euclidean : The canonical lattice ℤⁿ, viewed as a submodule of Euclidean space.
2. isZLattice_EucLattice : The canonical lattice ℤⁿ is indeed a lattice in Euclidean space.

Main Results

1. EuclideanSpace.mem_Zn_Submodule_iff : An element of Euclidean space lies in ℤⁿ iff it comes from a ℤ-valued vector.
2. Zn_dualSubmodule_eq_Zn : The lattice ℤⁿ is self-dual.

def «termEuc(_)» : Lean.ParserDescr

We denote by Euc(n) the Euclidean Space in n dimensions.

Equations

• One or more equations did not get rendered due to their size.

In this section, we develop the theory of ℤⁿ as a submodule of Euclidean space.

def Zn_Submodule_Euclidean (n : ℕ) : Submodule ℤ Euc(n)

The canonical lattice ℤ^n, viewed as a submodule of Euclidean space.

Equations

• EucLattice(n) = { carrier := {x : Euc(n) | x ∈ ℤ^n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem EuclideanSpace.mem_Zn_Submodule_iff (n : ℕ) (x : Euc(n)) : x ∈ EucLattice(n) ↔ ∃ (m : Fin n → ℤ), ∀ (i : Fin n), x i = ↑(m i)

An element of the Euclidean space lies in ℤ^n iff it comes from a ℤ-valued vector.

theorem EuclideanSpace.mem_Zn_Submodule_iff' (n : ℕ) (x : Euc(n)) : x ∈ EucLattice(n) ↔ ∀ (i : Fin n), ∃ (m : ℤ), x i = ↑m

An element of the Euclidean space lies in ℤ^n iff all its coordinates are integers.

def «termEucLattice(_)» : Lean.ParserDescr

We denote by EuclideanLattice(n) the canonical free ℤ-submodule of Euc(n).

Equations

• One or more equations did not get rendered due to their size.

In this section, we develop the theory of ℤⁿ as a lattice in Euclidean space.

instance instDiscreteTopology_EucLattice (n : ℕ) : DiscreteTopology ↥EucLattice(n)

instance isZLattice_EucLattice (n : ℕ) : IsZLattice ℝ EucLattice(n)

In this section, we prove a few results about the interaction of EucLattice(n) with the standard basis of Euc(n).

theorem PiLp_basisFun_mem_EucLattice (n : ℕ) (i : Fin n) : (PiLp.basisFun 2 ℝ (Fin n)) i ∈ ℤ^n

In this section, we show that the canonical lattice is self-dual.

theorem Zn_dualSubmodule_eq_Zn (n : ℕ) : ZLattice.Dual bilinFormOfRealInner EucLattice(n) = EucLattice(n)