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

The concrete double-dual isomorphism V ≅ (V*)* in FGModuleCat k, obtained from the canonical evaluation equivalence on finite-dimensional vector spaces.

noncomputable def vecTensorCoherenceIsoConcrete (k : Type u) [Field k] (V W : FGModuleCat k) : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ

The tensor-coherence isomorphism (V*)* ⊗ (W*)* ≅ ((V ⊗ W)*)* in FGModuleCat k, built by combining the double-dual isomorphisms on the factors with the one on the tensor.

theorem vecDoubleDualIsoConcrete_naturality (k : Type u) [Field k] {V W : FGModuleCat k} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (vecDoubleDualIsoConcrete k W).hom = CategoryTheory.CategoryStruct.comp (vecDoubleDualIsoConcrete k V).hom (fᘁᘁ)

Naturality of the concrete double-dual isomorphism: for any f : V ⟶ W in FGModuleCat k, the square involving f and the iterated right adjoint mate of f commutes.

theorem vecDoubleDualIsoConcrete_monoidality (k : Type u) [Field k] (V W : FGModuleCat k) : (vecDoubleDualIsoConcrete k (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (vecDoubleDualIsoConcrete k V).hom (vecDoubleDualIsoConcrete k W).hom) (vecTensorCoherenceIsoConcrete k V W).hom

Monoidality of the concrete double-dual isomorphism: it factors the iso (V ⊗ W) ≅ ((V ⊗ W)*)* through the iso V ≅ (V*)* tensored with W ≅ (W*)*, followed by the tensor-coherence iso.

theorem vecDoubleDualIsoConcrete_dimUnit (k : Type u) [Field k] : TensorCategories.leftQuantumTrace (FGModuleCat k) (vecDoubleDualIsoConcrete k (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k))).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k))

The left quantum trace of the concrete double-dual isomorphism on the unit object equals the identity of the unit — equivalently, dim(𝟙) = 1 in Vec_k.

@[reducible]

noncomputable def vecPivotalCategoryInstance (k : Type u) [Field k] : TensorCategories.PivotalCategory (FGModuleCat k)

FGModuleCat k is a pivotal category, with pivotal structure given by the canonical double-dual evaluation isomorphism. This corresponds to Definitions 1.38.1–1.38.2.