English
If a polynomial f has distinguished factorization with h, then the degree of the map f is equal to the lift of the degree of the image under the quotient map.
Русский
Если существует представление f как произведение g*h с разделённой структурой, то deg f совпадает с подъёмом deg f в образ под факторной картой.
LaTeX
$$$\\text{degree}_{f} = \\mathrm{lift}(\\mathrm{order}(f.map(\\mathrm{Quotient.mk}\,I)))$ in appropriate setting$$
Lean4
theorem degree_eq_coe_lift_order_map (distinguish : g.IsDistinguishedAt I) (notMem : PowerSeries.constantCoeff h ∉ I)
(eq : f = g * h) :
g.degree =
(f.map (Ideal.Quotient.mk I)).order.lift
(order_finite_iff_ne_zero.2 (distinguish.map_ne_zero_of_eq_mul f h notMem eq)) :=
by
have : Nontrivial R :=
_root_.nontrivial_iff.mpr ⟨0, PowerSeries.constantCoeff h, ne_of_mem_of_not_mem I.zero_mem notMem⟩
rw [Polynomial.degree_eq_natDegree distinguish.monic.ne_zero, Nat.cast_inj, ← ENat.coe_inj, ENat.coe_lift, Eq.comm,
PowerSeries.order_eq_nat]
have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) * h.map (Ideal.Quotient.mk I) :=
by simp [← map_eq_X_pow distinguish, eq]
constructor
· simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem]
· intro i hi
simp [mapf, PowerSeries.coeff_X_pow_mul', hi]
