The Mackey subgroup

For subgroups H and K of a group G and an element s : G, the Mackey subgroup

mackeySubgroup s H K = K ⊓ sHs⁻¹

is the subgroup on which the summand of the Mackey decomposition attached to the double coset KsH lives: the conjugate representation {}^s A is a representation of sHs⁻¹, it is restricted along mackeySubgroup s H K ≤ sHs⁻¹ and then induced along mackeySubgroup s H K ≤ K. The two inclusions are pinned here as TauCeti.mackeyToConjH and TauCeti.mackeyToK; there is no second intersection with K.

The reason the Mackey subgroup is the right object is geometric. The group K acts on G ⧸ H by translation, and the stabilizer of the coset sH is exactly mackeySubgroup s H K (TauCeti.stabilizer_eq_mackeySubgroup_subgroupOf, resting on the description TauCeti.stabilizer_quotientGroup_mk of the stabilizer in G as the conjugate sHs⁻¹). The K-orbit of sH is the image of the double coset KsH (TauCeti.preimage_orbit_eq_doubleCoset), so the partition of G ⧸ H into K-orbits is the partition of G into double cosets, and orbit-stabilizer turns each orbit into an index: |K·sH| = [K : K ⊓ sHs⁻¹]. This is the combinatorial content of the Mackey decomposition, and it yields the classical double-coset size formula |KsH| · |K ⊓ sHs⁻¹| = |K| · |H| (TauCeti.card_doubleCoset_mul_card_mackeySubgroup). The two facts about the translation action that this rests on are generic group theory and live with the topics they belong to: the stabilizer description in TauCeti.GroupTheory.QuotientGroup.Basic and the identification of a double coset with an orbit in TauCeti.GroupTheory.DoubleCoset.Orbits.

Because the Mackey decomposition is indexed by double cosets while its summands are built from a chosen representative, the dependence on the representative has to be pinned too: replacing s by k * s * h with k ∈ K and h ∈ H conjugates the Mackey subgroup by k (TauCeti.mackeySubgroup_conj), so the two subgroups are isomorphic (TauCeti.mackeySubgroupCongr) and in particular have the same index in K. Nothing here asserts a canonical representative-independent summand; that would need coherent conjugation equivalences of the representations themselves.

Everything in this file is a statement about subgroups of G, with no coefficients and no representations; it is placed with the induction files because mackeySubgroup is the roadmap-specific subgroup the induction and restriction of that layer run along.

Main definitions

• TauCeti.mackeySubgroup: the subgroup K ⊓ sHs⁻¹.
• TauCeti.mackeyToK, TauCeti.mackeyToConjH: the two inclusions of the Mackey subgroup, into K and into sHs⁻¹.
• TauCeti.mackeySubgroupCongr: the isomorphism between the Mackey subgroups of two representatives of one double coset, and TauCeti.mackeySubgroupOfCongr, the same isomorphism with both sides read as subgroups of K.
• TauCeti.mackeySubgroupSelfEquiv: the identification of the Mackey subgroup of a representative lying in H with H itself.
• TauCeti.mackeySubgroupNormalEquiv: for normal H, the same identification at every representative.

Main statements

• TauCeti.stabilizer_eq_mackeySubgroup_subgroupOf: the stabilizer of sH in K is the Mackey subgroup.
• TauCeti.mackeySubgroup_conj: changing the double-coset representative conjugates the Mackey subgroup.
• TauCeti.card_orbit_eq_relIndex: the K-orbit of sH has as many elements as the Mackey subgroup has index in K.
• TauCeti.relIndex_mackeySubgroup_conj: that index depends only on the double coset.
• TauCeti.card_doubleCoset_mul_card_mackeySubgroup: the double-coset size formula |KsH| · |K ⊓ sHs⁻¹| = |K| · |H|.
• TauCeti.card_doubleCoset_eq_card_mul_relIndex: the same formula as an index, |KsH| = |K| · [sHs⁻¹ : K ⊓ sHs⁻¹].
• TauCeti.stabilizer_smul_eq_mackeySubgroup_subgroupOf: the same stabilizer description for an arbitrary G-set, at a translate s • p.
• TauCeti.mackeySubgroup_eq_bot_or_conj_smul_le_of_prime_card: for H of prime order the Mackey subgroup is ⊥ unless the whole conjugate sHs⁻¹ lies in K.
• TauCeti.mackeySubgroup_self_eq_bot_or_conj_smul_eq_self_of_prime_card: at K = H that dichotomy reads: H meets each of its conjugates in ⊥ or in itself.
• TauCeti.exists_notMem_mackeySubgroup_eq_bot_of_prime_card_of_not_normal: a non-normal subgroup of prime order therefore has a conjugate meeting it trivially.

