Hecke double cosets at a normalizing element

GroupTheory/DoubleCoset/Normalizer.lean collapses a double coset ΓgΓ to the single right coset Γg when g normalizes Γ. This file draws the Hecke-ring consequences, for a Hecke triple (Δ, Γ, Γ) and an x : Δ normalizing Γ:

• the underlying set of HeckeCoset.mk Γ Γ x is Γx, and so is the double coset of its chosen representative — the shape in which the slash sum of a double coset consumes a decomposition;
• the chosen representative again normalizes Γ, so the decomposition quotient Γ ⧸ (Γ ∩ xΓx⁻¹) is a subsingleton;
• consequently the basis elements multiply with no structure constant to count, [ΓxΓ] · [ΓyΓ] = [Γ(xy)Γ], as soon as one of the two factors normalizes Γ — the other is an arbitrary element of Δ. Both handednesses are proved, and neither follows from the other: multiplicity Γ₁ Γ₂ Γ₃ g h d quotients by Γ₃ on the right only, so it is not symmetric in its two arguments.

The last statement is what lets a submonoid of the normalizer of Γ act on the Hecke ring through its basis elements, and, because the right factor is unconstrained, lets that action be computed against an arbitrary basis element rather than only against another normalizing one. For Γ₁(N) ⊴ Γ₀(N) it is the diamond direction of the Γ₁(N) Hecke ring, in HeckeRing/GL2/Gamma1/DiamondCosets.lean.

Main results

• DoubleCoset.subsingleton_decompQuotient_of_mem_normalizer: the decomposition quotient at a normalizing element is a subsingleton.
• HeckeCoset.toSet_mk_eq_rightCoset_of_mem_normalizer and HeckeCoset.doubleCoset_out_mk_eq_rightCoset_of_mem_normalizer: the double coset of a normalizing element is the single right coset Γx, at x itself and at the chosen representative.
• DoubleCoset.multiplicity_le_one_of_mem_normalizer_right: the mirror of multiplicity_le_one_of_subsingleton, bounding via the second decomposition quotient. It asks only that the second element normalize Γ; the subsingleton hypothesis its counterpart takes is implied here.
• HeckeCosetModule.single_mul_single_of_mem_normalizer and HeckeCosetModule.single_mul_single_of_mem_normalizer_right: the basis element of a normalizing element times the basis element of an arbitrary one is the basis element of their product, with the normalizing factor on either side.
• HeckeCosetModule.commute_single_of_mem_normalizer: consequently a commutation question in the Hecke ring is discharged by the single coset identity Γ(xy)Γ = Γ(yx)Γ.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.1.

theorem DoubleCoset.subsingleton_decompQuotient_of_mem_normalizer {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑Γ) : Subsingleton (DecompQuotient Γ Γ g)

The decomposition quotient at a normalizing element is a subsingleton: the stabilizer Γ ∩ gΓg⁻¹ is all of Γ. This is subsingleton_decompQuotient_of_mem with membership in Γ weakened to membership in its normalizer.

theorem DoubleCoset.multiplicity_le_one_of_mem_normalizer_right {G : Type u_1} [Group G] {Γ : Subgroup G} {g h d : G} (hh : h ∈ Subgroup.normalizer ↑Γ) : multiplicity Γ Γ Γ g h d ≤ 1

A second factor that normalizes Γ forces multiplicity at most one.

The mirror of multiplicity_le_one_of_subsingleton, which bounds via the first decomposition quotient. multiplicity is not symmetric — it quotients by Γ₃ on the right only — so this is a separate statement rather than that one applied backwards, and normalisation is what replaces the subsingleton hypothesis the first-quotient version takes: here it is implied, by subsingleton_decompQuotient_of_mem_normalizer.

theorem HeckeCoset.toSet_mk_eq_rightCoset_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x : ↥Δ} (hx : ↑x ∈ Subgroup.normalizer ↑Γ) : (mk Γ Γ x).toSet = MulOpposite.op ↑x • ↑Γ

The double coset of a normalizing element is a single right coset, ΓxΓ = Γx.

theorem HeckeCoset.doubleCoset_out_mk_eq_rightCoset_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x : ↥Δ} (hx : ↑x ∈ Subgroup.normalizer ↑Γ) : DoubleCoset.doubleCoset ↑(Quotient.out (mk Γ Γ x)) ↑Γ ↑Γ = MulOpposite.op ↑x • ↑Γ

The same collapse read at the chosen representative of HeckeCoset.mk Γ Γ x, which is the shape a decomposition of a double coset into right cosets is stated in.

theorem HeckeCoset.rep_mk_mem_rightCoset_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x : ↥Δ} (hx : ↑x ∈ Subgroup.normalizer ↑Γ) : ↑(mk Γ Γ x).rep ∈ MulOpposite.op ↑x • ↑Γ

The chosen representative of HeckeCoset.mk Γ Γ x lies in the right coset Γx.

