English
A monic polynomial lifts if and only if it can be lifted to a monic polynomial of the same degree.
Русский
Монический многочлен поднимается тогда и только тогда, когда его можно поднять до монического многочлена той же степени.
LaTeX
$$$ \exists q : R[X], map f q = p \land q.\deg = p.\deg \land q.Monic$$$
Lean4
/-- A monic polynomial lifts if and only if it can be lifted to a monic polynomial
of the same degree. -/
theorem lifts_and_degree_eq_and_monic [Nontrivial S] {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) :
∃ q : R[X], map f q = p ∧ q.degree = p.degree ∧ q.Monic :=
by
rw [lifts_iff_coeff_lifts] at hlifts
let g : ℕ → R := fun k ↦ (hlifts k).choose
have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec
let q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
have hq : map f q = p := by
simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow, map_X, map_C, hg, ←
hp.as_sum]
have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩
