Restriction of actions

Restriction along a composite monoid homomorphism is successive restriction, as an equality of functors. This equality form complements Mathlib's natural isomorphism Action.resComp.

For actions in a linear category, restriction along a surjective monoid homomorphism preserves the finrank of morphism spaces. This uses Mathlib's fullness result Action.full_res and Functor.homLinearEquiv, and in particular applies to intertwining spaces of finite-dimensional representations over a commutative ring.

Main results

• MonoidHom.actionRes_comp: restriction along a composite is successive restriction.
• MonoidHom.finrank_hom_actionRes_of_surjective: restriction along a surjective monoid homomorphism preserves the finrank of morphism spaces in a linear category.

theorem MonoidHom.actionRes_comp {V : Type u_1} [CategoryTheory.Category.{u_5, u_1} V] {H : Type u_2} {K : Type u_3} {L : Type u_4} [Monoid H] [Monoid K] [Monoid L] (φ : K →* L) (ψ : H →* K) : Action.res V (φ.comp ψ) = (Action.res V φ).comp (Action.res V ψ)

Restriction of actions along a composite is successive restriction. This is the equality form of Mathlib's natural isomorphism Action.resComp.

theorem MonoidHom.finrank_hom_actionRes_of_surjective {V : Type u_1} [CategoryTheory.Category.{u_6, u_1} V] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {k : Type u_5} [Semiring k] [CategoryTheory.Preadditive V] [CategoryTheory.Linear k V] (f : H →* K) (hf : Function.Surjective ⇑f) (X Y : Action V K) : Module.finrank k ((Action.res V f).obj X ⟶ (Action.res V f).obj Y) = Module.finrank k (X ⟶ Y)

Restriction along a surjective monoid homomorphism preserves the finrank of morphism spaces in a linear category. In particular it preserves the dimension of intertwining spaces of representations.