tendsto_valuation — Mathlib

English

The valuation map from RatFunc K extends continuously to the adic completion, yielding a limit behavior that matches the target valuation at the limit point.

Русский

Мапа ценности от RatFunc K продолжается непрерывно до адической завершения, давая предел, совпадающий с ценностью в пределе.

LaTeX

$$$\\mathrm{Tendsto}\\bigl(\\mathrm{Valued.v}: \\mathrm{RatFunc} K \\to \\mathbb{Z}^{\\mathbf{0}}\\bigr)\\; (\\mathrm{comap}\\, (\\mathrm{\\iota},\\,\\mathcal{N}_a))\\; (\\mathcal{N}_{\\mathrm{Valued.v}(a)})$$$

Lean4

theorem tendsto_valuation (a : (idealX K).adicCompletion (RatFunc K)) :
    Tendsto (Valued.v : RatFunc K → ℤᵐ⁰) (comap (↑) (𝓝 a)) (𝓝 (Valued.v a : ℤᵐ⁰)) :=
  by
  have := Valued.is_topological_valuation (R := (idealX K).adicCompletion (RatFunc K))
  by_cases ha : a = 0
  · rw [tendsto_def]
    intro S hS
    rw [ha, map_zero, WithZeroTopology.hasBasis_nhds_zero.1 S] at hS
    obtain ⟨γ, γ_ne_zero, γ_le⟩ := hS
    use {t | Valued.v t < γ}
    constructor
    · rw [ha, this]
      use Units.mk0 γ γ_ne_zero
      rw [Units.val_mk0]
    · refine Set.Subset.trans (fun a _ ↦ ?_) (Set.preimage_mono γ_le)
      rwa [Set.mem_preimage, Set.mem_Iio, ← Valued.valuedCompletion_apply a]
  · rw [WithZeroTopology.tendsto_of_ne_zero ((Valuation.ne_zero_iff Valued.v).mpr ha), Filter.eventually_comap,
      Filter.Eventually, Valued.mem_nhds]
    use Units.mk0 (Valued.v a) (by simp [ha])
    simp only [Units.val_mk0, v_def, Set.setOf_subset_setOf]
    rintro y val_y b rfl
    simp [← Valuation.map_eq_of_sub_lt _ val_y]
      /- The extension of the `X`-adic valuation from `RatFunc K` up to its abstract completion coincides,
      modulo the isomorphism with `K⸨X⸩`, with the `X`-adic valuation on `K⸨X⸩`. -/

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