English
For a valuation v on R with value group Γ₀, there exists rank-one structure on v if and only if Γ₀ is MulArchimedean. In particular, Nonempty v.RankOne is equivalent to MulArchimedean Γ₀.
Русский
Для оценки v на кольце R с группой значений Γ₀ существование структуры ранга один для v эквивалентно тому, что Γ₀ является MulArchimedean. В частности, существует ранг одна для v тогда и только тогда, когда Γ₀ — MulArchimedean.
LaTeX
$$$\text{Nonempty } v.\mathrm{RankOne} \iff \operatorname{MulArchimedean}(\Gamma_0).$$$
Lean4
theorem nonempty_rankOne_iff_mulArchimedean {v : Valuation R Γ₀} [v.IsNontrivial] :
Nonempty v.RankOne ↔ MulArchimedean Γ₀ := by
constructor
· rintro ⟨⟨f, hf⟩⟩
exact .comap f.toMonoidHom hf
· intro _
obtain ⟨f, hf⟩ := Archimedean.exists_orderAddMonoidHom_real_injective (Additive Γ₀ˣ)
let e := AddMonoidHom.toMultiplicativeRight (α := Γ₀ˣ) (β := ℝ) f
have he : StrictMono e :=
by
simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
-- toAdd_strictMono is already in an applied form, do defeq abuse instead
exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)
let rf : Multiplicative ℝ →* ℝ≥0ˣ :=
{ toFun
x :=
Units.mk0 ⟨(2 : ℝ) ^ (log (M := ℝ) x), by positivity⟩ <|
by
rw [ne_eq, Subtype.ext_iff]
positivity
map_one' := by simp
map_mul' _
_ := by
rw [Units.ext_iff, Subtype.ext_iff]
simp [log_mul, Real.rpow_add] }
have H : StrictMono (map' (rf.comp e)) := by
refine map'_strictMono ?_
intro a b h
simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h
exact
⟨{ hom :=
withZeroUnitsEquiv.toMonoidWithZeroHom.comp <|
(map' (rf.comp e)).comp withZeroUnitsEquiv.symm.toMonoidWithZeroHom
strictMono' := withZeroUnitsEquiv_strictMono.comp <| H.comp withZeroUnitsEquiv_symm_strictMono }⟩
