English
For all x ∈ K, extension (x) = v(x).
Русский
Для всех x ∈ K, extension(x) = v(x).
LaTeX
$$$extension(x) = v(x) \quad (x \in K)$$$
Lean4
/-- the extension of a valuation on a division ring to its completion. -/
noncomputable def extensionValuation : Valuation (hat K) Γ₀
where
toFun := Valued.extension
map_zero' := by
rw [← v.map_zero (R := K), ← Valued.extension_extends (0 : K)]
rfl
map_one' := by
rw [← Completion.coe_one, Valued.extension_extends (1 : K)]
exact Valuation.map_one _
map_mul' x
y := by
apply Completion.induction_on₂ x y (p := fun x y => extension (x * y) = extension x * extension y)
· have c1 : Continuous fun x : hat K × hat K => Valued.extension (x.1 * x.2) :=
Valued.continuous_extension.comp (continuous_fst.mul continuous_snd)
have c2 : Continuous fun x : hat K × hat K => Valued.extension x.1 * Valued.extension x.2 :=
(Valued.continuous_extension.comp continuous_fst).mul (Valued.continuous_extension.comp continuous_snd)
exact isClosed_eq c1 c2
· intro x y
norm_cast
exact Valuation.map_mul _ _ _
map_add_le_max' x
y := by
rw [le_max_iff]
apply
Completion.induction_on₂ x y (p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)
· have cont : Continuous (Valued.extension : hat K → Γ₀) := Valued.continuous_extension
exact
(isClosed_le (cont.comp continuous_add) <| cont.comp continuous_fst).union
(isClosed_le (cont.comp continuous_add) <| cont.comp continuous_snd)
· intro x y
norm_cast
rw [← le_max_iff]
exact v.map_add x y
