English
A semilocal domain is a Principal Ideal Domain if its localizations at maximal ideals are PIDs.
Русский
Полупринципальным будет кольцо, если локализации по максимумам — ПИД.
LaTeX
$$$\\text{IsDomain}(R) \\Rightarrow (\\forall P [P.IsMaximal], IsPrincipalIdealRing(R_p)) \\Rightarrow IsPrincipalIdealRing(R)$$$
Lean4
/-- A semilocal integral domain `A` is a PID if its localization at every maximal ideal is a PID. -/
theorem isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal [IsDomain R]
(hpid : ∀ (P : Ideal R) [P.IsMaximal], IsPrincipalIdealRing (Rₚ P)) : IsPrincipalIdealRing R :=
by
have : IsNoetherianRing R := IsNoetherianRing.of_isLocalization_maximal Rₚ fun P _ => inferInstance
have : IsIntegrallyClosed R :=
by
refine IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_
have : IsDomain (Rₚ P) := IsLocalization.isDomain_of_atPrime (Rₚ P) P
infer_instance
have : Ring.KrullDimLE 1 R := Ring.krullDimLE_of_isLocalization_maximal Rₚ fun P _ => inferInstance
rw [Ring.krullDimLE_one_iff_of_noZeroDivisors] at this
have dedekind : IsDedekindDomain R := { maximalOfPrime := this _ }
have hp_finite : {P : Ideal R | P.IsMaximal}.Finite :=
by
rw [← MaximalSpectrum.range_asIdeal]
exact Set.finite_range MaximalSpectrum.asIdeal
exact IsPrincipalIdealRing.of_finite_maximals hp_finite
