English
For any Laurent series x there exists f : RatFunc such that f maps to the same valuation as x under RatFunc valuation.
Русский
Для любого x существует f : RatFunc, для которого валидация такая же, как у x.
LaTeX
$$$\exists f : RatFunc K, Valued.v f = Valued.v x$$$
Lean4
/-- For every Laurent series `f` and every `γ : ℤᵐ⁰` one can find a rational function `Q` such
that the `X`-adic valuation `v` satisfies `v (f - Q) < γ`. -/
theorem exists_ratFunc_val_lt (f : K⸨X⸩) (γ : ℤᵐ⁰ˣ) : ∃ Q : RatFunc K, Valued.v (f - Q) < γ :=
by
set F := f.powerSeriesPart with hF
by_cases ord_nonpos : f.order < 0
· set η : ℤᵐ⁰ˣ := Units.mk0 (exp f.order) coe_ne_zero with hη
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt F (η * γ)
use RatFunc.X ^ f.order * (P : RatFunc K)
have F_mul := f.ofPowerSeries_powerSeriesPart
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (le_of_lt ord_nonpos)
rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul
· have : (algebraMap (RatFunc K) K⸨X⸩) 1 = 1 := by exact algebraMap.coe_one
rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, map_mul, zpow_neg, zpow_natCast,
inv_eq_one_div (RatFunc.X ^ s), map_div₀, map_pow, RatFunc.coe_X]
simp only [map_one]
rw [← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀, ← PowerSeries.coe_X, valuation_X_pow, ← hs, ← RatFunc.coe_coe,
← PowerSeries.coe_sub, ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap, ←
Units.val_mk0 (a := exp f.order) exp_ne_zero, ← hη]
apply inv_mul_lt_of_lt_mul₀
rwa [← Units.val_mul]
·
simp only [PowerSeries.coe_pow, pow_ne_zero, PowerSeries.coe_X, ne_eq, single_eq_zero_iff, one_ne_zero,
not_false_iff]
· obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (not_lt.mp ord_nonpos))
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ
use P
rw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe, ← PowerSeries.coe_sub, ← coe_algebraMap,
adicValued_apply, valuation_of_algebraMap]
exact hP
