Restriction of representations

This file collects restriction infrastructure shared by the induction files: how the restriction functors Rep.resFunctor and Action.res behave under composing and inverting the homomorphism restricted along, and, for a subgroup S of a group G, the restriction of a finitely generated representation of G to S together with its character and the class function that character carries (Subgroup.comap_subtype_ofFDRep). Restricting along a surjective homomorphism changes nothing essential: it identifies the lattices of invariant subspaces, and hence preserves irreducibility. In particular a representation trivial on a normal subgroup is irreducible exactly when the representation of the quotient group it factors through is, which makes simplicity of that quotient representation independent of the normal subgroup chosen.

FDRep k G is by definition Action (FGModuleCat k) G, so Mathlib's Action.res along S.subtype is the restriction functor FDRep k G ⥤ FDRep k S; nothing has to be built. Accordingly Subgroup.resFDRep is a reducible abbreviation for that functor on objects, exactly as Mathlib's Rep.res is one for Rep.resFunctor on objects, and everything functorial — restriction of an intertwiner, the functor laws, naturality — is used straight from Action.res (FGModuleCat k) S.subtype and its @[simps] lemmas (Action.res_obj_V, Action.res_obj_ρ, Action.res_map_hom) rather than restated here.

Main definitions

• MulEquiv.resFunctorEquiv: restriction along a monoid isomorphism, as an equivalence of categories.
• MonoidHom.resSubrepresentationOrderIso: restriction along a surjective monoid homomorphism identifies the lattices of invariant subspaces.
• Subgroup.resFDRep: restriction of a finitely generated representation to a subgroup.

Main statements

• MonoidHom.resFunctor_comp, MonoidHom.actionRes_comp: restriction along a composite is restriction twice over.
• MonoidHom.finrank_hom_actionRes_of_surjective: restriction along a surjective monoid homomorphism preserves the dimension of an intertwining space.
• MonoidHom.isIrreducible_comp_surjective_iff: restriction along a surjective monoid homomorphism preserves irreducibility, with MulEquiv.isIrreducible_comp_equiv_iff as the isomorphism case.
• Representation.isIrreducible_ofQuotient_iff, Rep.simple_ofQuotient_iff: a representation trivial on a normal subgroup S is irreducible, respectively simple, exactly when the representation of G ⧸ S it factors through is.

Implementation notes

The abbreviation is over a ring, matching Mathlib's FDRep. Irreducibility and characters use a field, as their Mathlib definitions require.

@[simp]

theorem Representation.isIrreducible_ofQuotient_iff {k : Type u} {G : Type v} [Group G] [Field k] {V : Type u_1} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : (ρ.ofQuotient S).IsIrreducible ↔ ρ.IsIrreducible

A representation trivial on a normal subgroup S is irreducible exactly when the representation of G ⧸ S it factors through is irreducible.

@[simp]

theorem Rep.simple_ofQuotient_iff {k : Type u} {G : Type v} [Group G] [Field k] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Simple (A.ofQuotient S) ↔ CategoryTheory.Simple A

An object of Rep k G on which a normal subgroup S acts trivially is simple exactly when the object of Rep k (G ⧸ S) it factors through is simple. In particular simplicity of A.ofQuotient S does not depend on the normal subgroup S acting trivially on A.

@[reducible, inline]

abbrev Subgroup.resFDRep {k : Type u} {G : Type v} [Group G] [Ring k] (S : Subgroup G) (B : FDRep k G) : FDRep k ↥S

Restriction of a finitely generated representation of G to a subgroup S: Mathlib's Action.res along S.subtype, under the definitional identification FDRep k G = Action (FGModuleCat k) G.

This is a reducible abbreviation, so Mathlib's Action.res API applies to it unchanged; in particular (Action.res (FGModuleCat k) S.subtype).map f : S.resFDRep B ⟶ S.resFDRep B' restricts an intertwiner, and is functorial by Functor.map_id and Functor.map_comp.

Equations

• S.resFDRep B = (Action.res (FGModuleCat k) S.subtype).obj B

@[simp]

theorem Subgroup.forget₂_obj_resFDRep {k : Type u} {G : Type v} [Group G] [Ring k] (S : Subgroup G) (B : FDRep k G) : (CategoryTheory.forget₂ (FDRep k ↥S) (Rep k ↥S)).obj (S.resFDRep B) = Rep.res S.subtype ((CategoryTheory.forget₂ (FDRep k G) (Rep k G)).obj B)

Restriction commutes with forgetting finite generation: after forgetting, Subgroup.resFDRep is Mathlib's Rep.res, on the nose rather than up to isomorphism.

@[simp]

theorem Subgroup.comap_subtype_ofFDRep {k : Type u} {G : Type v} [Group G] [Field k] (S : Subgroup G) (B : FDRep k G) : (TauCeti.ClassFunction.comap S.subtype) (TauCeti.ClassFunction.ofFDRep B) = TauCeti.ClassFunction.ofFDRep (S.resFDRep B)

Pulling the class function of a representation back along the inclusion of a subgroup gives the class function of the restricted representation: ClassFunction.comap S.subtype is restriction of class functions.