English
If q is homogeneous of degree n and hpq: MvPolynomial.aeval ![X,1] q = p, then p.homogenize n = q.
Русский
Если q гомогенный степени n и hpq: aeval ![X,1] q = p, тогда p.homogenize n = q.
LaTeX
$$$\\text{If } q \\text{ is homogeneous of degree } n \\text{ and } aeval \\!([X,1])\\, q = p, \\text{ then } p.homogenize\\ n = q.$$$
Lean4
theorem homogenize_eq_of_isHomogeneous {p : R[X]} {n : ℕ} {q : MvPolynomial (Fin 2) R} (hq : q.IsHomogeneous n)
(hpq : MvPolynomial.aeval ![X, 1] q = p) : p.homogenize n = q :=
by
subst p
rw [q.as_sum]
simp only [MvPolynomial.aeval_sum, MvPolynomial.aeval_monomial, ← C_eq_algebraMap, homogenize_finsetSum,
homogenize_C_mul]
refine Finset.sum_congr rfl fun m hm ↦ ?_
rw [MvPolynomial.monomial_eq]
congr 1
obtain rfl : m.weight 1 = n := hq <| by simpa using hm
simp [Finsupp.prod_fintype, Finsupp.weight_apply, Finsupp.sum_fintype, Fin.prod_univ_two, Fin.sum_univ_two]
