English
Under a suitable algebra isomorphism between FractionRing B L and K, the trace-dual commutes with the corresponding algebra equivalence: the map of traceDual equals traceDual after mapping I along the equivalence.
Русский
При подходящем изоморфизме дробной идеализации между FractionRing B L и K, дуальность по следу commute с соответствующим алгебраическим эквивалентом: отображение traceDual эквивалентно traceDual после отображения I через эквивалент.
LaTeX
$$$(\operatorname{traceDual} A (\operatorname{FractionRing} A) I).map (\operatorname{FractionRing}.algEquiv B L) = \operatorname{traceDual} A K (I.map (\operatorname{FractionRing}.algEquiv B L)).$$$
Lean4
@[simp]
theorem restrictScalars_traceDual {I : Submodule B L} :
Iᵛ.restrictScalars A = (Algebra.traceForm K L).dualSubmodule (I.restrictScalars A) :=
rfl
