English
In a rank-one discrete valuation, the maximal ideal of the valuation subring is generated by a uniformizer.
Русский
В дискретной оценке ранга один максимальный идеал подкольца значения образуется униформизатором.
LaTeX
$$$\operatorname{maximalIdeal}(v.valuationSubring) = \operatorname{span}\{ \pi \}.$$$
Lean4
theorem is_generator (π : Uniformizer v) : maximalIdeal v.valuationSubring = Ideal.span { π.1 } :=
by
apply (maximalIdeal.isMaximal _).eq_of_le
· intro h
rw [Ideal.span_singleton_eq_top] at h
apply π.2.not_isUnit h
· intro x hx
by_cases hx₀ : x = 0
· simp [hx₀]
· obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
rw [← Subring.coe_mul, Subtype.coe_inj] at hu
have hn : Not (IsUnit x) := fun h ↦ (maximalIdeal.isMaximal _).ne_top (eq_top_of_isUnit_mem _ hx h)
replace hn : n ≠ 0 := fun h ↦ by simp only [hu, h, pow_zero, one_mul, Units.isUnit, not_true] at hn
simp [Ideal.mem_span_singleton, hu, dvd_pow_self _ hn]
