English
For any x in K0, the image under algebraMap to L0 lies in the maximal ideal of L0 iff x lies in the maximal ideal of K0.
Русский
Для любого x в K0 образ через algebraMap в L0 лежит в максимальном идеале L0 тогда и только тогда, когда x лежит в максимальном идеале K0.
LaTeX
$$$\\forall x: K_0,\\ algebraMap_{K_0,L_0}(x) \\in \\mathfrak{m}_{L_0} \\iff x \\in \\mathfrak{m}_{K_0}$$$
Lean4
/-- Let `O` be the integers of the valuation `v` on some commutative ring `R`. For every element `x` in
`O`, `x` is a unit in `O` if and only if the image of `x` in `R` is a unit and has valuation 1.
-/
theorem isUnit_of_one (hv : Integers v O) {x : O} (hx : IsUnit (algebraMap O R x)) (hvx : v (algebraMap O R x) = 1) :
IsUnit x :=
let ⟨u, hu⟩ := hx
have h1 : v u ≤ 1 := hu.symm ▸ hv.2 x
have h2 : v (u⁻¹ : Rˣ) ≤ 1 := by rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
let ⟨r1, hr1⟩ := hv.3 h1
let ⟨r2, hr2⟩ := hv.3 h2
⟨⟨r1, r2, hv.1 <| by rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.mul_inv],
hv.1 <| by rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.inv_mul]⟩,
hv.1 <| hr1.trans hu⟩
