English
In a valuation setting with integers over O, IsPrincipalIdealRing O is equivalent to the negation of densely ordered behavior of the value group range.
Русский
В настройке оценки с целыми над O, IsPrincipalIdealRing O эквивалентно тому, что диапазон значений не плотный по порядку.
LaTeX
$$$\\mathrm{IsPrincipalIdealRing}\\; O \\; \\iff \\; \\neg \\mathrm{DenselyOrdered}\\; (\\mathrm{range}(v)).$$$
Lean4
theorem isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean (MonoidHom.mrange v)] (hv : Integers v O) :
IsPrincipalIdealRing O ↔ ¬DenselyOrdered (Set.range v) :=
by
refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩
rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _
· have := bijective_algebraMap_of_subsingleton_units_mrange hv
exact .of_surjective _ (RingEquiv.ofBijective _ this).symm.surjective
have : IsDomain O := hv.hom_inj.isDomain
have : ValuationRing O := ValuationRing.of_integers v hv
have : IsBezout O := ValuationRing.instIsBezout
have := ((IsBezout.TFAE (R := O)).out 1 3)
rw [this, hv.wfDvdMonoid_iff_wellFounded_gt_on_v, hv.wellFounded_gt_on_v_iff_discrete_mrange,
LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
exact H
