continuous_valuation — Mathlib

English

The valuation-based topology is compatible with ring homomorphisms preserving valuation structure.

Русский

Топология, заданная оценкой, совместима с гомоморфизмами колец, сохраняющими структуру оценки.

LaTeX

$$$\varphi:R\to R' \text{ ring homomorphism with } v'\circ\varphi = v$$$

Lean4

theorem continuous_valuation : Continuous v :=
  by
  simp only [continuous_iff_continuousAt, ContinuousAt]
  rintro x
  by_cases hx : v x = 0
  ·
    simpa [hx, (hasBasis_nhds _).tendsto_iff WithZeroTopology.hasBasis_nhds_zero,
      Valuation.map_sub_of_right_eq_zero _ hx] using fun i hi ↦ ⟨.mk0 i hi, fun y ↦ id⟩
  ·
    simpa [(hasBasis_nhds _).tendsto_iff (WithZeroTopology.hasBasis_nhds_of_ne_zero hx)] using
      ⟨.mk0 (v x) hx, fun _ ↦ Valuation.map_eq_of_sub_lt _⟩

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