English
The underlying submodule of the different ideal equals the inverse of the dual of the unit ideal: ↑(differentIdeal(A,B)) = (dual(A,K,1))^{-1}.
Русский
Основанный подмодуль различного идеала равен обратному двойственной единицы: ↑(differentIdeal(A,B)) = (dual(A,K,1))^{-1}.
LaTeX
$$\uparrow(\mathrm{differentIdeal}(A,B)) = (\mathrm{dual}_{A,K}(1))^{-1}$$
Lean4
/-- The different ideal of an extension of integral domains `B/A` is the inverse of the dual of `A`
as an ideal of `B`. See `coeIdeal_differentIdeal` and `coeSubmodule_differentIdeal`. -/
noncomputable def differentIdeal : Ideal B :=
(1 / Submodule.traceDual A (FractionRing A) 1 : Submodule B (FractionRing B)).comap
(Algebra.linearMap B (FractionRing B))
