noncomputable def dualTensorSwapEquiv (k : Type u) [Field k] (V W : Type u) [AddCommGroup V] [Module k V] [Module.Free k V] [Module.Finite k V] [AddCommGroup W] [Module k W] [Module.Free k W] [Module.Finite k W] : Module.Dual k (TensorProduct k V W) ≃ₗ[k] TensorProduct k (Module.Dual k W) (Module.Dual k V)

The canonical linear equivalence (V ⊗ W)* ≃ₗ[k] W* ⊗ V* for finite-dimensional free k-modules, obtained by chaining the tensor-hom adjunction with the swap.

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

The canonical tensor-coherence isomorphism (V*)* ⊗ (W*)* ≅ ((V ⊗ W)*)* in FGModuleCat k, needed to assemble a monoidal pivotal structure.

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

The monoidal version of the double-dual isomorphism on FGModuleCat k, packaged from the linear-algebraic evaluation equivalence.