valuedCompletion — Mathlib

English

The valuation on hat K is surjective iff the valuation on K is surjective.

Русский

Оценка на hat K сюръективна тогда и только тогда, когда оценка на K сюръективна.

LaTeX

$$$Function.Surjective(v: hat{K} \to Γ_0) \;\Leftrightarrow\; Function.Surjective(v: K \to Γ_0)$$$

Lean4

noncomputable instance valuedCompletion : Valued (hat K) Γ₀
    where
  v := extensionValuation
  is_topological_valuation
    s :=
    by
    suffices HasBasis (𝓝 (0 : hat K)) (fun _ => True) fun γ : Γ₀ˣ => {x | extensionValuation x < γ}
      by
      rw [this.mem_iff]
      exact exists_congr fun γ => by simp
    simp_rw [← closure_coe_completion_v_lt]
    exact (hasBasis_nhds_zero K Γ₀).hasBasis_of_isDenseInducing Completion.isDenseInducing_coe

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