Documentation

TauCeti.RepresentationTheory.Induction.Mackey.Irreducible

The Mackey irreducibility criterion #

Let H be a subgroup of a finite group G and let A be a finite-dimensional representation of H over an algebraically closed field in which |G| is invertible. The intertwining-number formula TauCeti.finrank_hom_indFDRep_mackey_erase reads

dim End_G(Ind_H^G A) = dim End_H A + ∑_{HsH ≠ H} dim Hom_{H ⊓ sHs⁻¹}(Res A, {}^s A),

a sum of natural numbers. Over an algebraically closed field in which |G| is invertible a finite-dimensional representation is irreducible exactly when its endomorphism algebra is a line (Mathlib's FDRep.simple_iff_end_is_rank_one), so the left-hand side is 1 exactly when the first summand is 1 and every other summand is 0. That reading is the Mackey irreducibility criterion: Ind_H^G A is irreducible if and only if A is irreducible and, for every double coset HsH other than H itself, the two restrictions Res_{H ⊓ sHs⁻¹} A and Res_{H ⊓ sHs⁻¹} ({}^s A) are disjoint, that is, have no nonzero intertwiner. Disjointness is named here as TauCeti.MackeyDisjoint, and both forms of the criterion are stated through it.

The criterion comes in two forms. The primary one, TauCeti.simple_indFDRep_iff_doubleCoset, quantifies over the double cosets H \ G / H and reads each Mackey term at the fixed representative Quotient.out. The elementwise form, TauCeti.simple_indFDRep_iff, quantifies over the group elements s ∉ H instead.

Main definitions #

Main statements #

Implementation notes #

TauCeti.MackeyDisjoint is stated as Subsingleton of the intertwining space; the intertwining-number formula produces the dimension of that space instead, and TauCeti.mackeyDisjoint_iff_finrank_eq_zero is the bridge between the two readings, along which the double-coset criterion is proved. That bridge is deliberately not a simp lemma: the named predicate is the form the criteria are stated in and the form its own API (TauCeti.mackeyDisjoint_mul_left_mul_right_iff) applies to, so unfolding it to a dimension on sight would be the wrong normal form.

The step in those proofs that the arithmetic does not hand over for free is that dim End_H A cannot be 0: a representation with no nonzero endomorphism is a zero object, and then every term of the sum vanishes too, so the total could not be 1. That is what the two private helpers of the ZeroObject section below record.

Passing between the two forms of the criterion needs the Mackey term to be constant on a double coset, which is TauCeti.finrank_hom_res_mackeyToH_mul_left_mul_right, proved with the formula it belongs to; TauCeti.mackeyDisjoint_mul_left_mul_right_iff is its reading through the predicate.

The dimension formula follows from FDRep.indHomMackeyLinearEquiv and holds over every field. The criteria require only [NeZero (Nat.card G : k)], the Maschke hypothesis used by Mathlib's FDRep.simple_iff_end_is_rank_one, rather than a characteristic-zero assumption. TauCeti.MackeyDisjoint and its API hold over any field.

For a normal subgroup the Mackey subgroup is all of H. Restricting along TauCeti.mackeySubgroupNormalEquiv shows that the corresponding Mackey term and Hom_H(A, {}^s A) have equal dimensions, and TauCeti.simple_indFDRep_iff_of_normal gives the resulting normal-subgroup corollary. This is the form used by Clifford theory.

References #

source
def TauCeti.MackeyDisjoint {k G : Type u} [Field k] [Group G] {H : Subgroup G} (A : FDRep k ↥H) (s : G) :
Prop

Mackey disjointness at s: the restrictions of A and of its conjugate {}^s A to the Mackey subgroup H ⊓ sHs⁻¹ admit no nonzero intertwiner. The conjugation and the restriction of {}^s A are packaged into the single homomorphism TauCeti.mackeyToH.

This is the condition the Mackey irreducibility criterion imposes on every double coset other than H itself.

Equations
Instances For
    source
    theorem TauCeti.mackeyDisjoint_iff_subsingleton {k G : Type u} [Field k] [Group G] {H : Subgroup G} (A : FDRep k ↥H) (s : G) :
    MackeyDisjoint A s ↔ Subsingleton (((mackeySubgroup s H H).subgroupOf H).resFDRep A ⟶ (Action.res (FGModuleCat k) (mackeyToH s H H)).obj A)

    Mackey disjointness unfolded. The body of TauCeti.MackeyDisjoint is not exposed, so this is how a consumer reads the definition.

    source
    theorem TauCeti.MackeyDisjoint.eq_zero {k G : Type u} [Field k] [Group G] {H : Subgroup G} {A : FDRep k ↥H} {s : G} (h : MackeyDisjoint A s) (φ : ((mackeySubgroup s H H).subgroupOf H).resFDRep A ⟶ (Action.res (FGModuleCat k) (mackeyToH s H H)).obj A) :
    φ = 0

    An intertwiner between the two restrictions of a Mackey disjoint pair is zero.

    source
    theorem TauCeti.mackeyDisjoint_of_forall_eq_zero {k G : Type u} [Field k] [Group G] {H : Subgroup G} {A : FDRep k ↥H} {s : G} (h : ∀ (φ : ((mackeySubgroup s H H).subgroupOf H).resFDRep A ⟶ (Action.res (FGModuleCat k) (mackeyToH s H H)).obj A), φ = 0) :
    MackeyDisjoint A s

    Mackey disjointness holds as soon as every intertwiner between the two restrictions is zero.

    source
    theorem TauCeti.mackeyDisjoint_iff_finrank_eq_zero {k G : Type u} [Field k] [Group G] {H : Subgroup G} (A : FDRep k ↥H) (s : G) :
    MackeyDisjoint A s ↔ Module.finrank k (((mackeySubgroup s H H).subgroupOf H).resFDRep A ⟶ (Action.res (FGModuleCat k) (mackeyToH s H H)).obj A) = 0

    Mackey disjointness read as the vanishing of a dimension, which is the shape in which the intertwining-number formula produces it.

    source
    theorem TauCeti.mackeyDisjoint_mul_left_mul_right_iff {k G : Type u} [Field k] [Group G] {H : Subgroup G} (A : FDRep k ↥H) {h₁ h₂ : G} (hh₁ : h₁ ∈ H) (hh₂ : h₂ ∈ H) (s : G) :
    MackeyDisjoint A (h₁ * s * h₂) ↔ MackeyDisjoint A s

    Mackey disjointness depends only on the double coset: it holds at h₁ s h₂ with h₁, h₂ ∈ H exactly when it holds at s. This is the predicate form of TauCeti.finrank_hom_res_mackeyToH_mul_left_mul_right, and is what moves the criterion between its double-coset and its elementwise reading.

    source
    theorem TauCeti.mackeyDisjoint_iff_isEmpty_iso_of_normal {k G : Type u} [Field k] [Group G] {H : Subgroup G} [H.Normal] (A : FDRep k ↥H) [CategoryTheory.Simple A] (s : G) :
    MackeyDisjoint A s ↔ IsEmpty (conjNormalFDRep s A ≅ A)

    For a normal subgroup and an irreducible A, Mackey disjointness at s says exactly that the conjugate {}^s A is not isomorphic to A.

    source
    theorem TauCeti.simple_indFDRep_iff_doubleCoset {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} (A : FDRep k ↥H) :
    CategoryTheory.Simple (indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ (D : DoubleCoset.Quotient ↑H ↑H), D ≠ DoubleCoset.mk H H 1 → MackeyDisjoint A (Quotient.out D)

    The Mackey irreducibility criterion. The representation induced from A is irreducible exactly when A is irreducible and every double coset HsH other than H itself, read at its chosen representative, is Mackey disjoint.

    source
    theorem TauCeti.simple_indFDRep_iff {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} (A : FDRep k ↥H) :
    CategoryTheory.Simple (indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ s ∉ H, MackeyDisjoint A s

    The Mackey irreducibility criterion, elementwise. The disjointness condition of TauCeti.simple_indFDRep_iff_doubleCoset may equally be asked of every element s ∉ H rather than of one chosen representative of every non-identity double coset.

    source
    theorem TauCeti.simple_indFDRep_iff_of_normal {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} [H.Normal] (A : FDRep k ↥H) :
    CategoryTheory.Simple (indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ s ∉ H, IsEmpty (conjNormalFDRep s A ≅ A)

    The Mackey irreducibility criterion for a normal subgroup. If H ◁ G, then the representation induced from A is irreducible exactly when A is irreducible and none of its conjugates {}^s A, for s ∉ H, is isomorphic to A.