English
Let R be a Dedekind domain, S an extension, p a prime of R; the localization S_p is a principal ideal domain.
Русский
Пусть R — Дедекинд домен, S — расширение, p — простой над R; локализация S_p — главный идеал-домен.
LaTeX
$$$$\\text{IsPrincipalIdealRing}(S_p)$$$$
Lean4
/-- Let `p` be a prime in the Dedekind domain `R` and `S` be an integral extension of `R`,
then the localization `Sₚ` of `S` at `p` is a PID. -/
theorem isPrincipalIdealRing_localization_over_prime [IsDomain S] : IsPrincipalIdealRing Sₚ :=
by
letI := Classical.decEq (Ideal Sₚ)
letI := Classical.decPred fun P : Ideal Sₚ => P.IsPrime
refine
IsPrincipalIdealRing.of_finite_primes
(Set.Finite.ofFinset ({P ∈ {⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset | P.IsPrime})
fun P => ?_)
rw [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton, Set.mem_setOf, Multiset.mem_toFinset]
exact
and_iff_right_of_imp fun hP =>
or_iff_not_imp_left.mpr (IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime S p hp0 hP)
