The double coset a pair of right-coset representatives lands in

Composing two Hecke operators indexed by double cosets Γ₁ δ₁ Γ₂ = ⊔ᵥ Γ₁ aᵥ and Γ₂ δ₂ Γ₃ = ⊔_w Γ₂ b_w — whether they act on functions on ℍ by slash sums or on modular symbols — produces a double sum over the products aᵥ b_w. Rewriting that double sum as ∑_D m(D₁, D₂; D) • T_D is a piece of set-level bookkeeping with no operator in it: group the pairs (v, w) by the double coset Γ₁ (aᵥ b_w) Γ₃ their product lies in, and count how often the pairs over one double coset D meet each of its right cosets. This file supplies that bookkeeping once, for both consumers.

pairCoset D₁ D₂ is the grouping map, from pairs of right-coset indices to HeckeCoset Δ Γ₁ Γ₃, characterised by pairCoset_eq_iff. The count is card_pairs_pairCoset_rightCoset_eq_multiplicity: among the pairs over D, the number whose product spans a given right coset Γ₁ x of D is Shimura's multiplicity in its right-coset indexed form DoubleCoset.multiplicity Γ₃ Γ₂ Γ₁ δ₂⁻¹ δ₁⁻¹ δ₃⁻¹, independently of x. Its two ingredients are DoubleCoset.card_pairs_mem_rightCoset_eq_multiplicity, which reconciles the handedness, and DoubleCoset.card_pairs_mem_rightCoset_congr, which supplies the uniformity in x.

Between images Γᵢ.map (mapGL ℚ) of subgroups of SL(2, ℤ), the double cosets met by the products of two integral representatives are again integral (mem_intEntries_of_mem_image_pairCoset), which is what operators indexed by integral double cosets need at each output coset of the composition law.

Main results

• HeckeRing.GL2.pairCoset: the double coset Γ₁ (aᵥ b_w) Γ₃ that a pair of right-coset representatives lands in — the map the double sum is fibred over.
• HeckeRing.GL2.pairCoset_eq_iff: a pair lies in the fibre over D exactly when the product of its two representatives lies in D's double coset.
• HeckeRing.GL2.PairCosetFiber: among the pairs lying over D, those whose product spans the right coset Γ₁ x — the type the multiplicity counts.
• HeckeRing.GL2.card_pairs_pairCoset_rightCoset_eq_multiplicity: each right coset of a double coset D is met by m(D₁, D₂; D) of the pairs, whichever right coset of D is chosen.
• HeckeRing.GL2.mem_intEntries_of_mem_image_pairCoset: between images of subgroups of SL(2, ℤ), every double coset met by the products of two integral representatives is integral.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4: the displayed computation preceding Proposition 3.37.

noncomputable def HeckeRing.GL2.pairCoset {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ Γ₃ : Subgroup (GL (Fin 2) ℚ)} [IsHeckeTriple Δ Γ₁ Γ₂] [IsHeckeTriple Δ Γ₂ Γ₃] (D₁ : HeckeCoset Δ Γ₁ Γ₂) (D₂ : HeckeCoset Δ Γ₂ Γ₃) (p : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D₁))⁻¹ × DoubleCoset.DecompQuotient Γ₃ Γ₂ (↑(Quotient.out D₂))⁻¹) : HeckeCoset Δ Γ₁ Γ₃

The double coset Γ₁ (aᵥ b_w) Γ₃ a pair of representatives lands in. This is the map the double sum of a composite of two Hecke operators is fibred over.

Equations

• HeckeRing.GL2.pairCoset D₁ D₂ p = HeckeCoset.mk Γ₁ Γ₃ (HeckeRing.GL2.pairRep✝ D₁ D₂ p)

@[simp]

