GL_n Hecke Algebra Commutativity via Transpose

The transpose ξ ↦ ᵗξ is an anti-automorphism of GL_n(ℚ) that preserves SL_n(ℤ) and the positive-determinant integer matrices Δ. Since every double coset has a diagonal representative (which is fixed by transpose), Shimura's Proposition 3.8 gives commutativity of the Hecke ring.

Main results

• GLPairAntiInvolution -- the transpose as an AntiInvolution for GLPair n
• instCommRingHeckeAlgebra -- CommRing (HeckeAlgebra n)

noncomputable def HeckeRing.GLn.GLTransposeEquiv (n : ℕ) : GL (Fin n) ℚ ≃* (GL (Fin n) ℚ)ᵐᵒᵖ

The transpose map GL_n(ℚ) → GL_n(ℚ)ᵐᵒᵖ as a multiplicative equivalence.

Equations

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

theorem HeckeRing.GLn.GL_transposeEquiv_val (n : ℕ) (g : GL (Fin n) ℚ) : ↑(MulOpposite.unop ((GLTransposeEquiv n) g)) = (↑g).transpose

theorem HeckeRing.GLn.GL_transposeEquiv_involutive (n : ℕ) (g : GL (Fin n) ℚ) : MulOpposite.unop ((GLTransposeEquiv n) (MulOpposite.unop ((GLTransposeEquiv n) g))) = g

theorem HeckeRing.GLn.SLnZ_to_GLnQ_transpose (n : ℕ) (σ : Matrix.SpecialLinearGroup (Fin n) ℤ) : MulOpposite.unop ((GLTransposeEquiv n) ((Matrix.SpecialLinearGroup.mapGL ℚ) σ)) = (Matrix.SpecialLinearGroup.mapGL ℚ) σ.transpose

theorem HeckeRing.GLn.GL_transpose_mem_SLnZ (n : ℕ) {g : GL (Fin n) ℚ} (hg : g ∈ SLnZSubgroup n) : MulOpposite.unop ((GLTransposeEquiv n) g) ∈ SLnZSubgroup n

theorem HeckeRing.GLn.HasIntEntries.transpose (n : ℕ) {g : GL (Fin n) ℚ} (hg : HasIntEntries n g) : HasIntEntries n (MulOpposite.unop ((GLTransposeEquiv n) g))

theorem HeckeRing.GLn.GL_transpose_mem_posDetInt (n : ℕ) {g : GL (Fin n) ℚ} (hg : g ∈ posDetIntSubmonoid n) : MulOpposite.unop ((GLTransposeEquiv n) g) ∈ posDetIntSubmonoid n

theorem HeckeRing.GLn.diagMat_GL_transpose_eq (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : MulOpposite.unop ((GLTransposeEquiv n) (diagMat n a)) = diagMat n a

noncomputable def HeckeRing.GLn.GLPairAntiInvolution (n : ℕ) [NeZero n] : AntiInvolution (GLPair n)

The transpose as an AntiInvolution for GLPair n.

Equations

• HeckeRing.GLn.GLPairAntiInvolution n = { toFun := (HeckeRing.GLn.GLTransposeEquiv n).toMonoidHom, involutive := ⋯, map_H := ⋯, map_Δ := ⋯ }

theorem HeckeRing.GLn.GL_pair_onHeckeCoset_eq (n : ℕ) [NeZero n] (D : HeckeCoset (GLPair n)) : (GLPairAntiInvolution n).onHeckeCoset D = D

Transpose fixes every double coset of GLPair n.

@[implicit_reducible]

noncomputable instance HeckeRing.GLn.instCommRingHeckeAlgebra (n : ℕ) [NeZero n] : CommRing (HeckeAlgebra n)

Shimura Proposition 3.8 for GL_n: the Hecke algebra is commutative.

Equations

• HeckeRing.GLn.instCommRingHeckeAlgebra n = HeckeRing.instCommRingOfAntiInvolution (HeckeRing.GLn.GLPairAntiInvolution n) ⋯