noncomputable def vecLeftQuantumTrace (k : Type u) [Field k] {V : FGModuleCat k} (a : V ⟶ Vᘁᘁ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k)

The concrete left quantum trace of a morphism a : V ⟶ (V*)* in FGModuleCat k, obtained by composing the coevaluation, whiskering by a, and the evaluation.

noncomputable def vecPivotalDim (k : Type u) [Field k] (V : FGModuleCat k) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k)

The concrete pivotal dimension of V in FGModuleCat k, defined as the left quantum trace of the canonical double-dual evaluation iso V ≅ (V*)*.

theorem vecPivotalDim_apply_one (k : Type u) [Field k] (V : FGModuleCat k) : (ModuleCat.Hom.hom (vecPivotalDim k V).hom) 1 = ↑(Module.finrank k ↑V)

Evaluating the concrete pivotal dimension of V at 1 ∈ k yields dim_k(V), recovering the classical identification of categorical and linear dimensions.

theorem vec_spherical_condition (k : Type u) [Field k] (V : FGModuleCat k) : vecPivotalDim k V = vecPivotalDim k Vᘁ

The sphericality condition for FGModuleCat k: the concrete pivotal dimension of V agrees with that of its dual V*, since dim_k V = dim_k V*.