Restriction to a normal subgroup preserves semisimplicity

Let N be a normal subgroup of G and let ρ be an irreducible representation of G. Cutting the group down to N does not preserve irreducibility, but it does preserve semisimplicity: the restriction of ρ to N is a sum of irreducibles, as soon as there is a minimal nonzero N-stable subspace to start from — which for a finite-dimensional ρ there always is.

The mechanism is a single observation. If U ⊆ V is stable under N, then so is ρ g '' U for every g : G, because ρ n (ρ g u) = ρ g (ρ (g⁻¹ n g) u) and g⁻¹ n g lies in N by normality. Translation by ρ g therefore acts on the lattice of N-subrepresentations (TauCeti.Representation.conjSubrep), by order isomorphisms (TauCeti.Representation.conjSubrepOrderIso), so it preserves atoms; and it identifies U with its translate not as representations of N on the nose but after twisting the action of N by conjugation (TauCeti.Representation.conjSubrepEquiv). That twist is exactly the conjugation action TauCeti.conjNormalRep on representations of N built in TauCeti/RepresentationTheory/Induction/Conjugate.lean, whose stabilisers are the inertia groups of TauCeti/RepresentationTheory/Induction/Inertia.lean.

Two theorems come out of it. First, the translates of a single nonzero N-subrepresentation span: their sum is stable under all of G, so irreducibility of ρ forces it to be everything (TauCeti.Representation.iSup_conjSubrep_eq_top). Second, if the subrepresentation being translated is minimal, the span exhibits V as a sum of simple N-submodules, so the restriction to N is semisimple (TauCeti.Representation.isSemisimpleRepresentation_comp_subtype_of_isAtom) -- and this needs no invertibility of Nat.card N, so it is not Maschke's theorem in disguise.

Throughout, an irreducible constituent is presented as an atom of the lattice of N-subrepresentations rather than as an abstract irreducible representation of N mapping in. That is what keeps the argument free of finiteness hypotheses: no dimension count and no counting of conjugates enters. Finite-dimensionality is used only to produce an atom, in TauCeti.Representation.isSemisimpleRepresentation_comp_subtype.

Main definitions

• TauCeti.Representation.conjSubrep: the translate ρ g '' U of an N-subrepresentation U.
• TauCeti.Representation.conjSubrepOrderIso: translation as an order isomorphism of the lattice of N-subrepresentations.
• TauCeti.Representation.conjSubrepEquiv: translation by ρ g as an equivalence from U, with its action of N twisted by conjugation, onto the translate.

Main statements

• TauCeti.Representation.iSup_conjSubrep_eq_top: the translates of a nonzero N-subrepresentation of an irreducible representation span.
• TauCeti.Representation.iSup_asSubmodule_conjSubrep_eq_top: the same statement read in the lattice of k[N]-submodules of the restriction.
• Representation.apply_eq_smul_of_ne_bot: if N acts on one nonzero N-subrepresentation through conjugation-invariant scalars, it acts on everything through them.
• TauCeti.Representation.isSemisimpleRepresentation_comp_subtype_of_isAtom: if some N-subrepresentation of an irreducible representation IsAtom, then the restriction to N is semisimple.
• TauCeti.Representation.isSemisimpleRepresentation_comp_subtype: the same conclusion for a finite-dimensional irreducible representation, where such an atom is automatic (Representation.exists_isAtom).

Implementation notes

The three constructions above are opaque: their bodies are not exported, and everything downstream goes through their characteristic lemmas toSubmodule_conjSubrep, conjSubrepOrderIso_apply, conjSubrepOrderIso_symm_apply, coe_conjSubrepEquiv_apply and coe_conjSubrepEquiv_symm_apply instead. The first four are proved by (rfl) rather than by rfl: a bare rfl body asks in addition that the equation stay true by rfl outside this file, which for an unexposed definition it is not. The parenthesized form checks the proof here, where the bodies are visible, and exports only the statement.

References

