f(tx,ty)=t^nf(x,y) then f(x,y) is homogeneous

Stream: new members

[Zhang Qinchuan]

Is there any theorem in Mathlib can prove that if f(tx,ty)=t^nf(x,y) then f(x,y) is homogeneous.

Homogeneous polynomial is defined in Mathlib4 such that If every monomial in p has the same degree then p is homogeneous. ( docs#MvPolynomial.IsHomogeneous )

I searched on LeanSearch but failed to find such theorem.

import Mathlib

open MvPolynomial

example {n : ℕ} {f : MvPolynomial (Fin 2) ℝ}
    (hf : ∀ x : Fin 2 → ℝ, ∀ t : ℝ, eval (t • x) f = t ^ n * eval x f) :
    f.IsHomogeneous n := by
  sorry

[Ruben Van de Velde]

https://loogle.lean-lang.org/?q=MvPolynomial.IsHomogeneous finds 44 declarations that mention IsHomogeneous and none seem relevant

[Kevin Buzzard]

It's not true over a finite field, so one would need an infinite assumption (and there are infinite base rings for which it's false too, for example infinite products of Z/pZ have x^p=x for all p)

[Michael Stoll]

One could take t to be a (new) indeterminate, so that the title equation is an equality of polynomials in three variables. Then this holds quite generally. (And probably one can deduce the desired result from that under the infiniteness assumption.)

[Scott Carnahan]

This may be in some sense the same as the indeterminate method, but you can let t run over all elements of all commutative R-algebras.

[Zhang Qinchuan]

Michael Stoll said:

One could take t to be a (new) indeterminate, so that the title equation is an equality of polynomials in three variables. Then this holds quite generally. (And probably one can deduce the desired result from that under the infiniteness assumption.)

That sounds good. But I failed to finish the proof:

import Mathlib

open MvPolynomial

variable {σ R : Type*} [DecidableEq σ] [Field R] [CharZero R]

def EvalHomo (f : MvPolynomial σ R) (n : ℕ) : Prop :=
  ∀ x : σ → R, ∀ t : R, eval (t • x) f = t ^ n * eval x f

noncomputable def Xnew_mul (f : MvPolynomial σ R) : MvPolynomial (σ ⊕ Unit) R :=
  ∑ d ∈ f.support, C (f.coeff d) * ∏ i ∈ d.support, (X (.inr .unit) * X (.inl i)) ^ d i

noncomputable def Xnew_pow_mul (f : MvPolynomial σ R) (n : ℕ) : MvPolynomial (σ ⊕ Unit) R :=
  X (.inr .unit) ^ n * ∑ d ∈ f.support, C (f.coeff d) * ∏ i ∈ d.support, X (.inl i) ^ d i

omit [DecidableEq σ] in
lemma EvalHomo.Xnew_mul_eq_Xnew_pow_mul {n : ℕ} {f : MvPolynomial σ R} (hf : EvalHomo f n) :
    Xnew_mul f = Xnew_pow_mul f n := by
  apply MvPolynomial.funext
  intro x
  convert hf (fun i => x (.inl i)) (x (.inr .unit))
  all_goals
    nth_rw 2 [eval_eq]
    simp [Xnew_mul, Xnew_pow_mul]

lemma EvalHomo.degree_Xnew_pow_mul {n : ℕ} {f : MvPolynomial σ R} (hf : EvalHomo f n) :
    ∀ d ∈ (Xnew_pow_mul f n).support, d (.inr .unit) = n := by
  sorry

lemma EvalHomo.degree_Xnew_mul {n : ℕ} {f : MvPolynomial σ R} :
    ∀ d ∈ (Xnew_mul f).support, d (.inr .unit) = ∑ i ∈ d.support \ {.inr .unit}, d i := by
  sorry

theorem EvalHomo.isHomogeneous {n : ℕ} {f : MvPolynomial σ R} (hf : EvalHomo f n) :
    IsHomogeneous f n := by
  intro d hcoeff
  rw [← mem_support_iff] at hcoeff
  rw [Finsupp.weight_apply, Finsupp.sum]
  conv_lhs => rhs; intro i; rw [Pi.one_apply, smul_eq_mul, mul_one]
  show ∑ i ∈ d.support, d i = n
  sorry