Internal Hom from a finite projective module

For a finite projective module M, the canonical contraction from Mᵛ ⊗ N to Hom_R(M,N) is an isomorphism, natural in both variables. This is the affine algebraic model for the identification of the internal Hom from a finite locally free sheaf with tensoring by its dual. The construction uses Mathlib's dualTensorHomEquiv.

noncomputable def ModuleCat.dualTensorIhomIso {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (N : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.tensorObj (↧(Module.Dual R ↑M)) N ≅ (CategoryTheory.ihom M).obj N

The dual of a finite projective module tensored with N is the internal Hom from M to N. Its forward map sends f ⊗ n to m ↦ f(m) • n.

Equations

• M.dualTensorIhomIso N = ((dualTensorHomEquiv R ↑M ↑N).trans ModuleCat.homLinearEquiv.symm).toModuleIso

@[simp]

theorem ModuleCat.dualTensorIhomIso_hom_tmul {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (N : ModuleCat R) (f : Module.Dual R ↑M) (n : ↑N) (m : ↑M) : (Hom.hom ((CategoryTheory.ConcreteCategory.hom (M.dualTensorIhomIso N).hom) (f ⊗ₜ[R] n))) m = f m • n

The contraction isomorphism evaluates a pure tensor by applying its functional to the argument and scaling the tensor's second factor.

noncomputable def ModuleCat.dualTensorIhomNatIso {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] : CategoryTheory.MonoidalCategory.tensorLeft ↧(Module.Dual R ↑M) ≅ CategoryTheory.ihom M

The contraction isomorphism is natural in the target module.

Equations

• M.dualTensorIhomNatIso = CategoryTheory.NatIso.ofComponents M.dualTensorIhomIso ⋯

@[simp]

theorem ModuleCat.dualTensorIhomNatIso_hom_app {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (N : ModuleCat R) : M.dualTensorIhomNatIso.hom.app N = (M.dualTensorIhomIso N).hom

The component of the natural tensor–Hom comparison is the contraction isomorphism.

@[simp]

theorem ModuleCat.dualTensorIhomNatIso_inv_app {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (N : ModuleCat R) : M.dualTensorIhomNatIso.inv.app N = (M.dualTensorIhomIso N).inv

The inverse component of the natural tensor–Hom comparison is the inverse contraction isomorphism.

@[simp]

theorem ModuleCat.dualTensorIhomIso_ev {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (N : ModuleCat R) (m : ↑M) (f : Module.Dual R ↑M) (n : ↑N) : (Hom.hom ((CategoryTheory.ihom.ev M).app N)) (m ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom (M.dualTensorIhomIso N).hom) (f ⊗ₜ[R] n)) = f m • n

Under the contraction isomorphism, internal-Hom evaluation sends m ⊗ (f ⊗ n) to f(m) • n.

theorem ModuleCat.dualTensorIhomIso_naturality_left {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] (M' : ModuleCat R) [Module.Finite R ↑M'] [Module.Projective R ↑M'] (φ : M ⟶ M') (N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ofHom (Hom.hom φ).dualMap) N) (M.dualTensorIhomIso N).hom = CategoryTheory.CategoryStruct.comp (M'.dualTensorIhomIso N).hom ((CategoryTheory.MonoidalClosed.pre φ).app N)

The tensor–Hom comparison is contravariantly natural in a finite projective source: precomposing a linear map with φ corresponds to tensoring with the dual map of φ.