English
A valued field is a completable topological field.
Русский
Ценностное поле является дополняемым (комплектуемым) топологическим полем.
LaTeX
$$$CompletableTopField(K)$$$
Lean4
/-- A valued field is completable. -/
instance (priority := 100) completable : CompletableTopField K :=
{ ValuedRing.separated with
nice := by
rintro F hF h0
have : ∃ γ₀ : Γ₀ˣ, ∃ M ∈ F, ∀ x ∈ M, (γ₀ : Γ₀) ≤ v x :=
by
rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩
rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩
exists γ₀, M, M_in
intro x xM
apply le_of_not_gt _
intro hyp
have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
rwa [H] at this
rcases this with ⟨γ₀, M₀, M₀_in, H₀⟩
rw [Valued.cauchy_iff] at hF ⊢
refine ⟨hF.1.map _, ?_⟩
replace hF := hF.2
intro γ
rcases hF (min (γ * γ₀ * γ₀) γ₀) with ⟨M₁, M₁_in, H₁⟩
clear hF
use (fun x : K => x⁻¹) '' (M₀ ∩ M₁)
constructor
· rw [mem_map]
apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)
exact subset_preimage_image _ _
· rintro _ ⟨x, ⟨x_in₀, x_in₁⟩, rfl⟩ _ ⟨y, ⟨_, y_in₁⟩, rfl⟩
simp only
specialize H₁ x x_in₁ y y_in₁
replace x_in₀ := H₀ x x_in₀
clear H₀
apply Valuation.inversion_estimate
· have : (v x : Γ₀) ≠ 0 := by
intro h
rw [h] at x_in₀
simp at x_in₀
exact (Valuation.ne_zero_iff _).mp this
· refine lt_of_lt_of_le H₁ ?_
rw [Units.min_val]
apply min_le_min _ x_in₀
rw [mul_assoc]
have : ((γ₀ * γ₀ : Γ₀ˣ) : Γ₀) ≤ v x * v x :=
calc
↑γ₀ * ↑γ₀ ≤ ↑γ₀ * v x := mul_le_mul_left' x_in₀ ↑γ₀
_ ≤ _ := mul_le_mul_right' x_in₀ (v x)
rw [Units.val_mul]
exact mul_le_mul_left' this γ }
