# mathlib3documentation

representation_theory.Action

# `Action V G`, the category of actions of a monoid `G` inside some category `V`. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The prototypical example is `V = Module R`, where `Action (Module R) G` is the category of `R`-linear representations of `G`.

We check `Action V G ≌ (single_obj G ⥤ V)`, and construct the restriction functors `res {G H : Mon} (f : G ⟶ H) : Action V H ⥤ Action V G`.

• When `V` has (co)limits so does `Action V G`.
• When `V` is monoidal, braided, or symmetric, so is `Action V G`.
• When `V` is preadditive, linear, or abelian so is `Action V G`.
structure Action (V : Type (u+1)) (G : Mon) :
Type (u+1)

An `Action V G` represents a bundled action of the monoid `G` on an object of some category `V`.

As an example, when `V = Module R`, this is an `R`-linear representation of `G`, while when `V = Type` this is a `G`-action.

Instances for `Action`
@[simp]
theorem Action.ρ_one {V : Type (u+1)} {G : Mon} (A : G) :
(A.ρ) 1 = 𝟙 A.V
def Action.ρ_Aut {V : Type (u+1)} {G : Group} (A : (Mon.of G)) :

When a group acts, we can lift the action to the group of automorphisms.

Equations
@[simp]
theorem Action.ρ_Aut_apply_inv {V : Type (u+1)} {G : Group} (A : (Mon.of G)) (g : G) :
((A.ρ_Aut) g).inv = (A.ρ) g⁻¹
@[simp]
theorem Action.ρ_Aut_apply_hom {V : Type (u+1)} {G : Group} (A : (Mon.of G)) (g : G) :
((A.ρ_Aut) g).hom = (A.ρ) g
@[protected, instance]
def Action.inhabited' (G : Mon) :
Equations
def Action.trivial (G : Mon) :

The trivial representation of a group.

Equations
@[protected, instance]
def Action.inhabited (G : Mon) :
Equations
@[ext]
structure Action.hom {V : Type (u+1)} {G : Mon} (M N : G) :

A homomorphism of `Action V G`s is a morphism between the underlying objects, commuting with the action of `G`.

Instances for `Action.hom`
theorem Action.hom.ext {V : Type (u+1)} {_inst_1 : category_theory.large_category V} {G : Mon} {M N : G} (x y : M.hom N) (h : x.hom = y.hom) :
x = y
theorem Action.hom.ext_iff {V : Type (u+1)} {_inst_1 : category_theory.large_category V} {G : Mon} {M N : G} (x y : M.hom N) :
x = y x.hom = y.hom
theorem Action.hom.comm {V : Type (u+1)} {G : Mon} {M N : G} (self : M.hom N) (g : G) :
(M.ρ) g self.hom = self.hom (N.ρ) g
def Action.hom.id {V : Type (u+1)} {G : Mon} (M : G) :
M.hom M

The identity morphism on a `Action V G`.

Equations
@[simp]
theorem Action.hom.id_hom {V : Type (u+1)} {G : Mon} (M : G) :
.hom = 𝟙 M.V
@[protected, instance]
def Action.hom.inhabited {V : Type (u+1)} {G : Mon} (M : G) :
Equations
def Action.hom.comp {V : Type (u+1)} {G : Mon} {M N K : G} (p : M.hom N) (q : N.hom K) :
M.hom K

The composition of two `Action V G` homomorphisms is the composition of the underlying maps.

