mathlib3 documentation

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.

source
structure Action (V : Type (u+1)) [category_theory.large_category V] (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
source
@[simp]
theorem Action.ρ_one {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (A : Action V G) :
⇑(A.ρ) 1 = 𝟙 A.V
source
def Action.ρ_Aut {V : Type (u+1)} [category_theory.large_category V] {G : Group} (A : Action V (Mon.of ↥G)) :
G ⟶ Group.of (category_theory.Aut A.V)

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

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

The trivial representation of a group.

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

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

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

The identity morphism on a Action V G.

Equations
source
@[simp]
theorem Action.hom.id_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
(Action.hom.id M).hom = 𝟙 M.V
source
@[protected, instance]
def Action.hom.inhabited {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
inhabited (M.hom M)
Equations
source
def Action.hom.comp {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N K : Action V 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
source
@[simp]
theorem Action.hom.comp_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N K : Action V G} (p : M.hom N) (q : N.hom K) :
(p.comp q).hom = p.hom ≫ q.hom
source
@[protected, instance]
def Action.category_theory.category {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
category_theory.category (Action V G)
Equations
source
@[simp]
theorem Action.id_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
(𝟙 M).hom = 𝟙 M.V
source
@[simp]
theorem Action.comp_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) :
(f ≫ g).hom = f.hom ≫ g.hom
source
@[simp]
theorem Action.mk_iso_inv_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : ↥G), ⇑(M.ρ) g ≫ f.hom = f.hom ≫ ⇑(N.ρ) g) :
(Action.mk_iso f comm).inv.hom = f.inv
source
@[simp]
theorem Action.mk_iso_hom_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : ↥G), ⇑(M.ρ) g ≫ f.hom = f.hom ≫ ⇑(N.ρ) g) :
(Action.mk_iso f comm).hom.hom = f.hom
source
def Action.mk_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V 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
source
@[protected, instance]
def Action.is_iso_of_hom_is_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M ⟶ N) [category_theory.is_iso f.hom] :
category_theory.is_iso f
source
@[protected, instance]
def Action.is_iso_hom_mk {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M.V ⟶ N.V) [category_theory.is_iso f] (w : (∀ (g : ↥G), ⇑(M.ρ) g ≫ f = f ≫ ⇑(N.ρ) g) . "obviously") :
category_theory.is_iso {hom := f, comm' := w}
source
@[simp]
theorem Action.functor_category_equivalence.functor_obj_obj {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) (_x : category_theory.single_obj ↥G) :
(Action.functor_category_equivalence.functor.obj M).obj _x = M.V
source
@[simp]
theorem Action.functor_category_equivalence.functor_obj_map {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) (_x _x_1 : category_theory.single_obj ↥G) (g : _x ⟶ _x_1) :
(Action.functor_category_equivalence.functor.obj M).map g = ⇑(M.ρ) g
source
@[simp]
theorem Action.functor_category_equivalence.functor_map_app {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M N : Action V G) (f : M ⟶ N) (_x : category_theory.single_obj ↥G) :
(Action.functor_category_equivalence.functor.map f).app _x = f.hom
source
def Action.functor_category_equivalence.functor {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
Action V G ⥤ category_theory.single_obj ↥G ⥤ V

Auxilliary definition for functor_category_equivalence.

Equations
source
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_ρ_apply {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (F : category_theory.single_obj ↥G ⥤ V) (g : ↥G) :
⇑((Action.functor_category_equivalence.inverse.obj F).ρ) g = F.map g
source
def Action.functor_category_equivalence.inverse {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
(category_theory.single_obj ↥G ⥤ V) ⥤ Action V G

Auxilliary definition for functor_category_equivalence.

Equations
source
@[simp]
theorem Action.functor_category_equivalence.inverse_map_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M N : category_theory.single_obj ↥G ⥤ V) (f : M ⟶ N) :
(Action.functor_category_equivalence.inverse.map f).hom = f.app punit.star
source
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_V {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (F : category_theory.single_obj ↥G ⥤ V) :
(Action.functor_category_equivalence.inverse.obj F).V = F.obj punit.star
source
def Action.functor_category_equivalence.unit_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
𝟭 (Action V G) ≅ Action.functor_category_equivalence.functor ⋙ Action.functor_category_equivalence.inverse

Auxilliary definition for functor_category_equivalence.

Equations
source
@[simp]
theorem Action.functor_category_equivalence.unit_iso_inv_app_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (X : Action V G) :
(Action.functor_category_equivalence.unit_iso.inv.app X).hom = 𝟙 X.V
source
@[simp]
theorem Action.functor_category_equivalence.unit_iso_hom_app_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (X : Action V G) :
(Action.functor_category_equivalence.unit_iso.hom.app X).hom = 𝟙 X.V
source
@[simp]
theorem Action.functor_category_equivalence.counit_iso_hom_app_app {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (X : category_theory.single_obj ↥G ⥤ V) (X_1 : category_theory.single_obj ↥G) :
(Action.functor_category_equivalence.counit_iso.hom.app X).app X_1 = (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).hom
source
@[simp]
theorem Action.functor_category_equivalence.counit_iso_inv_app_app {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (X : category_theory.single_obj ↥G ⥤ V) (X_1 : category_theory.single_obj ↥G) :
(Action.functor_category_equivalence.counit_iso.inv.app X).app X_1 = (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).inv
source
def Action.functor_category_equivalence.counit_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
Action.functor_category_equivalence.inverse ⋙ Action.functor_category_equivalence.functor ≅ 𝟭 (category_theory.single_obj ↥G ⥤ V)

Auxilliary definition for functor_category_equivalence.

Equations
source
def Action.functor_category_equivalence (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
Action V G ≌ category_theory.single_obj ↥G ⥤ V

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

Equations
source
@[simp]
theorem Action.functor_category_equivalence_counit_iso (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).counit_iso = Action.functor_category_equivalence.counit_iso
source
@[simp]
theorem Action.functor_category_equivalence_inverse (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).inverse = Action.functor_category_equivalence.inverse
source
@[simp]
theorem Action.functor_category_equivalence_unit_iso (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).unit_iso = Action.functor_category_equivalence.unit_iso
source
@[simp]
theorem Action.functor_category_equivalence_functor (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).functor = Action.functor_category_equivalence.functor
source
theorem Action.functor_category_equivalence.functor_def (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).functor = Action.functor_category_equivalence.functor
source
theorem Action.functor_category_equivalence.inverse_def (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).inverse = Action.functor_category_equivalence.inverse
source
@[protected, instance]
def Action.category_theory.limits.has_finite_products (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_finite_products V] :
category_theory.limits.has_finite_products (Action V G)
source
@[protected, instance]
def Action.category_theory.limits.has_finite_limits (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_finite_limits V] :
category_theory.limits.has_finite_limits (Action V G)
source
@[protected, instance]
def Action.category_theory.limits.has_limits (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_limits V] :
category_theory.limits.has_limits (Action V G)
source
@[protected, instance]
def Action.category_theory.limits.has_colimits (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_colimits V] :
category_theory.limits.has_colimits (Action V G)
source
def Action.forget (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
Action V 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
source
@[simp]
theorem Action.forget_map (V : Type (u+1)) [category_theory.large_category V] (G : Mon) (M N : Action V G) (f : M ⟶ N) :
(Action.forget V G).map f = f.hom
source
@[simp]
theorem Action.forget_obj (V : Type (u+1)) [category_theory.large_category V] (G : Mon) (M : Action V G) :
(Action.forget V G).obj M = M.V
source
@[protected, instance]
def Action.forget.category_theory.faithful (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
category_theory.faithful (Action.forget V G)
source
@[protected, instance]
def Action.category_theory.concrete_category (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.concrete_category V] :
category_theory.concrete_category (Action V G)
Equations
source
@[protected, instance]
def Action.has_forget_to_V (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.concrete_category V] :
category_theory.has_forget₂ (Action V G) V
Equations
source
def Action.functor_category_equivalence_comp_evaluation (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
(Action.functor_category_equivalence V G).functor ⋙ (category_theory.evaluation (category_theory.single_obj ↥G) V).obj punit.star ≅ Action.forget V G

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

Equations
source
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_limits (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_limits V] :
category_theory.limits.preserves_limits (Action.forget V G)
Equations
source
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_colimits (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.limits.has_colimits V] :
category_theory.limits.preserves_colimits (Action.forget V G)
Equations
source
theorem Action.iso.conj_ρ {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M ≅ N) (g : ↥G) :
⇑(N.ρ) g = ⇑(((Action.forget V G).map_iso f).conj) (⇑(M.ρ) g)
source
@[protected, instance]
def Action.category_theory.limits.has_zero_morphisms {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.limits.has_zero_morphisms V] :
category_theory.limits.has_zero_morphisms (Action V G)
Equations
source
@[protected, instance]
def Action.forget_preserves_zero_morphisms {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.limits.has_zero_morphisms V] :
(Action.forget V G).preserves_zero_morphisms
source
@[protected, instance]
def Action.forget₂_preserves_zero_morphisms {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.limits.has_zero_morphisms V] [category_theory.concrete_category V] :
(category_theory.forget₂ (Action V G) V).preserves_zero_morphisms
source
@[protected, instance]
def Action.functor_category_equivalence_preserves_zero_morphisms {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.limits.has_zero_morphisms V] :
(Action.functor_category_equivalence V G).functor.preserves_zero_morphisms
source
@[protected, instance]
def Action.category_theory.preadditive {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] :
category_theory.preadditive (Action V G)
Equations
source
@[protected, instance]
def Action.forget_additive {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] :
(Action.forget V G).additive
source
@[protected, instance]
def Action.forget₂_additive {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] [category_theory.concrete_category V] :
(category_theory.forget₂ (Action V G) V).additive
source
@[protected, instance]
def Action.functor_category_equivalence_additive {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] :
(Action.functor_category_equivalence V G).functor.additive
source
@[simp]
theorem Action.zero_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} :
0.hom = 0
source
@[simp]
theorem Action.neg_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} (f : X ⟶ Y) :
(-f).hom = -f.hom
source
@[simp]
theorem Action.add_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} (f g : X ⟶ Y) :
(f + g).hom = f.hom + g.hom
source
@[simp]
theorem Action.sum_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} {ι : Type u_1} (f : ι → (X ⟶ Y)) (s : finset ι) :
(s.sum f).hom = s.sum (λ (i : ι), (f i).hom)
source
@[protected, instance]
def Action.category_theory.linear {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] :
category_theory.linear R (Action V G)
Equations
source
@[protected, instance]
def Action.forget_linear {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] :
category_theory.functor.linear R (Action.forget V G)
source
@[protected, instance]
def Action.forget₂_linear {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] [category_theory.concrete_category V] :
category_theory.functor.linear R (category_theory.forget₂ (Action V G) V)
source
@[protected, instance]
def Action.functor_category_equivalence_linear {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] :
category_theory.functor.linear R (Action.functor_category_equivalence V G).functor
source
@[simp]
theorem Action.smul_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] {X Y : Action V G} (r : R) (f : X ⟶ Y) :
(r • f).hom = r • f.hom
source
def Action.abelian_aux {V : Type (u+1)} [category_theory.large_category V] {G : Mon} :
Action V G ≌ ulift (category_theory.single_obj ↥G) ⥤ V

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

Equations
source
@[protected, instance]
noncomputable def Action.category_theory.abelian {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.abelian V] :
category_theory.abelian (Action V G)
Equations
source
@[protected, instance]
def Action.category_theory.monoidal_category {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] :
category_theory.monoidal_category (Action V G)
Equations
source
@[simp]
theorem Action.tensor_unit_V {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] :
(𝟙_ (Action V G)).V = 𝟙_ V
source
@[simp]
theorem Action.tensor_unit_rho {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {g : ↥G} :
⇑((𝟙_ (Action V G)).ρ) g = 𝟙 (𝟙_ V)
source
@[simp]
theorem Action.tensor_V {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y : Action V G} :
(X ⊗ Y).V = X.V ⊗ Y.V
source
@[simp]
theorem Action.tensor_rho {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y : Action V G} {g : ↥G} :
⇑((X ⊗ Y).ρ) g = ⇑(X.ρ) g ⊗ ⇑(Y.ρ) g
source
@[simp]
theorem Action.tensor_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {W X Y Z : Action V G} (f : W ⟶ X) (g : Y ⟶ Z) :
(f ⊗ g).hom = f.hom ⊗ g.hom
source
@[simp]
theorem Action.associator_hom_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y Z : Action V G} :
(α_ X Y Z).hom.hom = (α_ X.V Y.V Z.V).hom
source
@[simp]
theorem Action.associator_inv_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y Z : Action V G} :
(α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
source
@[simp]
theorem Action.left_unitor_hom_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X : Action V G} :
(λ_ X).hom.hom = (λ_ X.V).hom
source
@[simp]
theorem Action.left_unitor_inv_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X : Action V G} :
(λ_ X).inv.hom = (λ_ X.V).inv
source
@[simp]
theorem Action.right_unitor_hom_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X : Action V G} :
(ρ_ X).hom.hom = (ρ_ X.V).hom
source
@[simp]
theorem Action.right_unitor_inv_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X : Action V G} :
(ρ_ X).inv.hom = (ρ_ X.V).inv
source
def Action.tensor_unit_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {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
source
def Action.forget_monoidal (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
category_theory.monoidal_functor (Action V G) V

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

Equations
source
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_ε (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
(Action.forget_monoidal V G).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ V)
source
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_to_functor (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
(Action.forget_monoidal V G).to_lax_monoidal_functor.to_functor = Action.forget V G
source
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_μ (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (X Y : Action V G) :
(Action.forget_monoidal V G).to_lax_monoidal_functor.μ X Y = 𝟙 ({obj := (Action.forget V G).obj, map := (Action.forget V G).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (Action.forget V G).obj, map := (Action.forget V G).map, map_id' := _, map_comp' := _}.obj Y)
source
@[protected, instance]
def Action.forget_monoidal_faithful (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
category_theory.faithful (Action.forget_monoidal V G).to_lax_monoidal_functor.to_functor
source
@[protected, instance]
def Action.category_theory.braided_category (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.braided_category V] :
category_theory.braided_category (Action V G)
Equations
source
@[simp]
theorem Action.forget_braided_to_monoidal_functor (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.braided_category V] :
(Action.forget_braided V G).to_monoidal_functor = Action.forget_monoidal V G
source
def Action.forget_braided (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.braided_category V] :
category_theory.braided_functor (Action V G) V

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

Equations
source
@[protected, instance]
def Action.forget_braided_faithful (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.braided_category V] :
category_theory.faithful (Action.forget_braided V G).to_monoidal_functor.to_lax_monoidal_functor.to_functor
source
@[protected, instance]
def Action.category_theory.symmetric_category (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.symmetric_category V] :
category_theory.symmetric_category (Action V G)
Equations
source
@[protected, instance]
def Action.category_theory.monoidal_preadditive (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.preadditive V] [category_theory.monoidal_preadditive V] :
category_theory.monoidal_preadditive (Action V G)
source
@[protected, instance]
def Action.category_theory.monoidal_linear (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] [category_theory.preadditive V] [category_theory.monoidal_preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] [category_theory.monoidal_linear R V] :
category_theory.monoidal_linear R (Action V G)
source
noncomputable def Action.functor_category_monoidal_equivalence (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
category_theory.monoidal_functor (Action V G) (category_theory.single_obj ↥G ⥤ V)

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

Equations
source
@[protected, instance]
def Action.to_functor.category_theory.is_equivalence (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
category_theory.is_equivalence (Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor
Equations
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.μ_app (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A B : Action V G) :
((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.μ A B).app punit.star = 𝟙 (((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.obj A ⊗ (Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.obj B).obj punit.star)
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.μ_iso_inv_app (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A B : Action V G) :
((Action.functor_category_monoidal_equivalence V G).μ_iso A B).inv.app punit.star = 𝟙 (((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.obj (A ⊗ B)).obj punit.star)
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.ε_app (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] :
(Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.ε.app punit.star = 𝟙 ((𝟙_ (category_theory.single_obj ↥G ⥤ V)).obj punit.star)
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.inv_counit_app_hom (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A : Action V G) :
((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv.adjunction.counit.app A).hom = 𝟙 (((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv.inv ⋙ (Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv).obj A).V
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.counit_app (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A : category_theory.single_obj ↥G ⥤ V) :
((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.adjunction.counit.app A).app punit.star = 𝟙 ((((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv ⋙ (Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor).obj A).obj punit.star)
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.inv_unit_app_app (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A : category_theory.single_obj ↥G ⥤ V) :
((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv.adjunction.unit.app A).app punit.star = 𝟙 (((𝟭 (category_theory.single_obj ↥G ⥤ V)).obj A).obj punit.star)
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.unit_app_hom (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] (A : Action V G) :
((Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.adjunction.unit.app A).hom = 𝟙 ((𝟭 (Action V G)).obj A).V
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.functor_map (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] {A B : Action V G} (f : A ⟶ B) :
(Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.map f = Action.functor_category_equivalence.functor.map f
source
@[simp]
theorem Action.functor_category_monoidal_equivalence.inverse_map (V : Type (u+1)) [category_theory.large_category V] (G : Mon) [category_theory.monoidal_category V] {A B : category_theory.single_obj ↥G ⥤ V} (f : A ⟶ B) :
(Action.functor_category_monoidal_equivalence V G).to_lax_monoidal_functor.to_functor.inv.map f = Action.functor_category_equivalence.inverse.map f
source
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.right_rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.right_rigid_category V] :
category_theory.right_rigid_category (category_theory.single_obj ↥↑H ⥤ V)
Equations
source
@[protected, instance]
noncomputable def Action.category_theory.right_rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.right_rigid_category V] :
category_theory.right_rigid_category (Action V ↑H)

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

Equations
source
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.left_rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.left_rigid_category V] :
category_theory.left_rigid_category (category_theory.single_obj ↥↑H ⥤ V)
Equations
source
@[protected, instance]
noncomputable def Action.category_theory.left_rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.left_rigid_category V] :
category_theory.left_rigid_category (Action V ↑H)

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

Equations
source
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.rigid_category V] :
category_theory.rigid_category (category_theory.single_obj ↥↑H ⥤ V)
Equations
source
@[protected, instance]
noncomputable def Action.category_theory.rigid_category (V : Type (u+1)) [category_theory.large_category V] [category_theory.monoidal_category V] (H : Group) [category_theory.rigid_category V] :
category_theory.rigid_category (Action V ↑H)

If V is rigid, so is Action V G.

Equations
source
@[simp]
theorem Action.right_dual_V {V : Type (u+1)} [category_theory.large_category V] [category_theory.monoidal_category V] {H : Group} (X : Action V ↑H) [category_theory.right_rigid_category V] :
Xᘁ.V = X.Vᘁ
source
@[simp]
theorem Action.left_dual_V {V : Type (u+1)} [category_theory.large_category V] [category_theory.monoidal_category V] {H : Group} (X : Action V ↑H) [category_theory.left_rigid_category V] :
ᘁX.V = ᘁ(X.V)
source
@[simp]
theorem Action.right_dual_ρ {V : Type (u+1)} [category_theory.large_category V] [category_theory.monoidal_category V] {H : Group} (X : Action V ↑H) [category_theory.right_rigid_category V] (h : ↥H) :
⇑(Xᘁ.ρ) h = (⇑(X.ρ) h⁻¹)ᘁ
source
@[simp]
theorem Action.left_dual_ρ {V : Type (u+1)} [category_theory.large_category V] [category_theory.monoidal_category V] {H : Group} (X : Action V ↑H) [category_theory.left_rigid_category V] (h : ↥H) :
⇑(ᘁX.ρ) h = ᘁ(⇑(X.ρ) h⁻¹)
source
def Action.Action_punit_equivalence {V : Type (u+1)} [category_theory.large_category V] :
Action V (Mon.of punit) ≌ V

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

Equations
source
def Action.res (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) :
Action V H ⥤ Action V 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
source
@[simp]
theorem Action.res_obj_V (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) (M : Action V H) :
((Action.res V f).obj M).V = M.V
source
@[simp]
theorem Action.res_obj_ρ (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) (M : Action V H) :
((Action.res V f).obj M).ρ = f ≫ M.ρ
source
@[simp]
theorem Action.res_map_hom (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) (M N : Action V H) (p : M ⟶ N) :
((Action.res V f).map p).hom = p.hom
source
def Action.res_id (V : Type (u+1)) [category_theory.large_category V] {G : Mon} :
Action.res V (𝟙 G) ≅ 𝟭 (Action V G)

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

Equations
source
@[simp]
theorem Action.res_id_hom_app_hom (V : Type (u+1)) [category_theory.large_category V] {G : Mon} (X : Action V G) :
((Action.res_id V).hom.app X).hom = 𝟙 X.V
source
@[simp]
theorem Action.res_id_inv_app_hom (V : Type (u+1)) [category_theory.large_category V] {G : Mon} (X : Action V G) :
((Action.res_id V).inv.app X).hom = 𝟙 X.V
source
def Action.res_comp (V : Type (u+1)) [category_theory.large_category V] {G H K : Mon} (f : G ⟶ H) (g : H ⟶ K) :
Action.res V g ⋙ Action.res V f ≅ Action.res V (f ≫ g)

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

Equations
source
@[simp]
theorem Action.res_comp_inv_app_hom (V : Type (u+1)) [category_theory.large_category V] {G H K : Mon} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) :
((Action.res_comp V f g).inv.app X).hom = 𝟙 X.V
source
@[simp]
theorem Action.res_comp_hom_app_hom (V : Type (u+1)) [category_theory.large_category V] {G H K : Mon} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) :
((Action.res_comp V f g).hom.app X).hom = 𝟙 X.V
source
@[protected, instance]
def Action.res_additive (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) [category_theory.preadditive V] :
(Action.res V f).additive
source
@[protected, instance]
def Action.res_linear (V : Type (u+1)) [category_theory.large_category V] {G H : Mon} (f : G ⟶ H) {R : Type u_1} [semiring R] [category_theory.preadditive V] [category_theory.linear R V] :
category_theory.functor.linear R (Action.res V f)
source
def Action.of_mul_action (G H : Type u) [monoid G] [mul_action G H] :
Action (Type u) (Mon.of G)

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

Equations
source
@[simp]
theorem Action.of_mul_action_apply {G H : Type u} [monoid G] [mul_action G H] (g : G) (x : H) :
⇑((Action.of_mul_action G H).ρ) g x = g • x
source
def Action.of_mul_action_limit_cone {ι : Type v} (G : Type (max v u)) [monoid G] (F : ι → Type (max v u)) [Π (i : ι), mul_action G (F i)] :
category_theory.limits.limit_cone (category_theory.discrete.functor (λ (i : ι), Action.of_mul_action G (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
source
def Action.left_regular (G : Type u) [monoid G] :
Action (Type u) (Mon.of G)

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

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

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

Equations
source
@[simp]
theorem Action.diagonal_ρ_apply (G : Type u) [monoid G] (n : ℕ) (ᾰ : ↥(Mon.of G)) (ᾰ_1 : fin n → G) (ᾰ_2 : fin n) :
⇑((Action.diagonal G n).ρ) ᾰ ᾰ_1 ᾰ_2 = ᾰ * ᾰ_1 ᾰ_2
source
@[simp]
theorem Action.diagonal_V (G : Type u) [monoid G] (n : ℕ) :
(Action.diagonal G n).V = (fin n → G)
source
def Action.diagonal_one_iso_left_regular (G : Type u) [monoid G] :
Action.diagonal G 1 ≅ Action.left_regular G

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

Equations
source
@[simp]
theorem Action.left_regular_tensor_iso_inv_hom (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) (g : (Action.left_regular G ⊗ {V := X.V, ρ := 1}).V) :
(Action.left_regular_tensor_iso G X).inv.hom g = (g.fst, ⇑(X.ρ) g.fst g.snd)
source
def Action.left_regular_tensor_iso (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) :
Action.left_regular G ⊗ X ≅ Action.left_regular 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
source
@[simp]
theorem Action.left_regular_tensor_iso_hom_hom (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) (g : (Action.left_regular G ⊗ X).V) :
(Action.left_regular_tensor_iso G X).hom.hom g = (g.fst, ⇑(X.ρ) (g.fst)⁻¹ g.snd)
source
@[simp]
theorem Action.diagonal_succ_inv_hom (G : Type u) [monoid G] (n : ℕ) (ᾰ : (Action.left_regular G ⊗ Action.diagonal G n).V) :
(Action.diagonal_succ G n).inv.hom ᾰ = fin.cons ᾰ.fst ᾰ.snd
source
@[simp]
theorem Action.diagonal_succ_hom_hom (G : Type u) [monoid G] (n : ℕ) (ᾰ : (Action.diagonal G (n + 1)).V) :
(Action.diagonal_succ G n).hom.hom ᾰ = (ᾰ 0, λ (j : fin n), ᾰ j.succ)
source
def Action.diagonal_succ (G : Type u) [monoid G] (n : ℕ) :
Action.diagonal G (n + 1) ≅ Action.left_regular G ⊗ Action.diagonal G n

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

Equations
source
@[simp]
theorem category_theory.functor.map_Action_map_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) (M N : Action V G) (f : M ⟶ N) :
((F.map_Action G).map f).hom = F.map f.hom
source
def category_theory.functor.map_Action {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) :
Action V G ⥤ Action W 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
source
@[simp]
theorem category_theory.functor.map_Action_obj_V {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) (M : Action V G) :
((F.map_Action G).obj M).V = F.obj M.V
source
@[simp]
theorem category_theory.functor.map_Action_obj_ρ_apply {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) (M : Action V G) (g : ↥G) :
⇑(((F.map_Action G).obj M).ρ) g = F.map (⇑(M.ρ) g)
source
@[protected, instance]
def category_theory.functor.map_Action_preadditive {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) [category_theory.preadditive V] [category_theory.preadditive W] [F.additive] :
(F.map_Action G).additive
source
@[protected, instance]
def category_theory.functor.map_Action_linear {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V ⥤ W) (G : Mon) [category_theory.preadditive V] [category_theory.preadditive W] {R : Type u_1} [semiring R] [category_theory.linear R V] [category_theory.linear R W] [F.additive] [category_theory.functor.linear R F] :
category_theory.functor.linear R (F.map_Action G)
source
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_μ_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) (X Y : Action V G) :
((F.map_Action G).to_lax_monoidal_functor.μ X Y).hom = F.to_lax_monoidal_functor.μ X.V Y.V
source
def category_theory.monoidal_functor.map_Action {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) :
category_theory.monoidal_functor (Action V G) (Action W G)

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

Equations
source
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_to_functor {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) :
(F.map_Action G).to_lax_monoidal_functor.to_functor = F.to_lax_monoidal_functor.to_functor.map_Action G
source
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_ε_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) :
(F.map_Action G).to_lax_monoidal_functor.ε.hom = F.to_lax_monoidal_functor.ε
source
@[simp]
theorem category_theory.monoidal_functor.map_Action_ε_inv_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) :
(category_theory.inv (F.map_Action G).to_lax_monoidal_functor.ε).hom = category_theory.inv F.to_lax_monoidal_functor.ε
source
@[simp]
theorem category_theory.monoidal_functor.map_Action_μ_inv_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] [category_theory.monoidal_category V] [category_theory.monoidal_category W] (F : category_theory.monoidal_functor V W) (G : Mon) (X Y : Action V G) :
(category_theory.inv ((F.map_Action G).to_lax_monoidal_functor.μ X Y)).hom = category_theory.inv (F.to_lax_monoidal_functor.μ X.V Y.V)