English
In a linearly ordered commutative group with zero, discreteness is equivalent to not being densely ordered when units are considered with zero.
Русский
В линейно упорядоченной коммутативной группе с нулем дискретность эквивалентна тому, что порядок не плотный, если учитывать нули и единицы.
LaTeX
$$$(\exists \phi: G \cong_o \mathbb{Z}^{\mathbf{m0}}) \iff \lnot \mathrm{DenselyOrdered}(G)$$$
Lean4
/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
either isomorphic (and order-isomorphic) to `ℤᵐ⁰`, or is densely ordered, exclusively -/
theorem discrete_iff_not_denselyOrdered (G : Type*) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ]
[MulArchimedean G] : Nonempty (G ≃*o ℤᵐ⁰) ↔ ¬DenselyOrdered G :=
by
rw [← denselyOrdered_units_iff, ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]
refine Nonempty.congr ?_ ?_ <;> intro f
· refine ⟨MulEquiv.withZero.symm (withZeroUnitsEquiv.trans f), ?_⟩
intros
simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk,
recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv, MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk,
map_eq_zero, coe_ne_zero, ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]
· refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
intros
simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
EquivLike.coe_coe, MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
split_ifs <;> simp_all [← Units.val_le_val]
