The standard spherical structure on finite-dimensional representations

For a field k and a group G, the category FDRep k G of finite-dimensional representations is symmetric and rigid, so it carries the canonical spherical structure of a symmetric rigid category (TauCeti.symmetricSphericalCategory). This is the standard spherical structure on FDRep k G, and this file identifies it with the classical data of linear algebra:

• its pivotal isomorphism V ≅ Vᘁᘁ is, on underlying vector spaces, the evaluation map Module.Dual.eval k V into the double dual;
• the categorical trace of an equivariant endomorphism f is the linear trace of f, read as the scalar endomorphism of the trivial representation k;
• the quantum dimension of a representation is the dimension of its underlying vector space.

All three are transported from FGModuleCat k along the forgetful functor, using that traces in categories of actions are computed on underlying objects (Action.drinfeldIso_hom_hom and Action.trace_hom).

Main results

• FDRep.drinfeldIso_hom_hom_hom_hom: the pivotal isomorphism, which is the Drinfeld isomorphism, is the double-dual evaluation map;
• FDRep.trace_eq_smul: the categorical trace is the linear trace;
• FDRep.quantumDim_eq_smul: the quantum dimension is the dimension.

References

• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.7

theorem FDRep.drinfeldIso_hom_hom_hom_hom {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) : ModuleCat.Hom.hom (TauCeti.drinfeldIso V).hom.hom.hom = Module.Dual.eval k ↑V.V

The Drinfeld isomorphism V ≅ Vᘁᘁ of a finite-dimensional representation, which is the canonical pivotal isomorphism pivotalIsoApp V by TauCeti.pivotalIsoApp_eq_drinfeldIso, is on underlying vector spaces the evaluation map into the double dual.

@[simp]

theorem FDRep.trace_eq_smul {k : Type u} {G : Type v} [Field k] [Group G] {V : FDRep k G} (f : V ⟶ V) : TauCeti.trace f = (LinearMap.trace k ↑V.V) (ModuleCat.Hom.hom f.hom.hom) • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G))

The categorical trace of an equivariant endomorphism of a finite-dimensional representation is its linear trace, acting on the trivial representation by scalar multiplication.

@[simp]

theorem FDRep.quantumDim_eq_smul {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) : TauCeti.quantumDim V = ↑(Module.finrank k ↑V.V) • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G))

The quantum dimension of a finite-dimensional representation is the dimension of its underlying vector space, acting on the trivial representation by scalar multiplication.