Equations
@[simp]
theorem Action.hom.comp_hom {V : Type (u+1)} {G : Mon} {M N K : G} (p : M.hom N) (q : N.hom K) :
(p.comp q).hom = p.hom q.hom
@[protected, instance]
def Action.category_theory.category {V : Type (u+1)} {G : Mon} :
Equations
@[simp]
theorem Action.id_hom {V : Type (u+1)} {G : Mon} (M : G) :
(𝟙 M).hom = 𝟙 M.V
@[simp]
theorem Action.comp_hom {V : Type (u+1)} {G : Mon} {M N K : G} (f : M N) (g : N K) :
(f g).hom = f.hom g.hom
@[simp]
theorem Action.mk_iso_inv_hom {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
comm).inv.hom = f.inv
@[simp]
theorem Action.mk_iso_hom_hom {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
comm).hom.hom = f.hom
def Action.mk_iso {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
M N

Construct an isomorphism of `G` actions/representations from an isomorphism of the the underlying objects, where the forward direction commutes with the group action.

Equations
@[protected, instance]
def Action.is_iso_of_hom_is_iso {V : Type (u+1)} {G : Mon} {M N : G} (f : M N)  :
@[protected, instance]
def Action.is_iso_hom_mk {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (w : ( (g : G), (M.ρ) g f = f (N.ρ) g) . "obviously") :
@[simp]
theorem Action.functor_category_equivalence.functor_obj_map {V : Type (u+1)} {G : Mon} (M : G) (_x _x_1 : category_theory.single_obj G) (g : _x _x_1) :
= (M.ρ) g
@[simp]
theorem Action.functor_category_equivalence.functor_map_app {V : Type (u+1)} {G : Mon} (M N : G) (f : M N) (_x : category_theory.single_obj G) :

Auxilliary definition for `functor_category_equivalence`.

Equations
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_ρ_apply {V : Type (u+1)} {G : Mon} (F : V) (g : G) :
= F.map g

Auxilliary definition for `functor_category_equivalence`.

Equations
@[simp]
theorem Action.functor_category_equivalence.inverse_map_hom {V : Type (u+1)} {G : Mon} (M N : V) (f : M N) :
= f.app punit.star
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_V {V : Type (u+1)} {G : Mon} (F : V) :
= F.obj punit.star

Auxilliary definition for `functor_category_equivalence`.

Equations
@[simp]
@[simp]
@[simp]
theorem Action.functor_category_equivalence.counit_iso_hom_app_app {V : Type (u+1)} {G : Mon} (X : V) (X_1 : category_theory.single_obj G) :
= (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).hom
@[simp]
theorem Action.functor_category_equivalence.counit_iso_inv_app_app {V : Type (u+1)} {G : Mon} (X : V) (X_1 : category_theory.single_obj G) :
= (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).inv

Auxilliary definition for `functor_category_equivalence`.

Equations
def Action.functor_category_equivalence (V : Type (u+1)) (G : Mon) :
G

The category of actions of `G` in the category `V` is equivalent to the functor category `single_obj G ⥤ V`.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Action.forget (V : Type (u+1)) (G : Mon) :
G V

(implementation) The forgetful functor from bundled actions to the underlying objects.

Use the `category_theory.forget` API provided by the `concrete_category` instance below, rather than using this directly.

Equations
Instances for `Action.forget`
@[simp]
theorem Action.forget_map (V : Type (u+1)) (G : Mon) (M N : G) (f : M N) :
G).map f = f.hom
@[simp]
theorem Action.forget_obj (V : Type (u+1)) (G : Mon) (M : G) :
G).obj M = M.V
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
def Action.has_forget_to_V (V : Type (u+1)) (G : Mon)  :
Equations

The forgetful functor is intertwined by `functor_category_equivalence` with evaluation at `punit.star`.

Equations
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_limits (V : Type (u+1)) (G : Mon)  :
Equations
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_colimits (V : Type (u+1)) (G : Mon)  :
Equations
theorem Action.iso.conj_ρ {V : Type (u+1)} {G : Mon} {M N : G} (f : M N) (g : G) :
(N.ρ) g = (((Action.forget V G).map_iso f).conj) ((M.ρ) g)
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Action.category_theory.preadditive {V : Type (u+1)} {G : Mon}  :
Equations
@[protected, instance]
def Action.forget_additive {V : Type (u+1)} {G : Mon}  :
@[protected, instance]
def Action.forget₂_additive {V : Type (u+1)} {G : Mon}  :
@[protected, instance]
@[simp]
theorem Action.zero_hom {V : Type (u+1)} {G : Mon} {X Y : G} :
0.hom = 0
@[simp]
theorem Action.neg_hom {V : Type (u+1)} {G : Mon} {X Y : G} (f : X Y) :
(-f).hom = -f.hom
@[simp]
theorem Action.add_hom {V : Type (u+1)} {G : Mon} {X Y : G} (f g : X Y) :
(f + g).hom = f.hom + g.hom
@[simp]
theorem Action.sum_hom {V : Type (u+1)} {G : Mon} {X Y : G} {ι : Type u_1} (f : ι (X Y)) (s : finset ι) :
(s.sum f).hom = s.sum (λ (i : ι), (f i).hom)
@[protected, instance]
def Action.category_theory.linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
(Action V G)
Equations
@[protected, instance]
def Action.forget_linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
@[protected, instance]
def Action.forget₂_linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
@[protected, instance]
def Action.functor_category_equivalence_linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
@[simp]
theorem Action.smul_hom {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R] {X Y : G} (r : R) (f : X Y) :
(r f).hom = r f.hom
def Action.abelian_aux {V : Type (u+1)} {G : Mon} :
G