This file supplies item (iii) of the prerequisite of Layer 5 (Clifford theory over a normal subgroup) of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md — "restriction along a subgroup preserves semisimplicity" — in the normal-subgroup case Clifford theory uses, as TauCeti.Representation.isSemisimpleRepresentation_comp_subtype. It stops there: nothing below mentions a decomposition, an isotypic component, a multiplicity or a G-orbit of constituents. What the file does leave in place is the translation machinery the Clifford's theorem milestone runs on, since it is the same machinery the semisimplicity statement is proved from; the single-orbit half of that milestone is TauCeti/RepresentationTheory/Induction/Clifford/Orbit/Basic.lean.

The mathematics is the classical argument of C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §49.

def TauCeti.Representation.conjSubrep {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : Subrepresentation (MonoidHom.comp ρ N.subtype)

The translate of an N-subrepresentation σ by g : G: the image of σ under ρ g, again stable under N because N is normal.

For g ∈ N this is σ itself; in general it is a possibly different subspace, carrying the representation of N obtained from σ by conjugating with g (conjSubrepEquiv).

The carrier is σ.toSubmodule.map (ρ g) (toSubmodule_conjSubrep), which is how everything below reasons about a translate: through the submodule lattice rather than through this definition.

@[simp]

theorem TauCeti.Representation.toSubmodule_conjSubrep {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : (conjSubrep ρ g σ).toSubmodule = Submodule.map (ρ g) σ.toSubmodule

@[simp]

theorem TauCeti.Representation.mem_conjSubrep_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {g : G} {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} {v : V} : v ∈ conjSubrep ρ g σ ↔ (ρ g⁻¹) v ∈ σ

@[simp]

theorem TauCeti.Representation.conjSubrep_eq_self_of_mem {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {g : G} (hg : g ∈ N) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : conjSubrep ρ g σ = σ

Translating by an element of N itself does nothing: an N-subrepresentation is already stable under N, and under N-inverses.

theorem TauCeti.Representation.conjSubrep_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : conjSubrep ρ 1 σ = σ

Translation is an action: translating by 1 does nothing. Not a simp lemma, since conjSubrep_eq_self_of_mem already rewrites this way once it discharges (1 : G) ∈ N.

@[simp]

theorem TauCeti.Representation.conjSubrep_conjSubrep {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g h : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : conjSubrep ρ g (conjSubrep ρ h σ) = conjSubrep ρ (g * h) σ

@[simp]

theorem TauCeti.Representation.conjSubrep_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) : conjSubrep ρ g ⊥ = ⊥

@[simp]

theorem TauCeti.Representation.conjSubrep_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) : conjSubrep ρ g ⊤ = ⊤

def TauCeti.Representation.conjSubrepOrderIso {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) : Subrepresentation (MonoidHom.comp ρ N.subtype) ≃o Subrepresentation (MonoidHom.comp ρ N.subtype)

Translation by ρ g is an order isomorphism of the lattice of N-subrepresentations, with inverse translation by ρ g⁻¹. In particular it takes atoms to atoms (isAtom_conjSubrep_iff).

@[simp]

theorem TauCeti.Representation.conjSubrepOrderIso_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : (conjSubrepOrderIso ρ g) σ = conjSubrep ρ g σ

@[simp]

theorem TauCeti.Representation.conjSubrepOrderIso_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : (conjSubrepOrderIso ρ g).symm σ = conjSubrep ρ g⁻¹ σ

@[simp]

theorem TauCeti.Representation.isAtom_conjSubrep_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {g : G} {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} : IsAtom (conjSubrep ρ g σ) ↔ IsAtom σ

noncomputable def TauCeti.Representation.conjSubrepEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : Representation.Equiv (MonoidHom.comp σ.toRepresentation ↑(MulAut.conjNormal g⁻¹)) (conjSubrep ρ g σ).toRepresentation

Translation by ρ g identifies σ, with its action of N twisted by conjugation by g, with the translate conjSubrep ρ g σ.

The twist is unavoidable: the two subspaces are exchanged by ρ g, which does not commute with N but conjugates it. The twisted source is the conjugate representation TauCeti.conjNormalRep g of TauCeti/RepresentationTheory/Induction/Conjugate.lean, unbundled: it is (conjNormalRep g (Rep.of σ.toRepresentation)).ρ by TauCeti.conjNormalRep_ρ. It is written here as the plain composition rather than through Rep.of, which would need V to be an AddCommGroup where this section asks only for an AddCommMonoid. Read on isomorphism classes, this says that conjSubrep ρ g σ represents the image of the class of σ under the conjugation action of g on representations of N.

The underlying map is ρ g (coe_conjSubrepEquiv_apply), and its inverse is ρ g⁻¹ (coe_conjSubrepEquiv_symm_apply).

@[simp]

theorem TauCeti.Representation.coe_conjSubrepEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (u : ↥σ.toSubmodule) : ↑((conjSubrepEquiv ρ g σ) u) = (ρ g) ↑u

@[simp]

theorem TauCeti.Representation.coe_conjSubrepEquiv_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (v : ↥(conjSubrep ρ g σ).toSubmodule) : ↑((conjSubrepEquiv ρ g σ).symm v) = (ρ g⁻¹) ↑v

The inverse of conjSubrepEquiv is translation back by ρ g⁻¹.

theorem TauCeti.Representation.iSup_conjSubrep_eq_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : σ ≠ ⊥) : ⨆ (g : G), (conjSubrep ρ g σ).toSubmodule = ⊤

The translates of a nonzero N-subrepresentation of an irreducible representation span. Their sum is a subspace stable under every ρ h, hence a subrepresentation of ρ itself, and it is nonzero, so irreducibility leaves it no choice.

theorem TauCeti.Representation.iSup_asSubmodule_conjSubrep_eq_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : σ ≠ ⊥) : ⨆ (g : G), (conjSubrep ρ g σ).asSubmodule = ⊤

