The standard spherical structure on finite-dimensional vector spaces

The category FGModuleCat K of finite-dimensional vector spaces over a field K is symmetric and rigid, so it carries the canonical spherical structure of a symmetric rigid category, whose pivotal isomorphisms are the Drinfeld isomorphisms. This file identifies that structure with the classical one:

• the pivotal isomorphism V ≅ Vᘁᘁ is the evaluation map Module.Dual.eval K V of a vector space into its double dual;
• the categorical trace of an endomorphism f is its linear trace LinearMap.trace K V f, read as the scalar endomorphism of the unit object K;
• consequently the quantum dimension of V is its dimension finrank K V, and every Frobenius–Schur indicator ν_n(V) equals finrank K V.

Main results

• FGModuleCat.drinfeldIso_hom_hom_hom: the pivotal isomorphism, which is the Drinfeld isomorphism, is the double-dual evaluation map;
• FGModuleCat.trace_eq_smul and FGModuleCat.trace_hom_hom_one: the categorical trace is the linear trace;
• FGModuleCat.quantumDim_eq_smul and FGModuleCat.quantumDim_hom_hom_one: the quantum dimension is the dimension;
• FGModuleCat.frobeniusSchurIndicator_eq_finrank: every Frobenius–Schur indicator ν_n(V) of a finite-dimensional vector space is (finrank K V : K).

References

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

@[simp]

theorem FGModuleCat.drinfeldIso_hom_hom_hom {K : Type u} [Field K] (V : FGModuleCat K) : ModuleCat.Hom.hom (TauCeti.drinfeldIso V).hom.hom = Module.Dual.eval K ↑V

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

@[simp]

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

The categorical trace of an endomorphism of a finite-dimensional vector space is its linear trace, acting on the unit object by scalar multiplication.

theorem FGModuleCat.trace_hom_hom_one {K : Type u} [Field K] {V : FGModuleCat K} (f : V ⟶ V) : (ModuleCat.Hom.hom (TauCeti.trace f).hom) 1 = (LinearMap.trace K ↑V) (ModuleCat.Hom.hom f.hom)

Evaluating the categorical trace of f : V ⟶ V at 1 : K recovers its linear trace.

@[simp]

theorem FGModuleCat.quantumDim_eq_smul {K : Type u} [Field K] (V : FGModuleCat K) : TauCeti.quantumDim V = ↑(Module.finrank K ↑V) • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat K))

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

theorem FGModuleCat.quantumDim_hom_hom_one {K : Type u} [Field K] (V : FGModuleCat K) : (ModuleCat.Hom.hom (TauCeti.quantumDim V).hom) 1 = ↑(Module.finrank K ↑V)

Evaluating the quantum dimension of V at 1 : K recovers finrank K V.

@[simp]

theorem FGModuleCat.frobeniusSchurIndicator_eq_finrank {K : Type u} [Field K] (V : FGModuleCat K) (n : ℕ+) : TauCeti.frobeniusSchurIndicator K V n = ↑(Module.finrank K ↑V)

Every Frobenius–Schur indicator ν_n(V) of a finite-dimensional vector space in FGModuleCat K equals (finrank K V : K).