Restriction of representations

Given a group homomorphism f : H →* G, we have the restriction functor resFunctor f : Rep k G ⥤ Rep k H which sends a G-representation ρ to the H-representation ρ.comp f.

@[reducible, inline]

abbrev Rep.resFunctor {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) : CategoryTheory.Functor (Rep k G) (Rep k H)

The restriction functor Rep R G ⥤ Rep R H for a subgroup H of G.

@[reducible, inline]

abbrev Rep.res {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (M : Rep k G) : Rep k H

The restriction of X : Rep k G associated to a monoid homomorphism f : H →* G

@[simp]

theorem Rep.res_obj_ρ {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (M : Rep k G) : (res f M).ρ = MonoidHom.comp M.ρ f

theorem Rep.coe_res_obj_ρ' {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (M : Rep k G) (h : H) : (res f M).ρ h = M.ρ (f h)

theorem Rep.res_obj_V {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (M : Rep k G) : ↑(res f M) = ↑M

theorem Rep.res_map_hom_toLinearMap {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {M N : Rep k G} (p : M ⟶ N) : (Hom.hom ((resFunctor f).map p)).toLinearMap = (Hom.hom p).toLinearMap

instance Rep.instFaithfulResFunctor {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) : (resFunctor f).Faithful

@[reducible, inline]

abbrev Rep.liftHomOfSurj {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {X Y : Rep k G} (hf : Function.Surjective ⇑f) (f' : res f X ⟶ res f Y) : X ⟶ Y

Morphism between X Y : Rep k G can be lifted from restrictions associated with f : H →* G when f is surjective.

@[simp]

theorem Rep.liftHomOfSurj_toLinearMap {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {X Y : Rep k G} (hf : Function.Surjective ⇑f) (f' : res f X ⟶ res f Y) : (Hom.hom (liftHomOfSurj f hf f')).toLinearMap = (Hom.hom f').toLinearMap

theorem Rep.full_res {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (hf : Function.Surjective ⇑f) : (resFunctor f).Full

instance Rep.instAdditiveResFunctor {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) : (resFunctor f).Additive

instance Rep.instLinearResFunctor {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) : CategoryTheory.Functor.Linear k (resFunctor f)

@[reducible, inline]

abbrev Rep.ofQuotient {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : Rep k (G ⧸ S)

Given a normal subgroup S ≤ G, a G-representation ρ which is trivial on S factors through G ⧸ S.

@[reducible, inline]

abbrev Rep.resOfQuotientIso {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : res (QuotientGroup.mk' S) (A.ofQuotient S) ≅ A

A G-representation A on which a normal subgroup S ≤ G acts trivially induces a G ⧸ S-representation on A, and composing this with the quotient map G → G ⧸ S gives the original representation by definition. Useful for typechecking.