English
Exists isUniformizer for a nontrivial cyclic value group case.
Русский
Существование uniformizer в случае ненулевой цикличной группы значений.
LaTeX
$$∃ π, v.IsUniformizer π$$
Lean4
theorem exists_pow_Uniformizer {r : K₀} (hr : r ≠ 0) (π : Uniformizer v) : ∃ n : ℕ, ∃ u : K₀ˣ, r = (π.1 ^ n).1 * u.1 :=
by
have hr₀ : v r ≠ 0 := by rw [ne_eq, zero_iff, Subring.coe_eq_zero_iff]; exact hr
set vr : Γˣ := Units.mk0 (v r) hr₀ with hvr_def
have hvr : vr ∈ (valueGroup v) := by
apply mem_valueGroup
rw [hvr_def, Units.val_mk0 hr₀]
exact mem_range_self _
rw [π.2.zpowers_eq_valueGroup, mem_zpowers_iff] at hvr
obtain ⟨m, hm⟩ := hvr
have hm' : v π.val ^ m = v r := by
rw [hvr_def] at hm
rw [← Units.val_mk0 hr₀, ← hm]
simp [Units.val_zpow_eq_zpow_val, Units.val_mk0]
have hm₀ : 0 ≤ m := by
rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']
exact r.2
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hm₀
use n
have hpow : v (π.1.1 ^ (-m) * r) = 1 := by rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
set a : K₀ := ⟨π.1.1 ^ (-m) * r, by apply le_of_eq hpow⟩ with ha
have ha₀ : (↑a : K) ≠ 0 :=
by
simp only [zpow_neg, ne_eq, mul_eq_zero, inv_eq_zero, ZeroMemClass.coe_eq_zero, not_or, ha]
refine ⟨?_, hr⟩
rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]
exact Or.inl π.ne_zero
have h_unit_a : IsUnit a := Integers.isUnit_of_one (integer.integers v) (isUnit_iff_ne_zero.mpr ha₀) hpow
use h_unit_a.unit
rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]
