Scalar duals as right modules

The scalar dual of a left module M over a k-algebra A is the right module ModuleCat.matlisDualObj k k M, the Matlis dual with values in the field k, with action (a • φ)(x) = φ(a.unop • x). Evaluation identifies a finite-dimensional module with the scalar dual of this right module. This pairing is used to form Tr D.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section I.3.

instance ModuleCat.instFiniteCarrierMulOppositeMatlisDualObj (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] (M : ModuleCat A) [Module.Finite k ↑M] : Module.Finite k ↑(matlisDualObj k k M)

The right scalar dual of a finite-dimensional module is finite-dimensional.

noncomputable def ModuleCat.scalarDualEvalEquiv (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] (M : ModuleCat A) [Module.Finite k ↑M] : ↑M ≃ₗ[k] Module.Dual k ↑(matlisDualObj k k M)

Evaluation pairs a finite-dimensional left module with its right scalar dual.

@[simp]

theorem ModuleCat.scalarDualEvalEquiv_apply (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] (M : ModuleCat A) [Module.Finite k ↑M] (x : ↑M) (φ : ↑(matlisDualObj k k M)) : ((scalarDualEvalEquiv k M) x) φ = ((matlisDualObjLinearEquiv k k M) φ) x

Evaluation on the right scalar dual is application of the underlying functional.

theorem ModuleCat.scalarDualEvalEquiv_smul (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] (M : ModuleCat A) [Module.Finite k ↑M] (a : A) (x : ↑M) (φ : ↑(matlisDualObj k k M)) : ((scalarDualEvalEquiv k M) (a • x)) φ = ((scalarDualEvalEquiv k M) x) (MulOpposite.op a • φ)

Evaluation respects the left action and its dual right action.