isDiscreteValuationRing_of_compactSpace

English

If the valuation ring is compact and the valuation is rank one, then the ring is a discrete valuation ring.

Русский

Если кольцо оценки компактно и валюация имеет ранг один, то кольцо является дискретным кольцом оценки.

LaTeX

$$$$ \text{If } 𝒪_K \text{ is compact and } (v: \mathcal{K}) \text{ has RankOne, then } 𝒪_K \text{ is a DVR}. $$$$

Lean4

theorem isDiscreteValuationRing_of_compactSpace [hn : (Valued.v : Valuation K Γ₀).IsNontrivial] [CompactSpace 𝒪[K]] :
    IsDiscreteValuationRing 𝒪[K] where
  -- To prove we have a DVR, we need to show it is
    -- a local ring (instance is directly inferred) and a PIR and not a field.

  __ := isPrincipalIdealRing_of_compactSpace
  not_a_field' := v.isNontrivial_iff_not_a_field.mp hn

Похожие утверждения