English
For a bilinear form B: S-linear on M and a submodule N of M (over R), the dualSubmodule N is the submodule of M consisting of all x with B(x,y) ∈ 1_S for every y ∈ N.
Русский
Относительно билинейной формы B: S-модуля M и подмодуля N ⊆ M, дуальная подмодуля N — это множество всех x в M, удовлетворяющих B(x,y) ∈ 1_S для всех y ∈ N.
LaTeX
$$$$ \mathrm{dualSubmodule}_B(N) = \{ x \in M \mid \forall y \in N,\ B(x,y) \in 1_S \}. $$$$
Lean4
/-- The dual submodule of a submodule with respect to a bilinear form. -/
def dualSubmodule (N : Submodule R M) : Submodule R M
where
carrier := {x | ∀ y ∈ N, B x y ∈ (1 : Submodule R S)}
add_mem' {a b} ha hb y hy := by simpa using add_mem (ha y hy) (hb y hy)
zero_mem' y _ := by rw [B.zero_left]; exact zero_mem _
smul_mem' r a ha y
hy := by
convert (1 : Submodule R S).smul_mem r (ha y hy)
rw [← IsScalarTower.algebraMap_smul S r a]
simp only [algebraMap_smul, map_smul_of_tower, LinearMap.smul_apply]
