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

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

noncomputable def VecTensorDualCoherence.vecTensorCoherenceIso (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, assembled from the double-dual isos on V, W, and V ⊗ W.