English
There exists an order isomorphism between ValueGroupWithZero R and Z with zero if and only if R is discrete, nontrivial, and MulArchimedean on the value group.
Русский
Существует порядковый изоморфизм между ValueGroupWithZero R и Z⁰ тогда и только тогда, когда R дискретно, ненулево и значение группы является MulArchimedean.
LaTeX
$$$ Nonempty\\ (ValueGroupWithZero\\ R \\simeq_*o\\ \\mathbb{Z}^0) \\ \\Leftrightarrow\\ (IsDiscrete R) \\wedge (IsNontrivial R) \\wedge (MulArchimedean (ValueGroupWithZero R)). $$$
Lean4
theorem nonempty_orderIso_withZeroMul_int_iff :
Nonempty (ValueGroupWithZero R ≃*o ℤᵐ⁰) ↔ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) :=
by
constructor
· rintro ⟨e⟩
let x := e.symm (exp (-1))
have hx0 : x ≠ 0 := by simp [x]
have hx1 : x < 1 := by simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]
refine ⟨⟨x, hx1, fun y hy ↦ ?_⟩, ⟨x, hx0, hx1.ne⟩, .comap e.toMonoidHom e.strictMono⟩
rcases eq_or_ne y 0 with rfl | hy0
· simp
· rw [← map_one e.symm, ← map_inv_lt_iff, ← log_lt_log (by simp [hy0]) (by simp)] at hy
rw [← map_inv_le_iff, ← log_le_log (by simp [hy0]) (by simp)]
simp only [OrderMonoidIso.equivLike_inv_eq_symm, OrderMonoidIso.symm_symm, log_one, log_exp] at hy ⊢
linarith
· rintro ⟨hD, hN, hM⟩
rw [isNontrivial_iff_nontrivial_units] at hN
rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
intro H
obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element
obtain ⟨y, hy, hy'⟩ := exists_between hx
exact hy.not_ge (hx' y hy')
