English
The canonical inclusion RatFunc(K) → K⟨X⟩ is a uniform inducing embedding.
Русский
Каноническое вложение RatFunc(K) в K⟨X⟩ является равномерно индуцирующим вложением.
LaTeX
$$$\mathrm{IsUniformInducing}(\iota: \mathrm{RatFunc}(K) \to K\langle X\rangle).$$$
Lean4
theorem inducing_coe : IsUniformInducing ((↑) : RatFunc K → K⸨X⸩) :=
by
rw [isUniformInducing_iff, Filter.comap]
ext S
simp only [Filter.mem_mk, Set.mem_setOf_eq, uniformity_eq_comap_nhds_zero, Filter.mem_comap]
constructor
· rintro ⟨T, ⟨⟨R, ⟨hR, pre_R⟩⟩, pre_T⟩⟩
obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hR
use {P : RatFunc K | Valued.v P < ↑d}
simp only [Valued.mem_nhds, sub_zero]
refine ⟨⟨d, by rfl⟩, subset_trans (fun _ _ ↦ pre_R ?_) pre_T⟩
apply hd
simp only [sub_zero, Set.mem_setOf_eq]
rw [← map_sub, valuation_def, ← valuation_eq_LaurentSeries_valuation]
assumption
· rintro ⟨_, ⟨hT, pre_T⟩⟩
obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hT
let X := {f : K⸨X⸩ | Valued.v f < ↑d}
refine ⟨(fun x : K⸨X⸩ × K⸨X⸩ ↦ x.snd - x.fst) ⁻¹' X, ⟨X, ?_⟩, ?_⟩
· refine ⟨?_, Set.Subset.refl _⟩
· simp only [Valued.mem_nhds, sub_zero]
use d
· refine subset_trans (fun _ _ ↦ ?_) pre_T
apply hd
rw [Set.mem_setOf_eq, sub_zero, v_def, valuation_eq_LaurentSeries_valuation, map_sub]
assumption
