English
For valuation subrings A,B of K, A ≤ B if and only if A.unitGroup ≤ B.unitGroup.
Русский
Для подкольц A,B ценности K: A ≤ B тогда и только тогда, когда A.unitGroup ≤ B.unitGroup.
LaTeX
$$$A \le B \;\Longleftrightarrow\; A_{\mathrm{unitGroup}} \le B_{\mathrm{unitGroup}}$$$
Lean4
theorem unitGroup_le_unitGroup {A B : ValuationSubring K} : A.unitGroup ≤ B.unitGroup ↔ A ≤ B :=
by
constructor
· intro h x hx
rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx
by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
by_cases h_2 : 1 + x = 0
· simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]
rcases hx with hx | hx
· have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
simpa using
B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)) (B.neg_mem _ B.one_mem)
· have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)
· rintro h x (hx : A.valuation x = 1)
apply_fun A.mapOfLE B h at hx
simpa using hx
