English
Let I be a submodule of L over B. Then an element x of L lies in the trace-dual Iᵛ if and only if, for every a in I, the trace form Tr(x,a) belongs to the image of A under the algebra homomorphism A → K. In other words, x ∈ Iᵛ ⇔ ∀ a ∈ I, traceForm K L (x,a) ∈ im(algebraMap A K).
Русский
Пусть I будет подмодулем L над B. Тогда элемент x ∈ L принадлежит следовой дуальности Iᵛ тогда и только тогда, когда для любого a ∈ I трейс-функция traceForm(x,a) лежит в образе A в K через алгебраическую вложенность A → K.
LaTeX
$$$x \in I^\vee \iff \forall a \in I,\; \operatorname{traceForm}_{K L}(x,a) \in \operatorname{range}(\operatorname{algebraMap}_{A K}).$$$
Lean4
theorem mem_traceDual {I : Submodule B L} {x} : x ∈ Iᵛ ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range :=
forall₂_congr fun _ _ ↦ mem_one
