English
A polynomial p lifts via f if and only if there exists q ∈ R[X] with map f q = p and deg(q) = deg(p).
Русский
Многочлен p поднимается через f тогда и только тогда, когда существует q ∈ R[X] с map f q = p и deg(q) = deg(p).
LaTeX
$$$ \exists q : R[X], map f q = p \land q.\deg = p.\deg $$$
Lean4
/-- A polynomial lifts if and only if it can be lifted to a polynomial of the same degree. -/
theorem mem_lifts_and_degree_eq {p : S[X]} (hlifts : p ∈ lifts f) : ∃ q : R[X], map f q = p ∧ q.degree = p.degree :=
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 := fun k ↦ (hlifts k).choose_spec
let q : R[X] := ∑ k ∈ p.support, monomial k (g k)
have hq : map f q = p := by simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
have hq' : q.support = p.support :=
by
simp_rw [Finset.ext_iff, mem_support_iff, q, finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', ite_ne_right_iff,
mem_support_iff, and_iff_left_iff_imp, not_imp_not]
exact fun k h ↦ by rw [← hg, h, map_zero]
exact ⟨q, hq, congrArg Finset.max hq'⟩
