English
Nonempty order structure translates to a nontrivial, discrete, Archimedean value group structure on the extended value group in the valued relation setting.
Русский
Расширенная структура значений в рамках отношенияVALUATION образует не тривиальную дискретную Архимедову группу значений.
LaTeX
$$$ Nonempty\\ (ValueGroupWithZero R) \\Rightarrow (IsDiscrete R) \\wedge (IsNontrivial R) \\wedge (MulArchimedean (ValueGroupWithZero R)). $$$
Lean4
theorem of_compatible_withZeroMulInt (v : Valuation R ℤᵐ⁰) [v.Compatible] : IsDiscrete R :=
by
have : IsRankLeOne R := .of_compatible_mulArchimedean v
by_cases h : IsNontrivial R
· by_cases H : DenselyOrdered (ValueGroupWithZero R)
· exfalso
refine (MonoidWithZeroHom.range_nontrivial (ValueGroupWithZero.embed v)).not_subsingleton ?_
rw [← WithZero.denselyOrdered_set_iff_subsingleton]
exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
· rw [isNontrivial_iff_nontrivial_units] at h
rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H
rw [nonempty_orderIso_withZeroMul_int_iff] at H
exact H.left
· rw [isNontrivial_iff_nontrivial_units] at h; push_neg at h
refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
contrapose! hy
have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
exact Units.val_le_val.mpr this.le
