English
Let I and J be submodules of L over B. Then I is contained in the trace-dual of J if and only if the image, under the trace map after multiplying I and J, is contained in the unit submodule. Formally, I ≤ Jᵛ ↔ ((I * J) restricted to A) mapped by trace equals ≤ 1.
Русский
Пусть I и J — подмодули L над B. Тогда I содержится вtraceDual(J) тогда и только тогда, когда образ IJ подtrace карты после умножения I и J лежит в единичной подмодуля, то есть IJ⋅trace ≤ 1.
LaTeX
$$$I \le J^\vee \;\iff\; ((I \cdot J : Submodule B L).\text{restrictScalars } A).map((\operatorname{trace} K L).\text{restrictScalars } A) \le 1.$$$
Lean4
theorem le_traceDual_iff_map_le_one {I J : Submodule B L} :
I ≤ Jᵛ ↔ ((I * J : Submodule B L).restrictScalars A).map ((trace K L).restrictScalars A) ≤ 1 :=
by
rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]
simp [SetLike.le_def, mem_traceDual]