References

Layer 3 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, which asks to "name the subgroup mackeySubgroup s H K := K ⊓ (MulAut.conj s • H)" carrying the two homomorphisms mackeyToK and mackeyToConjH, and Layer 4, which asks for the invariance of the Mackey data "under replacing s by h₁ s h₂" as its own lemma. mackeySubgroup is pinned in the accompanying Suggested.lean.

• J.-P. Serre, Linear Representations of Finite Groups, Section 7.3.

def TauCeti.mackeySubgroup {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : Subgroup G

The Mackey subgroup K ⊓ sHs⁻¹: the subgroup carrying the summand of the Mackey decomposition attached to the double coset KsH.

It comes with the two inclusions TauCeti.mackeyToConjH into sHs⁻¹, along which the conjugate representation {}^s A is restricted, and TauCeti.mackeyToK into K, along which the result is induced.

Equations

• TauCeti.mackeySubgroup s H K = K ⊓ MulAut.conj s • H

theorem TauCeti.mackeySubgroup_def {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : mackeySubgroup s H K = K ⊓ MulAut.conj s • H

The Mackey subgroup unfolded: it is the intersection of K with the conjugate sHs⁻¹.

@[simp]

theorem TauCeti.mem_mackeySubgroup_iff {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} {x : G} : x ∈ mackeySubgroup s H K ↔ x ∈ K ∧ s⁻¹ * x * s ∈ H

theorem TauCeti.mackeySubgroup_le_right {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} : mackeySubgroup s H K ≤ K

The Mackey subgroup is contained in K, the second subgroup argument.

theorem TauCeti.mackeySubgroup_le_conj {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} : mackeySubgroup s H K ≤ MulAut.conj s • H

The Mackey subgroup is contained in the conjugate sHs⁻¹ of the first subgroup argument.

def TauCeti.mackeyToK {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : ↥(mackeySubgroup s H K) →* ↥K

The inclusion of the Mackey subgroup into K, along which the Mackey summand is induced.

Equations

• TauCeti.mackeyToK s H K = Subgroup.inclusion ⋯

def TauCeti.mackeyToConjH {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : ↥(mackeySubgroup s H K) →* ↥(MulAut.conj s • H)

The inclusion of the Mackey subgroup into sHs⁻¹, along which the conjugate representation {}^s A is restricted.

Equations

• TauCeti.mackeyToConjH s H K = Subgroup.inclusion ⋯

@[simp]

theorem TauCeti.coe_mackeyToK_apply {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} (x : ↥(mackeySubgroup s H K)) : ↑((mackeyToK s H K) x) = ↑x

@[simp]

theorem TauCeti.coe_mackeyToConjH_apply {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} (x : ↥(mackeySubgroup s H K)) : ↑((mackeyToConjH s H K) x) = ↑x

theorem TauCeti.mackeyToK_injective {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} : Function.Injective ⇑(mackeyToK s H K)

theorem TauCeti.mackeyToConjH_injective {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} : Function.Injective ⇑(mackeyToConjH s H K)

theorem TauCeti.mackeySubgroup_one {G : Type u_1} [Group G] (H K : Subgroup G) : mackeySubgroup 1 H K = K ⊓ H

@[simp]

theorem TauCeti.mackeySubgroup_of_mem {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} (hs : s ∈ H) : mackeySubgroup s H K = K ⊓ H

A representative lying in H gives back the plain intersection K ⊓ H.

theorem TauCeti.mackeySubgroup_subgroupOf_self_of_mem {G : Type u_1} [Group G] {s : G} {H : Subgroup G} (hs : s ∈ H) : (mackeySubgroup s H H).subgroupOf H = ⊤

A representative lying in H has all of H for its Mackey subgroup, so the Mackey subgroup sits inside H as the top subgroup.

noncomputable def TauCeti.mackeySubgroupSelfEquiv {G : Type u_1} [Group G] {s : G} {H : Subgroup G} (hs : s ∈ H) : ↥((mackeySubgroup s H H).subgroupOf H) ≃* ↥H

The Mackey subgroup of a representative lying in H, identified with H itself.

Equations

• TauCeti.mackeySubgroupSelfEquiv hs = (MulEquiv.subgroupCongr ⋯).trans Subgroup.topEquiv

@[simp]

theorem TauCeti.coe_mackeySubgroupSelfEquiv_apply {G : Type u_1} [Group G] {s : G} {H : Subgroup G} (hs : s ∈ H) (y : ↥((mackeySubgroup s H H).subgroupOf H)) : (mackeySubgroupSelfEquiv hs) y = ↑y

@[simp]

theorem TauCeti.mackeySubgroup_of_normal {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} [H.Normal] : mackeySubgroup s H K = K ⊓ H

For a normal H the Mackey subgroup does not depend on the representative at all: it is K ⊓ H for every s. This is why Clifford theory over a normal subgroup only ever sees the one intersection.

noncomputable def TauCeti.mackeySubgroupNormalEquiv {G : Type u_1} [Group G] {H : Subgroup G} (s : G) [H.Normal] : ↥((mackeySubgroup s H H).subgroupOf H) ≃* ↥H

For a normal subgroup, the Mackey subgroup at every representative is the whole subgroup. This is the group equivalence used to read a Mackey intertwining space over H itself.

Equations

• TauCeti.mackeySubgroupNormalEquiv s = (MulEquiv.subgroupCongr ⋯).trans Subgroup.topEquiv

@[simp]

theorem TauCeti.coe_mackeySubgroupNormalEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} (s : G) [H.Normal] (y : ↥((mackeySubgroup s H H).subgroupOf H)) : (mackeySubgroupNormalEquiv s) y = ↑y

@[simp]

theorem TauCeti.coe_mackeySubgroupNormalEquiv {G : Type u_1} [Group G] {H : Subgroup G} (s : G) [H.Normal] : ↑(mackeySubgroupNormalEquiv s) = ((mackeySubgroup s H H).subgroupOf H).subtype

The homomorphism underlying mackeySubgroupNormalEquiv is the canonical inclusion into H.

theorem TauCeti.mackeySubgroup_top_left {G : Type u_1} [Group G] (s : G) (K : Subgroup G) : mackeySubgroup s ⊤ K = K

Inducing from the whole group leaves nothing to intersect: the Mackey subgroup is K.

@[simp]

theorem TauCeti.mackeySubgroup_top_right {G : Type u_1} [Group G] (s : G) (H : Subgroup G) : mackeySubgroup s H ⊤ = MulAut.conj s • H

Restricting to the whole group leaves the bare conjugate sHs⁻¹.

theorem TauCeti.mackeySubgroup_conj {G : Type u_1} [Group G] {s : G} {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) : mackeySubgroup (k * s * h) H K = MulAut.conj k • mackeySubgroup s H K

Changing the representative of a double coset conjugates the Mackey subgroup. Replacing s by k * s * h, with k ∈ K and h ∈ H, leaves the double coset KsH unchanged and replaces K ⊓ sHs⁻¹ by its conjugate k (K ⊓ sHs⁻¹) k⁻¹.

def TauCeti.mackeySubgroupCongr {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) : ↥(mackeySubgroup s H K) ≃* ↥(mackeySubgroup (k * s * h) H K)

The Mackey subgroups of two representatives of one double coset are isomorphic, by conjugation. This is the invariance that makes the index of the Mackey subgroup, and hence the dimension of the Mackey summand, a function of the double coset alone.

Equations

• TauCeti.mackeySubgroupCongr hk hh s = (Subgroup.equivSMul (MulAut.conj k) (TauCeti.mackeySubgroup s H K)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.coe_mackeySubgroupCongr_apply {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) (x : ↥(mackeySubgroup s H K)) : ↑((mackeySubgroupCongr hk hh s) x) = k * ↑x * k⁻¹

@[simp]

theorem TauCeti.coe_mackeySubgroupCongr_symm_apply {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) (y : ↥(mackeySubgroup (k * s * h) H K)) : ↑((mackeySubgroupCongr hk hh s).symm y) = k⁻¹ * ↑y * k

def TauCeti.mackeySubgroupOfCongr {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) : ↥((mackeySubgroup s H K).subgroupOf K) ≃* ↥((mackeySubgroup (k * s * h) H K).subgroupOf K)

The same isomorphism as TauCeti.mackeySubgroupCongr, with both Mackey subgroups read inside K along TauCeti.mackeySubgroup_le_right. That is where the Mackey summands live, so this is the form in which a change of representative is transported.

Equations

• TauCeti.mackeySubgroupOfCongr hk hh s = ((Subgroup.subgroupOfEquivOfLe ⋯).trans (TauCeti.mackeySubgroupCongr hk hh s)).trans (Subgroup.subgroupOfEquivOfLe ⋯).symm

@[simp]

theorem TauCeti.coe_mackeySubgroupOfCongr_apply {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) (y : ↥((mackeySubgroup s H K).subgroupOf K)) : ↑↑((mackeySubgroupOfCongr hk hh s) y) = k * ↑↑y * k⁻¹

@[simp]

theorem TauCeti.coe_mackeySubgroupOfCongr_symm_apply {G : Type u_1} [Group G] {H K : Subgroup G} {k h : G} (hk : k ∈ K) (hh : h ∈ H) (s : G) (y : ↥((mackeySubgroup (k * s * h) H K).subgroupOf K)) : ↑↑((mackeySubgroupOfCongr hk hh s).symm y) = k⁻¹ * ↑↑y * k

@[simp]

theorem TauCeti.stabilizer_eq_mackeySubgroup_subgroupOf {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : MulAction.stabilizer ↥K ↑s = (mackeySubgroup s H K).subgroupOf K

The Mackey subgroup is a stabilizer: it is the stabilizer of the coset sH for the translation action of K on G ⧸ H, read as a subgroup of K.

theorem TauCeti.card_orbit_eq_relIndex {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : Nat.card ↑(MulAction.orbit ↥K ↑s) = (mackeySubgroup s H K).relIndex K

Orbit-stabilizer for the Mackey subgroup: the K-orbit of the coset sH has as many elements as the Mackey subgroup has index in K.

instance TauCeti.instIsFiniteRelIndexMackeySubgroup {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) [H.FiniteIndex] : (mackeySubgroup s H K).IsFiniteRelIndex K

If H has finite index in G then the Mackey subgroup has finite index in K, so the Mackey summand attached to s is induced along a finite-index inclusion.

theorem TauCeti.card_doubleCoset_mul_card_mackeySubgroup {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : Nat.card ↑(DoubleCoset.doubleCoset s ↑K ↑H) * Nat.card ↥(mackeySubgroup s H K) = Nat.card ↥K * Nat.card ↥H

The double-coset size formula: |KsH| · |K ⊓ sHs⁻¹| = |K| · |H|.

With Nat.card's convention that an infinite type has cardinality 0, this holds without any finiteness hypothesis.

theorem TauCeti.card_doubleCoset_eq_card_mul_relIndex {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) [Finite ↥H] : Nat.card ↑(DoubleCoset.doubleCoset s ↑K ↑H) = Nat.card ↥K * K.relIndex (MulAut.conj s • H)

The double-coset size formula, as an index: |KsH| = |K| · [sHs⁻¹ : K ⊓ sHs⁻¹].

Finiteness of H makes the conjugate subgroup sHs⁻¹ finite, so the relative index [sHs⁻¹ : K ⊓ sHs⁻¹] is a finite count of cosets.

theorem TauCeti.relIndex_mackeySubgroup_conj {G : Type u_1} [Group G] {s k h : G} {H K : Subgroup G} (hk : k ∈ K) (hh : h ∈ H) : (mackeySubgroup (k * s * h) H K).relIndex K = (mackeySubgroup s H K).relIndex K

The index of the Mackey subgroup in K depends only on the double coset KsH, not on the representative s chosen inside it: the two subgroups are conjugate by an element of K (TauCeti.mackeySubgroup_conj), and conjugation fixes K, so it preserves the relative index.

theorem TauCeti.stabilizer_smul_eq_mackeySubgroup_subgroupOf {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : G) (Γ : Subgroup G) (p : α) : MulAction.stabilizer (↥Γ) (s • p) = (mackeySubgroup s (MulAction.stabilizer G p) Γ).subgroupOf Γ

The Mackey subgroup is a stabilizer, for an arbitrary action. For a point p of any G-set and s : G, the stabilizer of the translate s • p in a subgroup Γ is the Mackey subgroup of Γ and stabilizer G p at s, read inside Γ.

stabilizer_eq_mackeySubgroup_subgroupOf above is the same statement for the translation action of Γ on G ⧸ H. Neither implies the other: that one is stated for Mathlib's mulLeftCosetsCompSubtypeVal action on cosets, this one for the restriction of scalars Subgroup.instMulAction, and MulAction ↥Γ (G ⧸ H) has both. The general form is the one a sum over the points of an arbitrary G-set needs.

theorem TauCeti.mackeySubgroup_eq_bot_or_conj_smul_le_of_prime_card {G : Type u_1} [Group G] {H : Subgroup G} (hp : Nat.Prime (Nat.card ↥H)) (s : G) (K : Subgroup G) : mackeySubgroup s H K = ⊥ ∨ MulAut.conj s • H ≤ K

A subgroup of prime order either meets K trivially after conjugation, or is carried inside K altogether. The Mackey subgroup K ⊓ sHs⁻¹ sits inside the conjugate sHs⁻¹, a group of prime order Nat.card H, so read inside sHs⁻¹ it is ⊥ or ⊤.

theorem TauCeti.mackeySubgroup_self_eq_bot_or_conj_smul_eq_self_of_prime_card {G : Type u_1} [Group G] {H : Subgroup G} (hp : Nat.Prime (Nat.card ↥H)) (s : G) : mackeySubgroup s H H = ⊥ ∨ MulAut.conj s • H = H

A subgroup of prime order meets each of its conjugates in ⊥ or in itself. This is TauCeti.mackeySubgroup_eq_bot_or_conj_smul_le_of_prime_card at K = H: the containment sHs⁻¹ ≤ H it produces is an equality because conjugate subgroups have the same finite order.

theorem TauCeti.exists_notMem_mackeySubgroup_eq_bot_of_prime_card_of_not_normal {G : Type u_1} [Group G] {H : Subgroup G} (hp : Nat.Prime (Nat.card ↥H)) (hH : ¬H.Normal) : ∃ s ∉ H, mackeySubgroup s H H = ⊥

A non-normal subgroup of prime order has a conjugate meeting it trivially. If every conjugate of H were H itself, H would be normal; so some conjugate is different, and by TauCeti.mackeySubgroup_self_eq_bot_or_conj_smul_eq_self_of_prime_card it then meets H trivially. The conjugating element lies outside H, since conjugating by an element of H preserves H.