English
If the valuation ring is compact, then it is a principal ideal ring.
Русский
Если кольцо оценки компактно, то оно имеет главные идеалы.
LaTeX
$$$$ 𝒪_K \text{ is a principal ideal ring}. $$$$
Lean4
theorem isPrincipalIdealRing_of_compactSpace [hc : CompactSpace 𝒪[K]] : IsPrincipalIdealRing 𝒪[K] := by
-- The strategy to show that we have a PIR is by contradiction,
-- assuming that the range of the valuation is densely ordered.
have hi : Valuation.Integers (R := K) Valued.v 𝒪[K] := Valuation.integer.integers v
have hc : IsCompact (X := K) 𝒪[K] := isCompact_iff_compactSpace.mpr hc
obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc
have hm := mulArchimedean_mrange_of_isCompact_integer hc
refine
hi.isPrincipalIdealRing_iff_not_denselyOrdered_mrange.mpr fun _ ↦
?_
-- since we are densely ordered, we necessarily are nontrivial
exact
not_subsingleton (MonoidHom.mrange (v : Valuation K Γ₀))ˣ
(LocallyFiniteOrder.denselyOrdered_iff_subsingleton.mp inferInstance)
