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.

@[implicit_reducible]

def Rep.resMap {k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] {X Y : Rep k G} (f : H →* G) (p : X ⟶ Y) : of (MonoidHom.comp X.ρ f) ⟶ of (MonoidHom.comp Y.ρ f)

The map induced by a monoid homomorphism f : H →* G on morphisms between G-representations.

Equations

• Rep.resMap f p = Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom p), isIntertwining' := ⋯ }

@[reducible, inline]

abbrev Rep.resFunctor {k : Type u} [Semiring 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.

Equations

• Rep.resFunctor f = { obj := fun (A : Rep k G) => Rep.of (MonoidHom.comp A.ρ f), map := fun {X Y : Rep k G} (f' : X ⟶ Y) => Rep.resMap f f', map_id := ⋯, map_comp := ⋯ }

@[reducible, inline]

abbrev Rep.res {k : Type u} [Semiring 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

Equations

• Rep.res f M = (Rep.resFunctor f).obj M

theorem Rep.res_id {k : Type u} [Semiring k] {G : Type v1} [Monoid G] (M : Rep k G) : res (MonoidHom.id G) M = M

@[simp]

theorem Rep.res_obj_ρ {k : Type u} [Semiring 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} [Semiring 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} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) (M : Rep k G) : ↑(res f M) = ↑M

@[simp]

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

@[deprecated Rep.resMap_hom_toLinearMap (since := "26/06/2026")]

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

Alias of Rep.resMap_hom_toLinearMap.

@[simp]

theorem Rep.resMap_hom_apply {k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {M N : Rep k G} (p : M ⟶ N) (x : ↑M) : (Hom.hom (resMap f p)) x = (Hom.hom p) x

instance Rep.instFaithfulResFunctor {k : Type u} [Semiring 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} [Semiring 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.

Equations

• Rep.liftHomOfSurj f hf f' = Rep.ofHom { toLinearMap := (Rep.Hom.hom f').toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Rep.liftHomOfSurj_toLinearMap {k : Type u} [Semiring 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} [Semiring 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} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) : (resFunctor f).Additive

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

instance Rep.instPreservesLimitsResFunctor {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {k : Type u} [Ring k] : CategoryTheory.Limits.PreservesLimits (resFunctor f)

instance Rep.instPreservesColimitsResFunctor {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {k : Type u} [Ring k] : CategoryTheory.Limits.PreservesColimits (resFunctor f)

theorem Rep.isZero_res_iff {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {k : Type u} [Ring k] (M : Rep k G) : CategoryTheory.Limits.IsZero (res f M) ↔ CategoryTheory.Limits.IsZero M

An object of Rep k G is zero iff its restriction to H is zero.

theorem Rep.res_map_exact {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {k : Type u} [CommRing k] (S : CategoryTheory.ShortComplex (Rep k G)) : (S.map (resFunctor f)).Exact ↔ S.Exact

The instances above show that the restriction functor res φ : Rep R G ⥤ Rep R H preserves and reflects exactness.

theorem Rep.shortExact_res {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] {k : Type u} [CommRing k] (φ : H →* G) {S : CategoryTheory.ShortComplex (Rep k G)} : (S.map (resFunctor φ)).ShortExact ↔ S.ShortExact

@[reducible, inline]

abbrev Rep.ofQuotient {k : Type u} [Semiring 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.

Equations

• A.ofQuotient S = Rep.of (A.ρ.ofQuotient S)

@[reducible, inline]

abbrev Rep.resOfQuotientIso {k : Type u} [Semiring 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.

Equations

• A.resOfQuotientIso S = CategoryTheory.Iso.refl (Rep.res (QuotientGroup.mk' S) (A.ofQuotient S))