The integral lattice in a rational coordinate space

For a finite index type ι, this file packages the standard integral lattice in ι → ℚ: the ℤ-span of the coordinate vectors. It records its coordinatewise membership criterion and its canonical basis. These declarations are shared by the standard Chevalley carriers and the Geck module instead of rebuilding the same restricted-scalars basis in each construction.

Main declarations

• TauCeti.coordinateLattice: the ℤ-span of the standard basis of ι → ℚ.
• TauCeti.mem_coordinateLattice_iff: membership means that every coordinate is integral.
• TauCeti.basisFun_mem_coordinateLattice and TauCeti.coordinateLatticeBasis: the standard coordinate vectors and basis over ℤ.
• TauCeti.apply_coordinateLatticeBasis_eq_sum_of_forall_apply_eq_mulVec: an endomorphism represented by an integer matrix has that matrix in the coordinate-lattice basis.

This is a reusable prerequisite for the Chevalley--Demazure carriers in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

def TauCeti.coordinateLattice (ι : Type u) [Finite ι] : Submodule ℤ (ι → ℚ)

The standard integral lattice in the rational coordinate space ι → ℚ.

Equations

• TauCeti.coordinateLattice ι = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℚ ι))

@[simp]

theorem TauCeti.mem_coordinateLattice_iff (ι : Type u) [Finite ι] {v : ι → ℚ} : v ∈ coordinateLattice ι ↔ ∀ (i : ι), ∃ (z : ℤ), ↑z = v i

A rational coordinate vector lies in the standard lattice exactly when every coordinate is an integer.

theorem TauCeti.basisFun_mem_coordinateLattice (ι : Type u) [Finite ι] (i : ι) : (Pi.basisFun ℚ ι) i ∈ coordinateLattice ι

Every standard coordinate basis vector lies in the coordinate lattice.

theorem TauCeti.ringChoose_end_apply_mem_coordinateLattice_of_apply_eq_intCast_smul (ι : Type u) [Finite ι] {f : Module.End ℚ (ι → ℚ)} {weight : ι → ℤ} (heigen : ∀ (i : ι), f ((Pi.basisFun ℚ ι) i) = ↑(weight i) • (Pi.basisFun ℚ ι) i) (n : ℕ) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (Ring.choose f n) v ∈ coordinateLattice ι

Binomial coefficients of an endomorphism preserve the coordinate lattice when every standard coordinate vector is an eigenvector with an integer eigenvalue.

noncomputable def TauCeti.coordinateLatticeBasis (ι : Type u) [Finite ι] : Module.Basis ι ℤ ↥(coordinateLattice ι)

The standard coordinate vectors, regarded as a basis of the coordinate lattice over ℤ.

Equations

• TauCeti.coordinateLatticeBasis ι = Module.Basis.restrictScalars ℤ (Pi.basisFun ℚ ι)

@[simp]

theorem TauCeti.coe_coordinateLatticeBasis (ι : Type u) [Finite ι] (i : ι) : ↑((coordinateLatticeBasis ι) i) = (Pi.basisFun ℚ ι) i

A coordinate-lattice basis vector is the corresponding standard coordinate vector.

theorem TauCeti.apply_coordinateLatticeBasis_eq_sum_of_forall_apply_eq_mulVec (ι : Type u) [Finite ι] [Fintype ι] (f : Module.End ℚ (ι → ℚ)) (X : Matrix ι ι ℤ) (hf : ∀ (v : ι → ℚ), f v = (X.map Int.cast).mulVec v) (s : ι) : f ↑((coordinateLatticeBasis ι) s) = ∑ r : ι, X r s • ↑((coordinateLatticeBasis ι) r)

An endomorphism represented by an integral matrix has that matrix as its coordinate-lattice basis expansion.

@[simp]

theorem TauCeti.intCast_coordinateLatticeBasis_repr (ι : Type u) [Finite ι] (v : ↥(coordinateLattice ι)) (i : ι) : ↑(((coordinateLatticeBasis ι).repr v) i) = ↑v i

Extending a coordinate-lattice basis coefficient to ℚ recovers the corresponding rational coordinate.

instance TauCeti.instIsLatticeCoordinateLattice (ι : Type u) [Finite ι] : Submodule.IsLattice ℚ (coordinateLattice ι)

The standard coordinate lattice is finitely generated and spans its rational coordinate space.