English
There exists π ∈ R such that v.intValuation π = -1 in the value group.
Русский
Существует π ∈ R такой, что v.intValuation(π) = -1.
LaTeX
$$\exists \pi \in R, v.intValuation(\pi) = -1$$
Lean4
/-- There exists `π ∈ R` with `v`-adic valuation `Multiplicative.ofAdd (-1)`. -/
theorem intValuation_exists_uniformizer : ∃ π : R, v.intValuation π = Multiplicative.ofAdd (-1 : ℤ) := by
classical
have hv : _root_.Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
have hlt : v.asIdeal ^ 2 < v.asIdeal := by
rw [← Ideal.dvdNotUnit_iff_lt]
exact ⟨v.ne_bot, v.asIdeal, (not_congr Ideal.isUnit_iff).mpr (Ideal.IsPrime.ne_top v.isPrime), sq v.asIdeal⟩
obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
have hπ : Associates.mk (Ideal.span { π }) ≠ 0 :=
by
rw [Associates.mk_ne_zero']
intro h
rw [h] at notMem
exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
use π
rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), WithZero.coe_inj]
apply congr_arg
rw [neg_inj, ← Int.ofNat_one, Int.natCast_inj]
rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
exact Nat.eq_of_le_of_lt_succ mem notMem
