theorem TensorCategories.vec_finrank_dual_eq (k : Type u) [Field k] (V : FGModuleCat k) : Module.finrank k ↑V = Module.finrank k ↑Vᘁ

For a finite-dimensional vector space V over a field k, the dimension of V equals the dimension of its dual V*.

theorem TensorCategories.vec_pivotalDimension_eq_finrank_smul_id (k : Type u) [Field k] (V : FGModuleCat k) : pivotalDimension (FGModuleCat k) V = Module.finrank k ↑V • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k))

The pivotal dimension of a finite-dimensional vector space V equals dim_k(V) times the identity of the unit object in FGModuleCat k.

theorem TensorCategories.vec_pivotalDimension_dual_eq_finrank_smul_id (k : Type u) [Field k] (V : FGModuleCat k) : pivotalDimension (FGModuleCat k) Vᘁ = Module.finrank k ↑Vᘁ • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k))

The pivotal dimension of the dual V* equals dim_k(V*) times the identity of the unit object in FGModuleCat k.

theorem TensorCategories.vec_pivotalDimension_dual_eq (k : Type u) [Field k] (V : FGModuleCat k) : pivotalDimension (FGModuleCat k) V = pivotalDimension (FGModuleCat k) Vᘁ

Sphericality of FGModuleCat k: the pivotal dimension of V agrees with the pivotal dimension of its dual V*.

@[implicit_reducible]

noncomputable instance TensorCategories.instSphericalCategoryFGModuleCat (k : Type u) [Field k] : SphericalCategory (FGModuleCat k)

FGModuleCat k is a spherical category (Definition 1.39.1), with sphericality witnessed by the equality of pivotal dimensions of V and V*.