Transporting Hecke multiplicities along group equivalences

The double-coset multiplicity is unchanged when the ambient group, its three subgroups, and the three elements are transported along a group equivalence. This is the naturality needed when a concrete Hecke action presents the structure constants after applying an automorphism of the ambient group.

Main results

• DoubleCoset.multiplicity_map_equiv: transport of Shimura's multiplicity along a group equivalence.
• DoubleCoset.multiplicity_doubleCoset_congr_second: invariance in the second input.
• DoubleCoset.multiplicity_doubleCoset_congr_first_of_comm: invariance in the first input when the multiplicity is symmetric.

@[simp]

theorem DoubleCoset.mem_doubleCoset_map_equiv_iff {G : Type u_1} {K : Type u_2} [Group G] [Group K] (e : G ≃* K) (H₁ H₂ : Subgroup G) (g x : G) : e x ∈ doubleCoset (e g) (⇑e '' ↑H₁) (⇑e '' ↑H₂) ↔ x ∈ doubleCoset g ↑H₁ ↑H₂

Membership in a double coset is preserved by a group equivalence.

noncomputable def DoubleCoset.decompQuotientEquivMap {G : Type u_1} {K : Type u_2} [Group G] [Group K] (e : G ≃* K) (H₁ H₂ : Subgroup G) (g : G) : DecompQuotient H₁ H₂ g ≃ DecompQuotient (Subgroup.map (↑e) H₁) (Subgroup.map (↑e) H₂) (e g)

A group equivalence carries the decomposition quotient of g to that of its image. The special case of decompQuotientEquivMapOfInjective at an isomorphism, which is the only injective homomorphism the multiplicity transport needs.

Equations

• DoubleCoset.decompQuotientEquivMap e H₁ H₂ g = DoubleCoset.decompQuotientEquivMapOfInjective ↑e ⋯ H₁ H₂ g

@[simp]

theorem DoubleCoset.decompQuotientEquivMap_mk {G : Type u_1} {K : Type u_2} [Group G] [Group K] (e : G ≃* K) (H₁ H₂ : Subgroup G) (g : G) (x : ↥H₁) : (decompQuotientEquivMap e H₁ H₂ g) ↑x = ↑((e.subgroupMap H₁) x)

The image of a decomposition class represented by x is represented by e x.

theorem DoubleCoset.decompQuotientEquivMap_out {G : Type u_1} {K : Type u_2} [Group G] [Group K] (e : G ≃* K) (H₁ H₂ : Subgroup G) (g : G) (i : DecompQuotient H₁ H₂ g) : (↑e g)⁻¹ * ((↑(Quotient.out ((decompQuotientEquivMap e H₁ H₂ g) i)))⁻¹ * ↑e ↑(Quotient.out i)) * ↑e g ∈ Subgroup.map (↑e) H₂

The chosen representative after transport differs from the transported representative by an element of the stabilizer.

@[simp]

theorem DoubleCoset.multiplicity_map_equiv {G : Type u_1} {K : Type u_2} [Group G] [Group K] (e : G ≃* K) (H₁ H₂ H₃ : Subgroup G) (g h d : G) : multiplicity (Subgroup.map (↑e) H₁) (Subgroup.map (↑e) H₂) (Subgroup.map (↑e) H₃) (e g) (e h) (e d) = multiplicity H₁ H₂ H₃ g h d

Shimura's multiplicity is unchanged when all of its data are transported along a group equivalence, without any finiteness hypothesis.

theorem DoubleCoset.multiplicity_doubleCoset_congr_second {G : Type u_1} [Group G] (H₁ H₂ H₃ : Subgroup G) (g : G) {h h' : G} (d : G) (hh : h' ∈ doubleCoset h ↑H₂ ↑H₃) : multiplicity H₁ H₂ H₃ g h' d = multiplicity H₁ H₂ H₃ g h d

Shimura's multiplicity depends on its second input only through its double coset, without any finiteness or Hecke-triple hypothesis.

theorem DoubleCoset.multiplicity_doubleCoset_congr_first_of_comm {G : Type u_1} [Group G] (H : Subgroup G) (hcomm : ∀ (a b d : G), multiplicity H H H a b d = multiplicity H H H b a d) {g g' : G} (h d : G) (hg : g' ∈ doubleCoset g ↑H ↑H) : multiplicity H H H g' h d = multiplicity H H H g h d

If the multiplicity is symmetric in its two inputs, it depends on its first input only through its double coset as well.