Restricting an action along a monoid homomorphism is a monoidal functor

For a monoidal category V and a monoid homomorphism f : G →* H, Mathlib's Action.res V f : Action V H ⥤ Action V G reindexes an action of H along f, keeping the underlying object of V and precomposing the action homomorphism with f. It is already known to be additive (Action.res_additive). This file records that it is also monoidal, and monoidal in the strictest possible way: restricting a tensor product is the same object as the tensor product of the restrictions, because (X ⊗ Y).ρ g is X.ρ g ⊗ₘ Y.ρ g on the nose, so precomposing with f distributes over the tensor product without any comparison map. The unit and the tensorator of Action.res V f are therefore identities.

This is the structure a Grothendieck-ring construction needs of a functor before it induces a ring homomorphism, and it is what makes restriction of representations a homomorphism of representation rings in TauCeti/RepresentationTheory/RepresentationRing/Restriction.lean.

Main definitions

• Action.resTensorator: the tensorator, an identity morphism.
• Action.resUnitor: the unit comparison, an identity morphism.
• Action.resCoreMonoidal: the two of them packaged as a CategoryTheory.Functor.CoreMonoidal structure, whence the instance Action.resMonoidal : (Action.res V f).Monoidal.

Main statements

• Action.res_ε_hom, Action.res_μ_hom, Action.res_η_hom, Action.res_δ_hom: all four structure maps of the monoidal functor are identities on the underlying objects of V. These mirror Mathlib's Action.forget_ε, Action.forget_μ, Action.forget_η, Action.forget_δ.

def Action.resTensorator (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) (X Y : Action V H) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((res V f).obj X) ((res V f).obj Y) ≅ (res V f).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The tensorator of restriction along a monoid homomorphism, the identity: the restriction of X ⊗ Y and the tensor product of the restrictions of X and Y are the same object of Action V G.

Equations

• Action.resTensorator V f X Y = Action.mkIso (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj ((Action.res V f).obj X) ((Action.res V f).obj Y)).V) ⋯

@[simp]

theorem Action.resTensorator_hom_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) (X Y : Action V H) : (resTensorator V f X Y).hom.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V)

@[simp]

theorem Action.resTensorator_inv_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) (X Y : Action V H) : (resTensorator V f X Y).inv.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V)

def Action.resUnitor (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G) ≅ (res V f).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V H))

The unit comparison of restriction along a monoid homomorphism, the identity: the restriction of the tensor unit is the tensor unit.

Equations

• Action.resUnitor V f = Action.mkIso (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).V) ⋯

@[simp]

theorem Action.resUnitor_hom_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (resUnitor V f).hom.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

@[simp]

theorem Action.resUnitor_inv_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (resUnitor V f).inv.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

def Action.resCoreMonoidal (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (res V f).CoreMonoidal

Restriction along a monoid homomorphism, as a CategoryTheory.Functor.CoreMonoidal: the unit and the tensorator are the identities of Action.resUnitor and Action.resTensorator, and the three coherence axioms reduce to the corresponding identities in V.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Action.resMonoidal (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (res V f).Monoidal

Restriction of an action along a monoid homomorphism is a monoidal functor.

Equations

• Action.resMonoidal V f = (Action.resCoreMonoidal V f).toMonoidal

@[simp]

theorem Action.res_ε_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (CategoryTheory.Functor.LaxMonoidal.ε (res V f)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

The lax unit of the monoidal structure on restriction is the identity on the underlying object of V: restricting the tensor unit gives back the tensor unit.

@[simp]

theorem Action.res_η_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : (CategoryTheory.Functor.OplaxMonoidal.η (res V f)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

The oplax counit of the monoidal structure on restriction is the identity on the underlying object of V, being the inverse of Action.res_ε_hom.

@[simp]

theorem Action.res_μ_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) (X Y : Action V H) : (CategoryTheory.Functor.LaxMonoidal.μ (res V f) X Y).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V)

The lax tensorator of the monoidal structure on restriction is the identity on the underlying object of V: the tensor product of two restrictions is the restriction of the tensor product.

@[simp]

theorem Action.res_δ_hom (V : Type u) [CategoryTheory.Category.{w, u} V] [CategoryTheory.MonoidalCategory V] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) (X Y : Action V H) : (CategoryTheory.Functor.OplaxMonoidal.δ (res V f) X Y).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V)

The oplax tensorator of the monoidal structure on restriction is the identity on the underlying object of V, being the inverse of Action.res_μ_hom.