Auxilliary construction for the `abelian (Action V G)` instance.

Equations
@[protected, instance]
noncomputable def Action.category_theory.abelian {V : Type (u+1)} {G : Mon}  :
Equations
@[protected, instance]
Equations
@[simp]
theorem Action.tensor_unit_V {V : Type (u+1)} {G : Mon}  :
(𝟙_ (Action V G)).V = 𝟙_ V
@[simp]
theorem Action.tensor_unit_rho {V : Type (u+1)} {G : Mon} {g : G} :
((𝟙_ (Action V G)).ρ) g = 𝟙 (𝟙_ V)
@[simp]
theorem Action.tensor_V {V : Type (u+1)} {G : Mon} {X Y : G} :
(X Y).V = X.V Y.V
@[simp]
theorem Action.tensor_rho {V : Type (u+1)} {G : Mon} {X Y : G} {g : G} :
((X Y).ρ) g = (X.ρ) g (Y.ρ) g
@[simp]
theorem Action.tensor_hom {V : Type (u+1)} {G : Mon} {W X Y Z : G} (f : W X) (g : Y Z) :
(f g).hom = f.hom g.hom
@[simp]
theorem Action.associator_hom_hom {V : Type (u+1)} {G : Mon} {X Y Z : G} :
(α_ X Y Z).hom.hom = (α_ X.V Y.V Z.V).hom
@[simp]
theorem Action.associator_inv_hom {V : Type (u+1)} {G : Mon} {X Y Z : G} :
(α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
@[simp]
theorem Action.left_unitor_hom_hom {V : Type (u+1)} {G : Mon} {X : G} :
(λ_ X).hom.hom = (λ_ X.V).hom
@[simp]
theorem Action.left_unitor_inv_hom {V : Type (u+1)} {G : Mon} {X : G} :
(λ_ X).inv.hom = (λ_ X.V).inv
@[simp]
theorem Action.right_unitor_hom_hom {V : Type (u+1)} {G : Mon} {X : G} :
(ρ_ X).hom.hom = (ρ_ X.V).hom
@[simp]
theorem Action.right_unitor_inv_hom {V : Type (u+1)} {G : Mon} {X : G} :
(ρ_ X).inv.hom = (ρ_ X.V).inv
def Action.tensor_unit_iso {V : Type (u+1)} {G : Mon} {X : V} (f : 𝟙_ V X) :
𝟙_ (Action V G) {V := X, ρ := 1}

Given an object `X` isomorphic to the tensor unit of `V`, `X` equipped with the trivial action is isomorphic to the tensor unit of `Action V G`.

Equations
def Action.forget_monoidal (V : Type (u+1)) (G : Mon)  :

When `V` is monoidal the forgetful functor `Action V G` to `V` is monoidal.

Equations
@[simp]
@[simp]
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_μ (V : Type (u+1)) (G : Mon) (X Y : G) :
= 𝟙 ({obj := G).obj, map := G).map, map_id' := _, map_comp' := _}.obj X {obj := G).obj, map := G).map, map_id' := _, map_comp' := _}.obj Y)
@[protected, instance]
@[protected, instance]
Equations
@[simp]
def Action.forget_braided (V : Type (u+1)) (G : Mon)  :

When `V` is braided the forgetful functor `Action V G` to `V` is braided.

Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def Action.category_theory.monoidal_linear (V : Type (u+1)) (G : Mon) {R : Type u_1} [semiring R]  :
noncomputable def Action.functor_category_monoidal_equivalence (V : Type (u+1)) (G : Mon)  :

Upgrading the functor `Action V G ⥤ (single_obj G ⥤ V)` to a monoidal functor.

