English
In rank-one valued fields, compactness of 𝒪[K] is equivalent to being a complete space, a discrete valuation ring, and having finite residue field.
Русский
Для поля с оценкой ранга один компактность 𝒪[K] эквивалентна тому, что это полное пространство, дискретное кольцо оценки и конечное остаточное поле.
LaTeX
$$$$ \text{For RankOne valuations } 1) 𝒪_K \text{ is compact } \iff 2) (CompleteSpace 𝒪_K) \land (IsDiscreteValuationRing 𝒪_K) \land (Finite 𝓀[K]). $$$$
Lean4
theorem compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField
[(Valued.v : Valuation K Γ₀).RankOne] :
CompactSpace 𝒪[K] ↔ CompleteSpace 𝒪[K] ∧ IsDiscreteValuationRing 𝒪[K] ∧ Finite 𝓀[K] :=
by
refine ⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩
· have : IsDiscreteValuationRing 𝒪[K] := isDiscreteValuationRing_of_compactSpace
refine ⟨complete_of_compact, by assumption, ?_⟩
rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete, totallyBounded_iff_finite_residueField] at h
exact h.left
· rw [← totallyBounded_iff_finite_residueField] at h
rw [isCompact_iff_totallyBounded_isComplete]
exact ⟨h, completeSpace_iff_isComplete_univ.mp ‹_›⟩
