English
Let R be a Dedekind domain, S an extension, p a prime ideal in R, then the localization S_p is a principal ideal ring provided finiteness of maximal ideals and coprimality conditions hold.
Русский
Пусть R — Дедекинд домен, S — расширение, p — простой идеал в R; тогда локализация S_p — кольцо главных идеалов при выполнении условий конечности максимальных идеалов и относительной взаимной неприводимости.
LaTeX
$$$$\\text{IsPrincipalIdealRing}(S_{p})$$$$
Lean4
theorem isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
{S : Submonoid R} [IsLocalization S A] (I : (FractionalIdeal S A)ˣ) {v : A} (hv : v ∈ (↑I⁻¹ : FractionalIdeal S A))
(h : Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R { v }) = ⊤) :
Submodule.IsPrincipal (I : Submodule R A) :=
by
have hinv := I.mul_inv
set J := Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R { v })
have hJ : IsLocalization.coeSubmodule A J = ↑I * Submodule.span R { v } :=
by
rw [coe_ext_iff, coe_mul, coe_one] at hinv
apply Submodule.map_comap_eq_self
rw [← Submodule.one_eq_range, ← hinv]
exact mul_le_mul_left' ((Submodule.span_singleton_le_iff_mem _ _).2 hv) _
have : (1 : A) ∈ ↑I * Submodule.span R { v } :=
by
rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
exact ⟨1, (algebraMap R _).map_one⟩
obtain ⟨w, hw, hvw⟩ := Submodule.mem_mul_span_singleton.1 this
refine ⟨⟨w, ?_⟩⟩
rw [← FractionalIdeal.coe_spanSingleton S, ← inv_inv I, eq_comm]
refine congr_arg coeToSubmodule (Units.eq_inv_of_mul_eq_one_left (le_antisymm ?_ ?_))
· conv_rhs => rw [← hinv, mul_comm]
apply mul_le_mul_left' (FractionalIdeal.spanSingleton_le_iff_mem.mpr hw)
· rw [FractionalIdeal.one_le, ← hvw, mul_comm]
exact FractionalIdeal.mul_mem_mul (FractionalIdeal.mem_spanSingleton_self _ _) hv
