Commutativity of the `GL_n` Hecke ring #

Transposition ξ ↦ ᵗξ is an anti-automorphism of GL_n(ℚ) preserving both SL_n(ℤ) and the submonoid Δ of integral matrices of positive determinant, so it restricts to a HeckeAntiInvolution of the arithmetic Hecke datum. Every double coset has a diagonal representative and transposition fixes a diagonal matrix, so the involution it induces on SL_n(ℤ) \ Δ / SL_n(ℤ) is the identity. Shimura's Proposition 3.8 then applies: the integral Hecke ring of GL_n is commutative.

Main definitions #

HeckeRing.GLn.transposeGLEquiv: transposition as an isomorphism GL_n(ℚ) ≃* GL_n(ℚ)ᵐᵒᵖ.
HeckeRing.GLn.transposeAntiInvolution: the induced HeckeAntiInvolution of (Δ, SL_n(ℤ)).

Main results #

HeckeRing.GLn.transposeAntiInvolution_onHeckeCoset_eq_self: transposition fixes every double coset.
HeckeRing.GLn.commSemiringHeckeRing: Shimura's Proposition 3.8 for GL_n — the Hecke ring is commutative over any commutative semiring of coefficients, with HeckeRing.GLn.commSemiringIntegralHeckeRing the integral case.

References #

G. Shimura, Introduction to the arithmetic theory of automorphic functions, Proposition 3.8.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/TransposeAntiInvolution.lean, Chris Birkbeck).

source

def HeckeRing.GLn.transposeGLEquiv (n : ℕ) :

GL (Fin n) ℚ ≃* (GL (Fin n) ℚ)ᵐᵒᵖ

Transposition as an isomorphism GL_n(ℚ) ≃* GL_n(ℚ)ᵐᵒᵖ: it reverses products, so it lands in the opposite group.

Equations

HeckeRing.GLn.transposeGLEquiv n = (Units.mapEquiv (Matrix.transposeRingEquiv (Fin n) ℚ).toMulEquiv).trans Units.opEquiv

Instances For

source

@[simp]

theorem HeckeRing.GLn.transposeGLEquiv_coe (n : ℕ) (g : GL (Fin n) ℚ) :

↑(MulOpposite.unop ((transposeGLEquiv n) g)) = (↑g).transpose

Transposition acts on the underlying matrix as Matrix.transpose.

source

@[simp]

theorem HeckeRing.GLn.transposeGLEquiv_transposeGLEquiv (n : ℕ) (g : GL (Fin n) ℚ) :

MulOpposite.unop ((transposeGLEquiv n) (MulOpposite.unop ((transposeGLEquiv n) g))) = g

Transposing twice is the identity.

source

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

MulOpposite.unop ((transposeGLEquiv n) g) ∈ SLnZ n

Transposition preserves SL_n(ℤ): the transpose of an integral matrix of determinant one again has determinant one.

source

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

MulOpposite.unop ((transposeGLEquiv n) g) ∈ posDetInt n

Transposition preserves Δ: it transposes the integral witness and leaves the determinant unchanged.

source

@[simp]

theorem HeckeRing.GLn.transposeGLEquiv_natDiagGL (n : ℕ) (a : Fin n → ℕ) :

MulOpposite.unop ((transposeGLEquiv n) (natDiagGL n a)) = natDiagGL n a

Transposition fixes every diagonal matrix, including the junk value 1 taken when some entry vanishes.

source

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

HeckeAntiInvolution (posDetInt n) (SLnZ n)

Transposition as an anti-involution of the arithmetic Hecke datum (Δ, SL_n(ℤ)).

Equations

HeckeRing.GLn.transposeAntiInvolution n = HeckeAntiInvolution.ofAmbient (HeckeRing.GLn.transposeGLEquiv n).toMonoidHom ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem HeckeRing.GLn.transposeAntiInvolution_bar (n : ℕ) {x : GL (Fin n) ℚ} (hx : x ∈ posDetInt n) :

(transposeAntiInvolution n).bar x hx = MulOpposite.unop ((transposeGLEquiv n) x)

The anti-involution acts as transposition, unfolding the sealed definition.

source

@[simp]

theorem HeckeRing.GLn.transposeAntiInvolution_onHeckeCoset_eq_self (n : ℕ) [NeZero n] (D : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)) :

(transposeAntiInvolution n).onHeckeCoset D = D

Transposition fixes every double coset: each one has a diagonal representative, and transposition fixes diagonal matrices.

source

@[instance_reducible]

noncomputable def HeckeRing.GLn.commSemiringHeckeRing (n : ℕ) [NeZero n] (R : Type u_1) [CommSemiring R] :

CommSemiring (HeckeRing (posDetInt n) (SLnZ n) R)

Shimura's Proposition 3.8 for GL_n: the Hecke ring of GL_n over any commutative semiring is commutative, transposition being an anti-involution that fixes every double coset.

Equations