The Canonical Lattice ℤ^n

In this file, we develop some theory about the canonical free ℤ-submodule of rank n, denoted ℤ^n, of the Pi space ℝ^n. In particular, we devlop some theory about ℤ^n as a lattice, with the long-term goal of proving the Poisson Summation Formula for Schwartz functions over ℤ^n.

Main Definition

1. Zn_Submodule : The canonical free ℤ-submodule of ℝ^n.
2. isZLattice_Zn : ℤ^n is a lattice.

Main Results

1. Zn_eq_ZSpan_Pi_basisFun : ℤ^n is the ℤ-span of the canonical ℝ-basis of ℝ^n.
2. Zn_covolume : The covolume of ℤ^n is 1.

We begin by defining some useful notation.

def «termℝ^_» : Lean.ParserDescr

We denote by ℝ^n the Pi type Fin n → ℝ.

Equations

• «termℝ^_» = Lean.ParserDescr.node `«termℝ^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℝ^") (Lean.ParserDescr.cat `term 1023))

We now develop the theory of ℤ^n as a submodule of Euclidean space.

def Zn_Submodule (n : ℕ) : Submodule ℤ (Fin n → ℝ)

We can define a submodule of ℝ^n whose elements are precisely those of ℤ^n that are coerced into ℝ^n.

Equations

• ℤ^n = { carrier := {x : Fin n → ℝ | ∃ (m : Fin n → ℤ), ∀ (i : Fin n), x i = ↑(m i)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def «termℤ^_» : Lean.ParserDescr

We denote by ℤ^n the canonical free ℤ-submodule living inside Fin n → ℝ.

Equations

• «termℤ^_» = Lean.ParserDescr.node `«termℤ^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℤ^") (Lean.ParserDescr.cat `term 1023))

In this section, we will use the standard basis for the Pi type ℝ^n to construct a basis for the submodule ℤ^n. We will then be able to use this basis to show that ℤ^n has covolume 1.

theorem Pi_basisFun_mem_Zn (n : ℕ) (i : Fin n) : (Pi.basisFun ℝ (Fin n)) i ∈ ℤ^n

The canonical basis of ℝ^n embeds into ℤ^n.

def Pi_basisFun_Zn (n : ℕ) : Fin n → ↥(ℤ^n)

The canonical basis of ℤ^n, defined as a family of vectors.

Equations

• Pi_basisFun_Zn n i = ⟨(Pi.basisFun ℝ (Fin n)) i, ⋯⟩

theorem Pi_basisFun_Z_linear_independent (n : ℕ) : LinearIndependent ℤ ⇑(Pi.basisFun ℝ (Fin n))

The canonical basis of ℝ^n is ℤ-linearly independent.

theorem Pi_basisFun_Zn_Z_linear_independent (n : ℕ) : LinearIndependent ℤ (Pi_basisFun_Zn n)

The canonical basis of ℤ^n is ℤ-linearly independent.

theorem Zn_eq_ZSpan_Pi_basisFun {n : ℕ} : ℤ^n = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ (Fin n)))

ℤ^n is the ℤ-span of the canonical ℝ-basis of ℝ^n.

theorem Pi_basisFun_Zn_Zspan (n : ℕ) : ⊤ ≤ Submodule.span ℤ (Set.range (Pi_basisFun_Zn n))

The canonical basis of ℤ^n spans ℤ^n.

def Pi_BasisFun_Z_basis (n : ℕ) : Basis (Fin n) ℤ ↥(ℤ^n)

The canonical basis of ℤ^n.

Equations

• Pi_BasisFun_Z_basis n = Basis.mk ⋯ ⋯

theorem Pi_BasisFun_basis.toMatrix (n : ℕ) : Matrix.of ⇑(Pi.basisFun ℝ (Fin n)) = 1

The canonical basis of ℝ^n has matrix equal to the identity matrix.

theorem Pi_BasisFun_Z_basis.toMatrix (n : ℕ) : Matrix.of (Subtype.val ∘ ⇑(Pi_BasisFun_Z_basis n)) = 1

The canonical basis of ℤ^n has matrix equal to the identity matrix.

theorem Pi_BasisFun_fundamentalDomain (n : ℕ) : MeasureTheory.volume (ZSpan.fundamentalDomain (Pi.basisFun ℝ (Fin n))) = 1

The fundamental domain of the canonical basis of ℝ^n has volume 1.

instance instDiscreteTopology_Zn (n : ℕ) : DiscreteTopology ↥(ℤ^n)

ℤ^n has the discrete topology.

instance isZLattice_Zn (n : ℕ) : IsZLattice ℝ (ℤ^n)

ℤ^n is a lattice.

In this section, we will explore the freeness of ℤ^n as a module over ℤ.

theorem Zn_free (n : ℕ) : Module.Free ℤ ↥(ℤ^n)

ℤ^n is a free ℤ-module.

theorem Zn_finrank (n : ℕ) : Module.finrank ℤ ↥(ℤ^n) = n

The finrank of the free ℤ-module ℤ^n is n.

theorem Zn_rank (n : ℕ) : Module.rank ℤ ↥(ℤ^n) = ↑n

The rank of the free ℤ-module ℤ^n is n.

In this section, we show that the covolume of the canonical lattice in Fin n → ℝ is 1.

theorem Zn_covolume (n : ℕ) : ZLattice.covolume (ℤ^n) MeasureTheory.volume = 1

The lattice ℤ^n has covolume 1.