English
Let Γ be a linearly ordered commutative group with zero and v a rank-one discrete valuation on a field K. If the maximal ideal of the valuation subring is generated by an element r (i.e., maxIdeal equals span{r}), then r is a uniformizer for v.
Русский
Пусть Γ — линейно упорядоченная коммутативная группа с нулём, а v — ранговая дискретная оценка на поле K. Если максимальный идеал подкольца оценки равен порождающей единице, порождённой элементом r (макс. идеал = span{r}), тогда r является униформизатором для v.
LaTeX
$$$ [v.IsRankOneDiscrete] \\land (\\maximalIdeal v.valuationSubring = \\operatorname{span} \\{ r \\}) \\ \\Rightarrow\\ \\ IsUniformizer\\ v\\ r. $$$
Lean4
theorem isUniformizer_of_maximalIdeal_eq_span [v.IsRankOneDiscrete] {r : K₀}
(hr : maximalIdeal v.valuationSubring = Ideal.span { r }) : IsUniformizer v r :=
by
have hr₀ : r ≠ 0 := by
intro h
rw [h, Set.singleton_zero, span_zero] at hr
exact
Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
(valuationSubring_not_isField v) hr
obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩
rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr
exact hπ.of_associated hr