theorem HeckeCoset.rep_mk_mem_normalizer_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x : ↥Δ} (hx : ↑x ∈ Subgroup.normalizer ↑Γ) : ↑(mk Γ Γ x).rep ∈ Subgroup.normalizer ↑Γ

The chosen representative of HeckeCoset.mk Γ Γ x again normalizes Γ: it lies in ΓxΓ, all of whose elements do.

theorem HeckeCoset.mulMap_rep_mk_eq_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x y : ↥Δ} [IsHeckeTriple Δ Γ Γ] (hx : ↑x ∈ Subgroup.normalizer ↑Γ) (p : DoubleCoset.DecompQuotient Γ Γ ↑(mk Γ Γ x).rep × DoubleCoset.DecompQuotient Γ Γ ↑(mk Γ Γ y).rep) : mulMap Γ Γ Γ (mk Γ Γ x).rep (mk Γ Γ y).rep p = mk Γ Γ (x * y)

Every value of HeckeCoset.mulMap at a normalizing left factor is the double coset of the product, Γ · xy · Γ — so there is no structure constant to compute.

Only the left factor need normalize Γ. The right one is an arbitrary element of Δ, which is what lets this compute a product against an arbitrary basis element rather than only against another normalizing one.

theorem HeckeCoset.mulMap_rep_mk_eq_of_mem_normalizer_right {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x y : ↥Δ} [IsHeckeTriple Δ Γ Γ] (hy : ↑y ∈ Subgroup.normalizer ↑Γ) (p : DoubleCoset.DecompQuotient Γ Γ ↑(mk Γ Γ x).rep × DoubleCoset.DecompQuotient Γ Γ ↑(mk Γ Γ y).rep) : mulMap Γ Γ Γ (mk Γ Γ x).rep (mk Γ Γ y).rep p = mk Γ Γ (x * y)

Every value of HeckeCoset.mulMap at a normalizing right factor is the double coset of the product — the mirror of mulMap_rep_mk_eq_of_mem_normalizer, with the normalisation hypothesis on the right factor instead of the left.

theorem HeckeCosetModule.single_mul_single_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x y : ↥Δ} [IsHeckeTriple Δ Γ Γ] (R : Type u_2) [Semiring R] (hx : ↑x ∈ Subgroup.normalizer ↑Γ) : single R (HeckeCoset.mk Γ Γ x) 1 * single R (HeckeCoset.mk Γ Γ y) 1 = single R (HeckeCoset.mk Γ Γ (x * y)) 1

A normalizing basis element multiplies any other, [ΓxΓ] · [ΓyΓ] = [Γ(xy)Γ], over any coefficient semiring, when x normalizes Γ. y is arbitrary.

There is no structure constant to compute: x normalizes Γ, so its decomposition quotient is a subsingleton and multiplicity ≤ 1 follows, and every pair of representatives multiplies into the same double coset. Both facts need only x.

theorem HeckeCosetModule.single_mul_single_of_mem_normalizer_right {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x y : ↥Δ} [IsHeckeTriple Δ Γ Γ] (R : Type u_2) [Semiring R] (hy : ↑y ∈ Subgroup.normalizer ↑Γ) : single R (HeckeCoset.mk Γ Γ x) 1 * single R (HeckeCoset.mk Γ Γ y) 1 = single R (HeckeCoset.mk Γ Γ (x * y)) 1

A normalizing basis element multiplies any other from the right, [ΓxΓ] · [ΓyΓ] = [Γ(xy)Γ], when y normalizes Γ. x is arbitrary.

The mirror of single_mul_single_of_mem_normalizer. It is a separate proof rather than that one applied backwards: multiplicity Γ₁ Γ₂ Γ₃ g h d quotients by Γ₃ on the right only, so the two sides are not interchangeable, and the bound used here is multiplicity_le_one_of_mem_normalizer_right.

theorem HeckeCosetModule.commute_single_of_mem_normalizer {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {x y : ↥Δ} [IsHeckeTriple Δ Γ Γ] (R : Type u_2) [Semiring R] (hx : ↑x ∈ Subgroup.normalizer ↑Γ) (hxy : HeckeCoset.mk Γ Γ (x * y) = HeckeCoset.mk Γ Γ (y * x)) : Commute (single R (HeckeCoset.mk Γ Γ x) 1) (single R (HeckeCoset.mk Γ Γ y) 1)

A normalizing basis element commutes with another whenever the double cosets of their two products agree, Γ(xy)Γ = Γ(yx)Γ.

This is what having both handednesses buys: the left-handed lemma computes [ΓxΓ] · [ΓyΓ] and the right-handed one computes [ΓyΓ] · [ΓxΓ], both as basis elements, so a commutation question in the Hecke ring is discharged by the single coset identity Γ(xy)Γ = Γ(yx)Γ. Neither lemma alone suffices, since each constrains a different side.

Only this direction is claimed, and only x need normalize Γ; y is arbitrary.