MvPolynomial_isHomogeneous_of_forall_eval_intCast_mul_eq_pow_mul.lean

theorem mvPolynomial_eq_of_forall_eval_intCast_eq [CommRing R] [IsDomain R] [CharZero R]
    {ι : Type*} {p q : MvPolynomial ι R}
    (h : ∀ c : ι → ℤ, eval (fun i => (c i : R)) p = eval (fun i => (c i : R)) q) : p = q := by
  refine MvPolynomial.funext_set (fun _ => Set.range (Int.cast : ℤ → R))
    (fun _ => Set.infinite_range_of_injective Int.cast_injective) ?_
  intro x hx
  choose c hc using fun i => hx i (Set.mem_univ i)
  have hx' : x = fun i => (c i : R) := funext fun i => (hc i).symm
  subst hx'
  exact h c

theorem eval_mul_of_isHomogeneous [CommRing R] {ι : Type*} {φ : MvPolynomial ι R} {n : ℕ}
    (hφ : φ.IsHomogeneous n) (t : R) (x : ι → R) :
    eval (fun i => t * x i) φ = t ^ n * eval x φ := by
  simp only [MvPolynomial.eval_eq, Finset.mul_sum]
  refine Finset.sum_congr rfl fun d hd => ?_
  have hdeg : ∑ i ∈ d.support, d i = n := by
    have h1 := hφ (mem_support_iff.mp hd)
    have h2 : (Finsupp.weight (1 : ι → ℕ)) d = Finsupp.degree d := by
      rw [Finsupp.degree_eq_weight_one]; rfl
    rw [h2, Finsupp.degree_apply] at h1
    exact h1
  have hprod : ∏ i ∈ d.support, (t * x i) ^ d i = t ^ n * ∏ i ∈ d.support, x i ^ d i := by
    rw [← hdeg, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_mul_distrib]
    exact Finset.prod_congr rfl fun i _ => mul_pow t (x i) (d i)
  rw [hprod]
  ring

theorem isHomogeneous_of_forall_eval_intCast_mul [CommRing R] [IsDomain R] [CharZero R]
    {ι : Type*} (P : MvPolynomial ι R) (d : ℕ)
    (h : ∀ (n : ℤ) (c : ι → ℤ), eval (fun i => ((n * c i : ℤ) : R)) P =
      (n : R) ^ d * eval (fun i => (c i : R)) P) :
    P.IsHomogeneous d := by
  classical
  set N := P.totalDegree with hN
  have hcomp : ∀ k, k ≠ d → homogeneousComponent k P = 0 := by
    intro k hkd
    by_cases hkN : N < k
    · exact homogeneousComponent_eq_zero k P hkN
    push Not at hkN
    apply mvPolynomial_eq_of_forall_eval_intCast_eq (R := R)
    intro c
    rw [map_zero]
    set q : Polynomial R :=
      ∑ j ∈ range (N + 1), Polynomial.C (eval (fun i => (c i : R)) (homogeneousComponent j P)) *
        Polynomial.X ^ j with hq
    set r : Polynomial R := Polynomial.C (eval (fun i => (c i : R)) P) * Polynomial.X ^ d with hr
    have hqr : q = r := by
      apply Polynomial.eq_of_infinite_eval_eq
      refine Set.Infinite.mono (s := Set.range (Int.cast : ℤ → R)) ?_
        (Set.infinite_range_of_injective Int.cast_injective)
      rintro _ ⟨n, rfl⟩
      change Polynomial.eval (n : R) q = Polynomial.eval (n : R) r
      have hqe : Polynomial.eval (n : R) q = eval (fun i => ((n * c i : ℤ) : R)) P := by
        rw [hq, Polynomial.eval_finsetSum]
        conv_rhs => rw [← sum_homogeneousComponent P, map_sum]
        refine Finset.sum_congr rfl fun j _ => ?_
        rw [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X,
          mul_comm]
        have e1 : (fun i => ((n * c i : ℤ) : R)) = fun i => (n : R) * (c i : R) := by
          funext i; push_cast; ring
        rw [e1, eval_mul_of_isHomogeneous (homogeneousComponent_isHomogeneous j P)]
      rw [hqe, h n c, hr, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow,
        Polynomial.eval_X, mul_comm]
    have hcq : q.coeff k = eval (fun i => (c i : R)) (homogeneousComponent k P) := by
      rw [hq, Polynomial.finsetSum_coeff]
      simp only [Polynomial.coeff_C_mul_X_pow]
      rw [Finset.sum_ite_eq, ite_eq_left (Finset.mem_range.mpr (Nat.lt_succ_of_le hkN))]
    have hcr : r.coeff k = 0 := by
      rw [hr, Polynomial.coeff_C_mul_X_pow, ite_eq_right hkd]
    rw [← hcq, hqr, hcr]
  have hP : P = homogeneousComponent d P := by
    conv_lhs => rw [← sum_homogeneousComponent P]
    rw [Finset.sum_eq_single d (fun k _ hk => hcomp k hk)]
    intro hd
    rw [Finset.mem_range, not_lt] at hd
    exact homogeneousComponent_eq_zero d P (Nat.lt_of_succ_le hd)
  rw [hP]
  exact homogeneousComponent_isHomogeneous d P

theorem _root_.MvPolynomial.isHomogeneous_of_forall_eval_intCast_mul_eq_pow_mul
    {R : Type*} [CommRing R] [IsDomain R] [CharZero R] {ι : Type*} (P : MvPolynomial ι R) (d : ℕ)
    (h : ∀ (n : ℤ) (c : ι → ℤ), MvPolynomial.eval (fun i => ((n * c i : ℤ) : R)) P =
      (n : R) ^ d * MvPolynomial.eval (fun i => (c i : R)) P) :
    P.IsHomogeneous d :=
  P2mPolyLines.isHomogeneous_of_forall_eval_intCast_mul P d h