Equations
@[protected, instance]
Equations
@[simp]
theorem Action.functor_category_monoidal_equivalence.μ_app (V : Type (u+1)) (G : Mon) (A B : G) :
punit.star =
@[simp]
theorem Action.functor_category_monoidal_equivalence.μ_iso_inv_app (V : Type (u+1)) (G : Mon) (A B : G) :
.inv.app punit.star = 𝟙 punit.star)
@[simp]
theorem Action.functor_category_monoidal_equivalence.ε_app (V : Type (u+1)) (G : Mon)  :
punit.star = 𝟙 ((𝟙_ .obj punit.star)
@[simp]
@[simp]
theorem Action.functor_category_monoidal_equivalence.counit_app (V : Type (u+1)) (G : Mon) (A : V) :
punit.star =
@[simp]
theorem Action.functor_category_monoidal_equivalence.inv_unit_app_app (V : Type (u+1)) (G : Mon) (A : V) :
punit.star = 𝟙 (((𝟭 .obj A).obj punit.star)
@[simp]
theorem Action.functor_category_monoidal_equivalence.unit_app_hom (V : Type (u+1)) (G : Mon) (A : G) :
= 𝟙 ((𝟭 (Action V G)).obj A).V
@[simp]
theorem Action.functor_category_monoidal_equivalence.functor_map (V : Type (u+1)) (G : Mon) {A B : G} (f : A B) :
@[simp]
theorem Action.functor_category_monoidal_equivalence.inverse_map (V : Type (u+1)) (G : Mon) {A B : V} (f : A B) :
@[protected, instance]
Equations
@[protected, instance]
noncomputable def Action.category_theory.right_rigid_category (V : Type (u+1)) (H : Group)  :

If `V` is right rigid, so is `Action V G`.

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def Action.category_theory.left_rigid_category (V : Type (u+1)) (H : Group)  :

If `V` is left rigid, so is `Action V G`.

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def Action.category_theory.rigid_category (V : Type (u+1)) (H : Group)  :

If `V` is rigid, so is `Action V G`.

Equations
@[simp]
theorem Action.right_dual_V {V : Type (u+1)} {H : Group} (X : H)  :
X.V = X.V
@[simp]
theorem Action.left_dual_V {V : Type (u+1)} {H : Group} (X : H)  :
X.V = (X.V)
@[simp]
theorem Action.right_dual_ρ {V : Type (u+1)} {H : Group} (X : H) (h : H) :
(X.ρ) h = ((X.ρ) h⁻¹)
@[simp]
theorem Action.left_dual_ρ {V : Type (u+1)} {H : Group} (X : H) (h : H) :
(X.ρ) h = ((X.ρ) h⁻¹)
def Action.Action_punit_equivalence {V : Type (u+1)}  :
V

Actions/representations of the trivial group are just objects in the ambient category.

Equations
def Action.res (V : Type (u+1)) {G H : Mon} (f : G H) :
H G

The "restriction" functor along a monoid homomorphism `f : G ⟶ H`, taking actions of `H` to actions of `G`.

(This makes sense for any homomorphism, but the name is natural when `f` is a monomorphism.)

Equations
Instances for `Action.res`
@[simp]
theorem Action.res_obj_V (V : Type (u+1)) {G H : Mon} (f : G H) (M : H) :
((Action.res V f).obj M).V = M.V
@[simp]
theorem Action.res_obj_ρ (V : Type (u+1)) {G H : Mon} (f : G H) (M : H) :
((Action.res V f).obj M).ρ = f M.ρ
@[simp]
theorem Action.res_map_hom (V : Type (u+1)) {G H : Mon} (f : G H) (M N : H) (p : M N) :
((Action.res V f).map p).hom = p.hom
def Action.res_id (V : Type (u+1)) {G : Mon} :
(𝟙 G) 𝟭 (Action V G)

The natural isomorphism from restriction along the identity homomorphism to the identity functor on `Action V G`.

Equations
@[simp]
theorem Action.res_id_hom_app_hom (V : Type (u+1)) {G : Mon} (X : G) :
@[simp]
theorem Action.res_id_inv_app_hom (V : Type (u+1)) {G : Mon} (X : G) :
def Action.res_comp (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) :
g f (f g)

The natural isomorphism from the composition of restrictions along homomorphisms to the restriction along the composition of homomorphism.

Equations
@[simp]
theorem Action.res_comp_inv_app_hom (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) (X : K) :
f g).inv.app X).hom = 𝟙 X.V
@[simp]
theorem Action.res_comp_hom_app_hom (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) (X : K) :
f g).hom.app X).hom = 𝟙 X.V
@[protected, instance]
def Action.res_additive (V : Type (u+1)) {G H : Mon} (f : G H)  :
@[protected, instance]
def Action.res_linear (V : Type (u+1)) {G H : Mon} (f : G H) {R : Type u_1} [semiring R]  :
def Action.of_mul_action (G H : Type u) [monoid G] [ H] :

