Coprime Product and Scalar Multiplication in the Hecke Ring

Shimura Propositions 3.16 and 3.17: when determinants are coprime, the product of double cosets is a single double coset with multiplicity 1. Scalar double cosets T(c,...,c) act by scaling.

Main results

• T_diag_scalar_mul — T(c,...,c) · T(b₁,...,bₙ) = T(cb₁,...,cbₙ)
• T_diag_mul_coprime — T(a) · T(b) = T(a·b) when (∏aᵢ, ∏bᵢ) = 1

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3.2

theorem HeckeRing.GLn.pi_mul_pos (n : ℕ) (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) (i : Fin n) : 0 < (a * b) i

Pointwise product of positive sequences is positive.

theorem HeckeRing.GLn.DivChain_mul (n : ℕ) (a b : Fin n → ℕ) (ha : DivChain n a) (hb : DivChain n b) : DivChain n (a * b)

Pointwise product of two divisibility chains is a divisibility chain.

@[simp]

theorem HeckeRing.GLn.diagMat_mul (n : ℕ) (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) : diagMat n a * diagMat n b = diagMat n (a * b)

Product of diagonal GL_n(ℚ) elements is diagonal with pointwise product.

theorem HeckeRing.GLn.T_diag_eq_T_mk_mul (n : ℕ) [NeZero n] (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) (_hab : DivChain n (a * b)) : TDiag (a * b) = ⟦⟨diagMat n a * diagMat n b, ⋯⟩⟧

theorem HeckeRing.GLn.diagMat_scalar_eq (n c : ℕ) (hc : 0 < c) : ↑(diagMat n fun (x : Fin n) => c) = ↑c • 1

theorem HeckeRing.GLn.diagMat_scalar_comm (n c : ℕ) (hc : 0 < c) (g : GL (Fin n) ℚ) : (diagMat n fun (x : Fin n) => c) * g = g * diagMat n fun (x : Fin n) => c

theorem HeckeRing.GLn.diagMat_scalar_conj_eq (n c : ℕ) (hc : 0 < c) (x : GL (Fin n) ℚ) : ((diagMat n fun (x : Fin n) => c)⁻¹ * x * diagMat n fun (x : Fin n) => c) = x

theorem HeckeRing.GLn.conjAct_scalar_smul_eq (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) : ConjAct.toConjAct (diagMat n fun (x : Fin n) => c) • (GLPair n).H = (GLPair n).H

theorem HeckeRing.GLn.HeckeCoset_deg_scalar (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) : HeckeCosetDeg (GLPair n) (TDiag fun (x : Fin n) => c) = 1

The degree of a scalar double coset T(c,...,c) is 1.

theorem HeckeRing.GLn.T_diag_scalar_mul (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) (b : Fin n → ℕ) (hb_pos : ∀ (i : Fin n), 0 < b i) (hb : DivChain n b) : (TElem fun (x : Fin n) => c) * TElem b = TElem ((fun (x : Fin n) => c) * b)

Scalar multiplication in the Hecke ring (Shimura Proposition 3.17).

theorem HeckeRing.GLn.SLnZ_CRT_decomposition (n d d' : ℕ) (hd : 0 < d) (hd' : 0 < d') (hcop : d.Coprime d') (τ : Matrix.SpecialLinearGroup (Fin n) ℤ) : ∃ (τ₁ : Matrix.SpecialLinearGroup (Fin n) ℤ) (τ₂ : Matrix.SpecialLinearGroup (Fin n) ℤ), τ = τ₁ * τ₂ ∧ (∀ (i j : Fin n), ↑d ∣ ↑τ₁ i j - if i = j then 1 else 0) ∧ ∀ (i j : Fin n), ↑d' ∣ ↑τ₂ i j - if i = j then 1 else 0

Chinese Remainder Theorem for SL_n(ℤ): every element decomposes as a product of congruence classes when gcd(d, d') = 1.

theorem HeckeRing.GLn.conjugate_congruent_mem_SLnZ (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (_hdiv : DivChain n a) (τ : Matrix.SpecialLinearGroup (Fin n) ℤ) (hcong : ∀ (i j : Fin n), ∏ k : Fin n, ↑(a k) ∣ ↑τ i j - if i = j then 1 else 0) : ∃ (σ : Matrix.SpecialLinearGroup (Fin n) ℤ), (Matrix.SpecialLinearGroup.mapGL ℚ) σ = diagMat n a * (Matrix.SpecialLinearGroup.mapGL ℚ) τ * (diagMat n a)⁻¹

A congruent-to-identity element conjugated by diag(a) remains in SL_n(ℤ).

theorem HeckeRing.GLn.inv_conjugate_congruent_mem_SLnZ (n : ℕ) (b : Fin n → ℕ) (hb : ∀ (i : Fin n), 0 < b i) (_hdiv : DivChain n b) (τ : Matrix.SpecialLinearGroup (Fin n) ℤ) (hcong : ∀ (i j : Fin n), ∏ k : Fin n, ↑(b k) ∣ ↑τ i j - if i = j then 1 else 0) : ∃ (σ : Matrix.SpecialLinearGroup (Fin n) ℤ), (Matrix.SpecialLinearGroup.mapGL ℚ) σ = (diagMat n b)⁻¹ * (Matrix.SpecialLinearGroup.mapGL ℚ) τ * diagMat n b

A congruent-to-identity element conjugated by diag(b)⁻¹ remains in SL_n(ℤ).

theorem HeckeRing.GLn.doubleCoset_mul_coprime_mem (n : ℕ) (a b : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (hb_pos : ∀ (i : Fin n), 0 < b i) (ha : DivChain n a) (hb : DivChain n b) (hcop : (∏ i : Fin n, a i).Coprime (∏ i : Fin n, b i)) (τ : Matrix.SpecialLinearGroup (Fin n) ℤ) : diagMat n a * (Matrix.SpecialLinearGroup.mapGL ℚ) τ * diagMat n b ∈ DoubleCoset.doubleCoset (diagMat n (a * b)) ↑(SLnZSubgroup n) ↑(SLnZSubgroup n)

Set-level coprime product (Shimura Proposition 3.16, key step).

theorem HeckeRing.GLn.mulMap_coprime_eq (n : ℕ) [NeZero n] (a b : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (hb_pos : ∀ (i : Fin n), 0 < b i) (ha : DivChain n a) (hb : DivChain n b) (_hab : DivChain n (a * b)) (hcop : (∏ i : Fin n, a i).Coprime (∏ i : Fin n, b i)) (p : decompQuot (GLPair n) (TDiag a).rep × decompQuot (GLPair n) (TDiag b).rep) : mulMap (GLPair n) (TDiag a).rep (TDiag b).rep p = TDiag (a * b)

theorem HeckeRing.GLn.T_diag_mul_coprime (n : ℕ) [NeZero n] (a b : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (hb_pos : ∀ (i : Fin n), 0 < b i) (ha : DivChain n a) (hb : DivChain n b) (hcop : (∏ i : Fin n, a i).Coprime (∏ i : Fin n, b i)) : TElem a * TElem b = TElem (a * b)

Coprime product in the Hecke ring (Shimura Proposition 3.16).