English
For a nonzero fractional ideal I, the image of its denominator I.den under the structure map to the ambient field lies in the inverse fractional ideal I^{-1}.
Русский
Для недопустимого по нулю дробного идеала I образ деноминаатора I.den через вложение в K принадлежит к I^{-1}.
LaTeX
$$(algebraMap R_1 K)(I.den) \\in I^{-1}$$
Lean4
theorem den_mem_inv {I : FractionalIdeal R₁⁰ K} (hI : I ≠ ⊥) : (algebraMap R₁ K) (I.den : R₁) ∈ I⁻¹ :=
by
rw [mem_inv_iff hI]
intro i hi
rw [← Algebra.smul_def (I.den : R₁) i, ← mem_coe, coe_one]
suffices Submodule.map (Algebra.linearMap R₁ K) I.num ≤ 1 from
this <| (den_mul_self_eq_num I).symm ▸ smul_mem_pointwise_smul i I.den I.coeToSubmodule hi
apply le_trans <| map_mono (show I.num ≤ 1 by simp only [Ideal.one_eq_top, le_top])
rw [Ideal.one_eq_top, Submodule.map_top, one_eq_range]
