English
In a nonarchimedean local field, every closed ball around 0 with any radius is compact.
Русский
В неархимедовом локальном поле вся замкнутая шарa вокруг 0 с любым радиусом компактна.
LaTeX
$$$$\{x\in K : v(x) \le \gamma\} \text{ is compact for all } \gamma.$$$$
Lean4
theorem isCompact_closedBall (γ : ValueGroupWithZero K) : IsCompact {x | valuation K x ≤ γ} :=
by
obtain ⟨γ, rfl⟩ := ValuativeRel.valuation_surjective γ
by_cases hγ : γ = 0
· simp [hγ]
letI := IsTopologicalAddGroup.toUniformSpace K
letI := isUniformAddGroup_of_addCommGroup (G := K)
obtain ⟨s, hs, -, hs'⟩ := LocallyCompactSpace.local_compact_nhds (0 : K) .univ Filter.univ_mem
obtain ⟨r, hr, hr1, H⟩ : ∃ r', r' ≠ 0 ∧ valuation K r' < 1 ∧ {x | valuation K x ≤ valuation K r'} ⊆ s :=
by
obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs
obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)
simp only [ne_eq, map_eq_zero] at hr'
obtain hr1 | hr1 := lt_or_ge r 1
· obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r
simp only [ne_eq, map_eq_zero] at hr
refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩
simp only [map_pow, Set.mem_setOf_eq] at hx ⊢
exact hx.trans_lt (by simpa [pow_two, hr])
· refine ⟨r', hr', hr, .trans ?_ hrs⟩
intro x hx
dsimp at hx ⊢
exact hx.trans_lt (hr.trans_le hr1)
convert
(hs'.of_isClosed_subset (Valued.isClosed_closedBall K _) H).image
(Homeomorph.mulLeft₀ (γ / r) (by simp [hr, div_eq_zero_iff, hγ])).continuous using
1
refine .trans ?_ (Equiv.image_eq_preimage _ _).symm
ext x
simp [div_mul_eq_mul_div, div_le_iff₀, IsValuativeTopology.v_eq_valuation, hγ, hr]
