English
The dualSubmoduleToDual is the natural linear map sending each x in B.dualSubmodule N to the functional on N defined by y ↦ B(x,y).
Русский
Функционал dualSubmoduleToDual отправляет x в B.dualSubmodule N в функционал на N, задаваемый y ↦ B(x,y).
LaTeX
$$$$ B.dualSubmoduleToDual(N)\;: B.dualSubmodule N \to \mathrm{Module.Dual}_R N,\quad x \mapsto (y \mapsto B(x,y)). $$$$
Lean4
/-- The natural paring of `B.dualSubmodule N` and `N`. -/
-- TODO: Show that this is perfect when `N` is a lattice and `B` is nondegenerate.
@[simps]
noncomputable def dualSubmoduleToDual [NoZeroSMulDivisors R S] (N : Submodule R M) :
B.dualSubmodule N →ₗ[R] Module.Dual R N :=
{ toFun := fun x ↦
{ toFun := B.dualSubmoduleParing x
map_add' := fun x y ↦ FaithfulSMul.algebraMap_injective R S (by simp)
map_smul' := fun r m ↦ FaithfulSMul.algebraMap_injective R S (by simp [← Algebra.smul_def]) }
map_add' := fun x y ↦ LinearMap.ext fun z ↦ FaithfulSMul.algebraMap_injective R S (by simp)
map_smul' := fun r x ↦ LinearMap.ext fun y ↦ FaithfulSMul.algebraMap_injective R S (by simp [← Algebra.smul_def]) }
