English
For any x in the unit group of A, x lies in the principal unit group if and only if its image under the local residue map lies in the kernel of the corresponding map on units.
Русский
Для любого элемента x из группы единиц A верно, что x лежит в главной группе единиц тогда и только тогда, когда его образ через локальное резидуальное отображение лежит в ядре соответствующего отображения единиц.
LaTeX
$$$\forall A:\mathrm{ValuationSubring}(K),\forall x:\mathrm{A.unitGroup},\ (x \in A.principalUnitGroup) \iff x \in \ker\big( (\mathrm{Units.map} (\mathrm{IsLocalRing.residue}(A)).toMonoidHom) \\circ A.unitGroupMulEquiv\big)$$$
Lean4
theorem coe_mem_principalUnitGroup_iff {x : A.unitGroup} :
(x : Kˣ) ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map (IsLocalRing.residue A).toMonoidHom).ker :=
by
rw [MonoidHom.mem_ker, Units.ext_iff]
let π := Ideal.Quotient.mk (IsLocalRing.maximalIdeal A); convert_to _ ↔ π _ = 1
rw [← π.map_one, ← sub_eq_zero, ← π.map_sub, Ideal.Quotient.eq_zero_iff_mem, valuation_lt_one_iff]
simp [mem_principalUnitGroup_iff]
