English
If the leading coefficient of p lies in the image of R under the localization, then scaling roots by the common denominator yields a polynomial that lies in lifts along the algebra map.
Русский
Если ведущий коэффициент p лежит в образе R под локализацией, умножение корней на общий знаменатель даёт полином, лежащий в росте вдоль отображения алгебраMap.
LaTeX
$$$p.scaleRoots( commonDenom(M,p.support,p.coeff) ) \in \text{Polynomial.lifts}(algebraMap_R_Rm)$$$
Lean4
theorem scaleRoots_commonDenom_mem_lifts (p : Rₘ[X]) (hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range) :
p.scaleRoots (algebraMap R Rₘ <| IsLocalization.commonDenom M p.support p.coeff) ∈
Polynomial.lifts (algebraMap R Rₘ) :=
by
rw [Polynomial.lifts_iff_coeff_lifts]
intro n
rw [Polynomial.coeff_scaleRoots]
by_cases h₁ : n ∈ p.support
on_goal 1 => by_cases h₂ : n = p.natDegree
· rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
· have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
rw [← tsub_add_cancel_of_le (le_tsub_of_add_le_left this), pow_add, pow_one, mul_comm, _root_.mul_assoc, ← map_pow]
change _ ∈ (algebraMap R Rₘ).range
apply mul_mem
· exact RingHom.mem_range_self _ _
· rw [← Algebra.smul_def]
exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩
· rw [Polynomial.notMem_support_iff] at h₁
rw [h₁, zero_mul]
exact zero_mem (algebraMap R Rₘ).range
