noncomputable def vecDoubleDualIso (k : Type u) [Field k] (V : FGModuleCat k) : V ≅ Vᘁᘁ

The canonical double-dual isomorphism V ≅ (V*)* in FGModuleCat k, realized via the linear-algebraic evaluation equivalence.

@[implicit_reducible]

noncomputable instance instPivotalCategoryVec (k : Type u) [Field k] : TensorCategories.PivotalCategory (VecInstances.Vec k)

Vec k = FGModuleCat k is a pivotal category, with pivotal structure given by the canonical double-dual isomorphism (Definition 1.38.2).

@[implicit_reducible]

noncomputable instance instSphericalCategoryVec (k : Type u) [Field k] : TensorCategories.SphericalCategory (VecInstances.Vec k)

Vec k is a spherical category (Definition 1.39.1): the pivotal dimension of any object equals the pivotal dimension of its dual.