theorem HeckeRing.GL2.pairCoset_eq_iff {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ Γ₃ : Subgroup (GL (Fin 2) ℚ)} [IsHeckeTriple Δ Γ₁ Γ₂] [IsHeckeTriple Δ Γ₂ Γ₃] {D₁ : HeckeCoset Δ Γ₁ Γ₂} {D₂ : HeckeCoset Δ Γ₂ Γ₃} {D : HeckeCoset Δ Γ₁ Γ₃} {p : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D₁))⁻¹ × DoubleCoset.DecompQuotient Γ₃ Γ₂ (↑(Quotient.out D₂))⁻¹} : pairCoset D₁ D₂ p = D ↔ DoubleCoset.rightCosetRep D₁ p.1 * DoubleCoset.rightCosetRep D₂ p.2 ∈ DoubleCoset.doubleCoset ↑(Quotient.out D) ↑Γ₁ ↑Γ₃

pairCoset is characterised by membership: a pair lies in the fibre over D exactly when the product of its two representatives lies in the double coset of D.

@[reducible, inline]

abbrev HeckeRing.GL2.PairCosetFiber {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ Γ₃ : Subgroup (GL (Fin 2) ℚ)} [IsHeckeTriple Δ Γ₁ Γ₂] [IsHeckeTriple Δ Γ₂ Γ₃] (D₁ : HeckeCoset Δ Γ₁ Γ₂) (D₂ : HeckeCoset Δ Γ₂ Γ₃) (D : HeckeCoset Δ Γ₁ Γ₃) (x : GL (Fin 2) ℚ) : Type

The pairs over D whose product spans the right coset Γ₁ x. Among the index pairs whose product lies in the double coset D, those whose product generates the same right coset of Γ₁ as x does. card_pairs_pairCoset_rightCoset_eq_multiplicity counts this type; its nonemptiness is what identifies the support of the Hecke structure constants downstream.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.GL2.card_pairs_pairCoset_rightCoset_eq_multiplicity {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ Γ₃ : Subgroup (GL (Fin 2) ℚ)} [IsHeckeTriple Δ Γ₁ Γ₂] [IsHeckeTriple Δ Γ₂ Γ₃] {D₁ : HeckeCoset Δ Γ₁ Γ₂} {D₂ : HeckeCoset Δ Γ₂ Γ₃} {D : HeckeCoset Δ Γ₁ Γ₃} {x : GL (Fin 2) ℚ} (hx : x ∈ DoubleCoset.doubleCoset ↑(Quotient.out D) ↑Γ₁ ↑Γ₃) : Nat.card (PairCosetFiber D₁ D₂ D x) = DoubleCoset.multiplicity Γ₃ Γ₂ Γ₁ (↑(Quotient.out D₂))⁻¹ (↑(Quotient.out D₁))⁻¹ (↑(Quotient.out D))⁻¹

Each right coset of a double coset D is met by Shimura's multiplicity m(D₁, D₂; D) many pairs, whichever x ∈ D names that right coset: among the pairs lying over D, the number whose product spans the right coset Γ₁ x does not depend on x.

theorem HeckeRing.GL2.mem_intEntries_of_mem_image_pairCoset {Δ : Submonoid (GL (Fin 2) ℚ)} (Γ₁ Γ₂ Γ₃ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [IsHeckeTriple Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₁) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₂)] [IsHeckeTriple Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₂) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₃)] (D₁ : HeckeCoset Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₁) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₂)) (D₂ : HeckeCoset Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₂) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₃)) (hD₁ : ↑(Quotient.out D₁) ∈ GLn.intEntries 2) (hD₂ : ↑(Quotient.out D₂) ∈ GLn.intEntries 2) {D : HeckeCoset Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₁) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ₃)} (hD : D ∈ Finset.image (pairCoset D₁ D₂) Finset.univ) : ↑(Quotient.out D) ∈ GLn.intEntries 2

Every double coset met by the products of the representatives is integral. Between images Γᵢ' = Γᵢ.map (mapGL ℚ) of subgroups of SL(2, ℤ), if D₁.out and D₂.out are integral then so is D.out for every D in the image of pairCoset D₁ D₂: such a D is the double coset of a product aᵥ b_u of two integral representatives, and HeckeRing.GLn.mem_intEntries_of_mem_doubleCoset applies. This supplies the integrality proof that operators indexed by integral double cosets ask for at each output coset of the composition law; nothing is assumed of the other elements of Δ.