The translates of a nonzero N-subrepresentation of an irreducible representation span, as k[N]-submodules. This is TauCeti.Representation.iSup_conjSubrep_eq_top read in the lattice of k[N]-submodules of Representation.asModule (ρ.comp N.subtype) instead of the lattice of k-subspaces of V; the two lattices are exchanged by Subrepresentation.subrepresentationSubmoduleOrderIso, and this is the only place the exchange is performed.

theorem TauCeti.Representation.isSemisimpleRepresentation_comp_subtype_of_isAtom {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) : Representation.IsSemisimpleRepresentation (MonoidHom.comp ρ N.subtype)

Restriction to a normal subgroup is semisimple, from a minimal constituent. If an irreducible representation has a minimal nonzero N-stable subspace, then its restriction to N is semisimple: the translates of that subspace are again minimal and they span, so the restriction is a sum of simple N-submodules.

No hypothesis relating Nat.card N to the characteristic is needed; irreducibility of the ambient representation does the work Maschke's theorem would otherwise do.

theorem TauCeti.Representation.isSemisimpleRepresentation_comp_subtype {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] : Representation.IsSemisimpleRepresentation (MonoidHom.comp ρ N.subtype)

Restriction to a normal subgroup preserves semisimplicity. The restriction to a normal subgroup of a finite-dimensional irreducible representation is semisimple.

The next lemma is stated for a Mathlib Representation, so it lives in that type's root namespace, where dot notation on ρ finds it.

theorem Representation.apply_eq_smul_of_ne_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : σ ≠ ⊥) (c : ↥N → k) (hc : ∀ (n : ↥N), ∀ v ∈ σ, (ρ ↑n) v = c n • v) (hconj : ∀ (g : G) (n : ↥N), c ((MulAut.conjNormal g) n) = c n) (n : ↥N) (v : V) : (ρ ↑n) v = c n • v

Scalars on one constituent are scalars everywhere. Suppose that N acts on a nonzero N-subrepresentation σ of an irreducible ρ through scalars c : N → k, and that c is invariant under conjugation by G. Then N acts on all of V through the same scalars: the translates ρ g σ span V (TauCeti.Representation.iSup_conjSubrep_eq_top), and n acts on ρ g σ by c (g⁻¹ n g) = c n.