English
For a field 𝕜 and a subset S of M closed under scalar multiplication, polarSubmodule 𝕜 S is the submodule of StrongDual 𝕜 M consisting of those functionals that evaluate to zero on every element of S.
Русский
Для поля 𝕜 и подмножества S ⊆ M, замкнутого по скалярному умножению, polarSubmodule 𝕜 S есть подмодуль StrongDual 𝕜 M, состоящий из функционалов, которые обнуляются на каждом элементе S.
LaTeX
$$$\operatorname{polarSubmodule}_{\mathbb{K}}(S) = \{\, \ell \in \mathrm{StrongDual}_{\mathbb{K}}(M) \mid \forall z \in S, \ell(z) = 0 \} \,$$$
Lean4
/-- Given a subset `s` in a monoid `M` (over a field `𝕜`) closed under scalar multiplication,
the polar `polarSubmodule 𝕜 s` is the submodule of `StrongDual 𝕜 M` consisting of those functionals
which evaluate to zero at all points `z ∈ s`. -/
def polarSubmodule (𝕜 : Type*) [NontriviallyNormedField 𝕜] {M : Type*} [AddCommMonoid M] [TopologicalSpace M]
[Module 𝕜 M] {S : Type*} [SetLike S M] [SMulMemClass S 𝕜 M] (m : S) : Submodule 𝕜 (StrongDual 𝕜 M) :=
(topDualPairing 𝕜 M).flip.polarSubmodule m
