The dual-tensor comparison for modules

The categorical map from the tensor product of the internal dual of M with N to the internal Hom from M to N is Mathlib's contraction dualTensorHom. Its action on a pure tensor is the familiar formula f ⊗ n ↦ (m ↦ f m • n). This identification connects categorical dualizability with the algebraic dual-basis criterion.

The contraction and dual-basis results are from Mathlib's LinearAlgebra.Contraction.

theorem ModuleCat.dualTensorIhom_app_eq {R : Type u} [CommRing R] (M N : ModuleCat R) : (TauCeti.dualTensorIhom M).app N = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight homLinearEquiv.toModuleIso.hom N) (CategoryTheory.CategoryStruct.comp (ofHom (dualTensorHom R ↑M ↑N)) homLinearEquiv.toModuleIso.inv)

The categorical dual-tensor comparison is linear contraction, after identifying internal Homs with linear maps.

theorem ModuleCat.isIso_dualTensorIhom_app_iff {R : Type u} [CommRing R] (M N : ModuleCat R) : CategoryTheory.IsIso ((TauCeti.dualTensorIhom M).app N) ↔ Function.Bijective ⇑(dualTensorHom R ↑M ↑N)

At a target module N, the categorical dual-tensor comparison is invertible exactly when linear contraction Mᵛ ⊗ N → Hom(M,N) is bijective.