English
Let K be a field with a valuation v into Γ₀. The surjectivity of the valuation on the completion ŷK is equivalent to the surjectivity of the valuation on K itself.
Русский
Пусть K — поле с valuations в Γ₀. Сюръективность отображения v на завершении ŷK эквивалентна сюръективности v на самом K.
LaTeX
$$$\\operatorname{Surjective}(v: \\hat K \\to \\Gamma_0) \\iff \\operatorname{Surjective}(v: K \\to \\Gamma_0)$$$
Lean4
theorem valuedCompletion_surjective_iff : Function.Surjective (v : hat K → Γ₀) ↔ Function.Surjective (v : K → Γ₀) :=
by
constructor <;> intro h γ <;> obtain ⟨a, ha⟩ := h γ
· induction a using Completion.induction_on
· by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
· simp [H]
· simp only [H, imp_false]
rcases eq_or_ne γ 0 with rfl | hγ
· simp at H
· convert isClosed_univ.sdiff (isOpen_sphere (hat K) hγ) using 1
ext x
simp
· exact ⟨_, by simpa using ha⟩
· exact ⟨a, by simp [ha]⟩