Bundles a type `H` with a multiplicative action of `G` as an `Action`.

Equations
@[simp]
theorem Action.of_mul_action_apply {G H : Type u} [monoid G] [ H] (g : G) (x : H) :
H).ρ) g x = g x
def Action.of_mul_action_limit_cone {ι : Type v} (G : Type (max v u)) [monoid G] (F : ι Type (max v u)) [Π (i : ι), (F i)] :

Given a family `F` of types with `G`-actions, this is the limit cone demonstrating that the product of `F` as types is a product in the category of `G`-sets.

Equations
def Action.left_regular (G : Type u) [monoid G] :

The `G`-set `G`, acting on itself by left multiplication.

Equations
@[simp]
theorem Action.left_regular_ρ_apply (G : Type u) [monoid G] (ᾰ : (Mon.of G)) (ᾰ_1 : G) :
.ρ) ᾰ_1 = * ᾰ_1
@[simp]
theorem Action.left_regular_V (G : Type u) [monoid G] :
.V = G
def Action.diagonal (G : Type u) [monoid G] (n : ) :

The `G`-set `Gⁿ`, acting on itself by left multiplication.

Equations
@[simp]
theorem Action.diagonal_ρ_apply (G : Type u) [monoid G] (n : ) (ᾰ : (Mon.of G)) (ᾰ_1 : fin n G) (ᾰ_2 : fin n) :
n).ρ) ᾰ_1 ᾰ_2 = * ᾰ_1 ᾰ_2
@[simp]
theorem Action.diagonal_V (G : Type u) [monoid G] (n : ) :
n).V = (fin n G)

We have `fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication.

Equations
@[simp]
theorem Action.left_regular_tensor_iso_inv_hom (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) (g : {V := X.V, ρ := 1}).V) :
g = (g.fst, (X.ρ) g.fst g.snd)
def Action.left_regular_tensor_iso (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) :
{V := X.V, ρ := 1}

Given `X : Action (Type u) (Mon.of G)` for `G` a group, then `G × X` (with `G` acting as left multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to `G × X` (with `G` acting as left multiplication on the first factor and trivially on the second). The isomorphism is given by `(g, x) ↦ (g, g⁻¹ • x)`.

Equations
@[simp]
theorem Action.left_regular_tensor_iso_hom_hom (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) (g : X).V) :
g = (g.fst, (X.ρ) (g.fst)⁻¹ g.snd)
@[simp]
theorem Action.diagonal_succ_inv_hom (G : Type u) [monoid G] (n : ) (ᾰ : .V) :
n).inv.hom = ᾰ.snd
@[simp]
theorem Action.diagonal_succ_hom_hom (G : Type u) [monoid G] (n : ) (ᾰ : (n + 1)).V) :
n).hom.hom = (ᾰ 0, λ (j : fin n), ᾰ j.succ)
def Action.diagonal_succ (G : Type u) [monoid G] (n : ) :
(n + 1)

The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on each factor.

Equations
@[simp]
theorem category_theory.functor.map_Action_map_hom {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M N : G) (f : M N) :
((F.map_Action G).map f).hom = F.map f.hom
def category_theory.functor.map_Action {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) :
G G

A functor between categories induces a functor between the categories of `G`-actions within those categories.

Equations
Instances for `category_theory.functor.map_Action`
@[simp]
theorem category_theory.functor.map_Action_obj_V {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M : G) :
((F.map_Action G).obj M).V = F.obj M.V
@[simp]
theorem category_theory.functor.map_Action_obj_ρ_apply {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M : G) (g : G) :
(((F.map_Action G).obj M).ρ) g = F.map ((M.ρ) g)
@[protected, instance]
def category_theory.functor.map_Action_preadditive {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) [F.additive] :
@[protected, instance]
def category_theory.functor.map_Action_linear {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) {R : Type u_1} [semiring R] [F.additive]  :
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_μ_hom {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) (X Y : G) :
.μ X Y).hom = Y.V
def category_theory.monoidal_functor.map_Action {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) :
(Action W G)

A monoidal functor induces a monoidal functor between the categories of `G`-actions within those categories.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.monoidal_functor.map_Action_ε_inv_hom {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) :
@[simp]
theorem category_theory.monoidal_functor.map_Action_μ_inv_hom {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) (X Y : G) :