GL_n HeckePair #

Constructs the canonical HeckePair (GL (Fin n) ℚ) with:

H = SL_n(ℤ) (embedded in GL_n(ℚ))
Δ = {α ∈ M_n(ℤ) ∩ GL_n(ℚ) | det(α) > 0} (integer matrices with positive determinant)

This is the foundation for the Hecke ring of GL_n following Shimura §3.2.

Main definitions #

SLnZSubgroup — SL_n(ℤ) as a subgroup of GL_n(ℚ) (via mathlib's mapGL ℚ)
posDetIntSubmonoid — positive-determinant integer matrices as a submonoid of GL_n(ℚ)
GLPair — the standard HeckePair

Main results #

SLnZ_le_posDetInt — SL_n(ℤ) ⊆ Δ
posDetInt_le_commensurator — Δ ⊆ commensurator(SL_n(ℤ))

source

@[reducible, inline]

noncomputable abbrev HeckeRing.GLn.SLnZSubgroup (n : ℕ) :

Subgroup (GL (Fin n) ℚ)

SL_n(ℤ) as a subgroup of GL_n(ℚ), via mapGL ℚ : SL(n, ℤ) →* GL(n, ℚ). Following mathlib's pattern for arithmetic subgroups.

Equations

HeckeRing.GLn.SLnZSubgroup n = (Matrix.SpecialLinearGroup.mapGL ℚ).range

Instances For

source

@[implicit_reducible]

noncomputable def HeckeRing.GLn.SLnZCoe (n : ℕ) :

Coe (Matrix.SpecialLinearGroup (Fin n) ℤ) (GL (Fin n) ℚ)

Coercion from SL_n(ℤ) to GL_n(ℚ) via mapGL ℚ.

Equations

HeckeRing.GLn.SLnZCoe n = { coe := ⇑(Matrix.SpecialLinearGroup.mapGL ℚ) }

Instances For

source

theorem HeckeRing.GLn.coe_mem_SLnZ (n : ℕ) (σ : Matrix.SpecialLinearGroup (Fin n) ℤ) :

(Matrix.SpecialLinearGroup.mapGL ℚ) σ ∈ SLnZSubgroup n

source

def HeckeRing.GLn.HasIntEntries (n : ℕ) (g : GL (Fin n) ℚ) :

Prop

An element of GL_n(ℚ) has integer matrix entries if its underlying matrix is the image of an integer matrix under ℤ → ℚ.

Equations

HeckeRing.GLn.HasIntEntries n g = ∃ (A : Matrix (Fin n) (Fin n) ℤ), ↑g = A.map Int.cast

Instances For

source

theorem HeckeRing.GLn.SLnZ_subgroup_hasIntEntries (n : ℕ) {g : GL (Fin n) ℚ} (hg : g ∈ SLnZSubgroup n) :

HasIntEntries n g

source

@[simp]

theorem HeckeRing.GLn.hasIntEntries_one (n : ℕ) :

HasIntEntries n 1

The identity matrix has integer entries.

source

theorem HeckeRing.GLn.HasIntEntries.mul (n : ℕ) {a b : GL (Fin n) ℚ} (ha : HasIntEntries n a) (hb : HasIntEntries n b) :

HasIntEntries n (a * b)

Product of integer-entry matrices has integer entries.

source

theorem HeckeRing.GLn.det_intMat_cast (n : ℕ) (A : Matrix (Fin n) (Fin n) ℤ) :

(A.map Int.cast).det = ↑A.det

det (A.map Int.cast) = ↑(det A) for integer matrices cast to ℚ.

source

noncomputable def HeckeRing.GLn.posDetIntSubmonoid (n : ℕ) :

Submonoid (GL (Fin n) ℚ)

The submonoid of GL_n(ℚ) consisting of invertible matrices with integer entries and positive determinant. This is Shimura's Δ.

Equations

HeckeRing.GLn.posDetIntSubmonoid n = { carrier := {g : GL (Fin n) ℚ | HeckeRing.GLn.HasIntEntries n g ∧ 0 < (↑g).det}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

theorem HeckeRing.GLn.SLnZ_le_posDetInt (n : ℕ) :

(SLnZSubgroup n).toSubmonoid ≤ posDetIntSubmonoid n

SL_n(ℤ) ⊆ Δ: elements of SL_n(ℤ) have integer entries and det = 1 > 0.

Helper lemmas for the commensurator proof (Shimura Lemma 3.10) #

source

theorem HeckeRing.GLn.posDetInt_le_commensurator (n : ℕ) [NeZero n] :

posDetIntSubmonoid n ≤ (Subgroup.Commensurable.commensurator (SLnZSubgroup n)).toSubmonoid

Δ ⊆ commensurator(SL_n(ℤ)): for any integer matrix α with positive determinant, SL_n(ℤ) and α · SL_n(ℤ) · α⁻¹ are commensurable.

The key idea (Shimura Lemma 3.10): if α has integer entries with det(α) = d > 0, then the congruence subgroup Γ(d) = ker(SL_n(ℤ) → SL_n(ℤ/dℤ)) has finite index in SL_n(ℤ) and is contained in both SL_n(ℤ) ∩ α·SL_n(ℤ)·α⁻¹ and SL_n(ℤ) ∩ α⁻¹·SL_n(ℤ)·α, establishing commensurability.

source