Duals of actions on underlying objects

For a right rigid monoidal category V and a group H, Mathlib makes Action V H right rigid by pulling the right duals of the functor category SingleObj H ⥤ V back along the equivalence Action.functorCategoryEquivalence. The underlying object of the dual action is the dual of the underlying object (Action.rightDual_v). This file records that the same holds for the structure maps: the evaluation and coevaluation of the pairing (X, Xᘁ) in Action V H have, as underlying morphisms of V, the evaluation and coevaluation of (X.V, X.Vᘁ).

These are the identities needed to compute categorical constructions built from duals in Action V H on underlying objects. The first such construction is the Drinfeld isomorphism X ≅ Xᘁᘁ of a braided category: when V is braided, so is Action V H, and the Drinfeld isomorphism of an action is that of its underlying object.

Main results

• Action.evaluation_hom: the underlying morphism of ε_ X Xᘁ is ε_ X.V X.Vᘁ;
• Action.coevaluation_hom: the underlying morphism of η_ X Xᘁ is η_ X.V X.Vᘁ;
• Action.drinfeldIso_hom_hom, Action.drinfeldIso_inv_hom: the Drinfeld isomorphism of an action is that of its underlying object.

@[simp]

theorem Action.evaluation_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.RightRigidCategory V] {H : Type u_2} [Group H] (X : Action V H) : (ε_ X Xᘁ).hom = ε_ X.V X.Vᘁ

The evaluation of a dual action is the evaluation of the dual of the underlying object.

@[simp]

theorem Action.coevaluation_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.RightRigidCategory V] {H : Type u_2} [Group H] (X : Action V H) : (η_ X Xᘁ).hom = η_ X.V X.Vᘁ

The coevaluation of a dual action is the coevaluation of the dual of the underlying object.

@[simp]

theorem Action.drinfeldIso_hom_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.RightRigidCategory V] {H : Type u_2} [Group H] [CategoryTheory.BraidedCategory V] (X : Action V H) : (TauCeti.drinfeldIso X).hom.hom = (TauCeti.drinfeldIso X.V).hom

The Drinfeld isomorphism X ≅ Xᘁᘁ of an action is, on underlying objects, the Drinfeld isomorphism of the underlying object.

@[simp]

theorem Action.drinfeldIso_inv_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.RightRigidCategory V] {H : Type u_2} [Group H] [CategoryTheory.BraidedCategory V] (X : Action V H) : (TauCeti.drinfeldIso X).inv.hom = (TauCeti.drinfeldIso X.V).inv

The inverse of the Drinfeld isomorphism of an action is, on underlying objects, the inverse of the Drinfeld isomorphism of the underlying object.