English
Under discrete range assumptions, the well-foundedness of the GT order on v ∘ algebraMap O F is equivalent to the existence of a nontrivial isomorphism between the valuation range and the integers.
Русский
При дискретном образе последовательность неразложимости, хорошо упорядованность GT над v ∘ algebraMap ՕF эквивалентна существованию ненулевого изоморфизма между диапазоном оценки и целыми числами.
LaTeX
$$$\\mathrm{WellFounded}\\; ((\\cdot > \\cdot) \\text{ on } (v \\circ \\mathrm{algebraMap}\\; O\\; F)) \\iff \\mathrm{Nonempty} (\\mathrm{MonoidHom} \\; \\text{mrange } v \\; \\cong_*\\mathbb{Z}).$$$
Lean4
theorem wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ] (hv : Integers v O) :
WellFounded ((· > ·) on (v ∘ algebraMap O F)) ↔ Nonempty (MonoidHom.mrange v ≃*o ℤᵐ⁰) :=
by
rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero one_ne_zero, ←
Set.wellFoundedOn_range]
classical
refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
· rintro ⟨_, x, rfl⟩
simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range, Function.comp_apply]
intro hx
obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
exact ⟨y, by simp⟩
· exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
· intro
simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq, forall_exists_index]
rintro x rfl
simp [← Subtype.coe_le_coe, hv.map_le_one]
· simp [Function.onFun]
