English
If I is a fractional ideal, then the underlying submodule is principal (noetherian context assumed).
Русский
Если I — дробный идеал, то соответствующий подмодуль порожден одним элементом (при условии существующих предпосылок).
LaTeX
$$I : FractionalIdeal R⁰ K, (I : Submodule R K).IsPrincipal$$
Lean4
instance isPrincipal {R} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Algebra R K] [IsFractionRing R K]
(I : FractionalIdeal R⁰ K) : (I : Submodule R K).IsPrincipal :=
by
obtain ⟨a, aI, -, ha⟩ := exists_eq_spanSingleton_mul I
use (algebraMap R K a)⁻¹ * algebraMap R K (generator aI)
suffices I = spanSingleton R⁰ ((algebraMap R K a)⁻¹ * algebraMap R K (generator aI))
by
rw [spanSingleton] at this
exact congr_arg Subtype.val this
conv_lhs => rw [ha, ← span_singleton_generator aI]
rw [Ideal.submodule_span_eq, coeIdeal_span_singleton (generator aI), spanSingleton_mul_spanSingleton]
