Moving the base point of a decomposition quotient

DoubleCoset.DecompQuotient Γ₁ Γ₂ g is Γ₁ ⧸ (gΓ₂g⁻¹).subgroupOf Γ₁, so it depends on g only through the conjugate gΓ₂g⁻¹. The conjugation facts themselves are general subgroup theory and live in TauCeti.GroupTheory.DoubleCoset.Basic (conjAct_smul_mul_right_of_mem_normalizer and the two subgroupOf_… lemmas); this file turns them into equivalences of the quotients:

• moving the base point on the left by anything normalizing Γ₁ conjugates the stabilizer, hence gives Γ₁/Stab(hg) ≃ Γ₁/Stab(g);
• moving it on the right by anything normalizing Γ₂ changes the stabilizer not at all, so the two-sided move reduces to the left one.

Ported from the AINTLIB LeanModularForms project, LeanModularForms/HeckeRIngs/AbstractHeckeRing/StabConjugation.lean (Chris Birkbeck). The source states these for a bundled HeckePair and for g in the ambient submonoid Δ; neither is used by the arguments, so they are stated here for arbitrary subgroups, an arbitrary g : G, and multipliers taken from the normalizers.

Main results

• DoubleCoset.decompQuotientEquivMulLeft, DoubleCoset.decompQuotientEquivMulLeftRight: the equivalences of decomposition quotients induced by moving the base point.
• DoubleCoset.decompQuotientEquivMulLeft_mk, DoubleCoset.decompQuotientEquivMulLeftRight_mk: what each does to a representative.

noncomputable def DoubleCoset.decompQuotientEquivMulLeft {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) (h : ↥(Subgroup.normalizer ↑Γ₁)) : DecompQuotient Γ₁ Γ₂ (↑h * g) ≃ DecompQuotient Γ₁ Γ₂ g

Moving the base point on the left by anything normalizing Γ₁ is an equivalence of decomposition quotients, Γ₁/Stab(hg) ≃ Γ₁/Stab(g), induced by σ ↦ h⁻¹σh.

Well-definedness is subgroupOf_conjAct_smul_mul_left_of_mem_normalizer: the two stabilizers differ by that conjugation, so it carries one coset relation to the other.

Equations

• DoubleCoset.decompQuotientEquivMulLeft Γ₁ Γ₂ g h = (Subgroup.quotientEquivOfEq ⋯).trans (Quotient.congr (MulEquiv.symm (Γ₁.normalizerMonoidHom h)).toEquiv ⋯)

theorem DoubleCoset.decompQuotientEquivMulLeft_mk {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) (h : ↥(Subgroup.normalizer ↑Γ₁)) (x : ↥Γ₁) : (decompQuotientEquivMulLeft Γ₁ Γ₂ g h) ↑x = ↑((MulEquiv.symm (Γ₁.normalizerMonoidHom h)) x)

What decompQuotientEquivMulLeft does to a representative: it conjugates by h⁻¹.

Deliberately not @[simp]. The left-hand side is not in simp normal form and cannot be made so: QuotientGroup.mk's implicit subgroup argument comes from the type index DecompQuotient Γ₁ Γ₂ (↑h * g), and simp rewrites ConjAct.toConjAct (↑h * g) inside it to ConjAct.toConjAct ↑h * ConjAct.toConjAct g via ConjAct.toConjAct_mul. scripts/lint-env.sh reports exactly that as a simpNF violation. Rewrite with this lemma by name.

noncomputable def DoubleCoset.decompQuotientEquivMulLeftRight {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) (h : ↥(Subgroup.normalizer ↑Γ₁)) {k : G} (hk : k ∈ Subgroup.normalizer ↑Γ₂) : DecompQuotient Γ₁ Γ₂ (↑h * g * k) ≃ DecompQuotient Γ₁ Γ₂ g

Moving the base point on both sides — on the left by anything normalizing Γ₁, on the right by anything normalizing Γ₂ — is again an equivalence of decomposition quotients. Right multiplication contributes nothing (subgroupOf_conjAct_smul_mul_right_of_mem_normalizer), so this is decompQuotientEquivMulLeft after re-associating.

Equations

• DoubleCoset.decompQuotientEquivMulLeftRight Γ₁ Γ₂ g h hk = (Subgroup.quotientEquivOfEq ⋯).trans ((DoubleCoset.decompQuotientEquivMulLeft Γ₁ Γ₂ (g * k) h).trans (Subgroup.quotientEquivOfEq ⋯))

theorem DoubleCoset.decompQuotientEquivMulLeftRight_mk {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) (h : ↥(Subgroup.normalizer ↑Γ₁)) {k : G} (hk : k ∈ Subgroup.normalizer ↑Γ₂) (x : ↥Γ₁) : (decompQuotientEquivMulLeftRight Γ₁ Γ₂ g h hk) ↑x = ↑((MulEquiv.symm (Γ₁.normalizerMonoidHom h)) x)

What decompQuotientEquivMulLeftRight does to a representative. Not @[simp], for the same reason as decompQuotientEquivMulLeft_mk.

theorem TauCeti.finite_decompQuotient_inv_of_mem_doubleCoset {G : Type u_1} [Group G] {H K : Subgroup G} {g δ : G} [Finite (DoubleCoset.DecompQuotient K H g⁻¹)] (hδ : δ ∈ DoubleCoset.doubleCoset g ↑H ↑K) : Finite (DoubleCoset.DecompQuotient K H δ⁻¹)

Finiteness of the right-coset decomposition is independent of the representative chosen in a double coset.