Traces of actions in a symmetric rigid category

Let V be a symmetric rigid monoidal category and H a group. Then Action V H is again symmetric and rigid, so both V and Action V H carry their canonical spherical structures, whose pivotal isomorphisms are the Drinfeld isomorphisms. Since the duals, the evaluations, the coevaluations and the braiding of Action V H are those of V on underlying objects, so are the pivotal isomorphisms (Action.drinfeldIso_hom_hom), the traces and the dimensions: the categorical trace of an equivariant endomorphism is the trace of the underlying endomorphism in V.

Furthermore, for any action X : Action V H, element g : H, and n : ℕ, the categorical trace in V of ((tensorPow X (n + 1)).ρ g).asHom followed by the cyclic shift (tensorPowShiftIso X n).hom.hom equals trace (X.ρ (g ^ (n + 1))).asHom (Action.trace_ρ_comp_tensorPowShiftIso_hom). For V = FGModuleCat k this computes the higher Frobenius–Schur indicators of FDRep k G.

Main results

• Action.rightTrace_hom, Action.leftTrace_hom, Action.trace_hom: the traces of an endomorphism of an action are those of the underlying endomorphism;
• Action.quantumDim_hom: the quantum dimension of an action is that of its underlying object;
• Action.trace_ρ_comp_tensorPowShiftIso_hom: the trace of g acting on tensorPow X (n + 1) composed with the cyclic shift equals the trace of g ^ (n + 1) acting on X.

@[simp]

theorem Action.rightTrace_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.RigidCategory V] {H : Type u_2} [Group H] {X : Action V H} (f : X ⟶ X) : (TauCeti.rightTrace f).hom = TauCeti.rightTrace f.hom

The right trace of an endomorphism of an action is the right trace of the underlying endomorphism.

@[simp]

theorem Action.leftTrace_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.RigidCategory V] {H : Type u_2} [Group H] {X : Action V H} (f : X ⟶ X) : (TauCeti.leftTrace f).hom = TauCeti.leftTrace f.hom

The left trace of an endomorphism of an action is the left trace of the underlying endomorphism.

@[simp]

theorem Action.trace_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.RigidCategory V] {H : Type u_2} [Group H] {X : Action V H} (f : X ⟶ X) : (TauCeti.trace f).hom = TauCeti.trace f.hom

The trace of an endomorphism of an action is the trace of the underlying endomorphism.

@[simp]

theorem Action.quantumDim_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.RigidCategory V] {H : Type u_2} [Group H] (X : Action V H) : (TauCeti.quantumDim X).hom = TauCeti.quantumDim X.V

The quantum dimension of an action is the quantum dimension of its underlying object.

theorem Action.trace_ρ_comp_tensorPowShiftIso_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.RigidCategory V] {H : Type u_2} [Group H] (X : Action V H) (g : H) (n : ℕ) : TauCeti.trace (CategoryTheory.CategoryStruct.comp ((TauCeti.tensorPow X (n + 1)).ρ g).asHom (TauCeti.tensorPowShiftIso X n).hom.hom) = TauCeti.trace (X.ρ (g ^ (n + 1))).asHom

The categorical trace in V of g acting on tensorPow X (n + 1) followed by the cyclic shift (tensorPowShiftIso X n).hom.hom equals the categorical trace of g ^ (n + 1) acting on X.V.