refactor(RingTheory.MvPolynomial.Homogeneous): refactor in terms of weightedHomogeneous (#7609)

We rewrite the definition of homogeneous polynomial as a special case of weighted homogeneous polynomial.

Question: should all uses of `∑ i in d.support, d i` be replaced by `degree d`?

Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>



Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Author: mariainesdff

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.Algebra.MvPolynomial.Equiv
 import Mathlib.Algebra.MvPolynomial.Variables
+import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 import Mathlib.Algebra.Polynomial.RingDivision
 
 #align_import ring_theory.mv_polynomial.homogeneous from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
@@ -37,19 +38,34 @@ variable {σ : Type*} {τ : Type*} {R : Type*} {S : Type*}
 
 /-
 TODO
-* create definition for `∑ i in d.support, d i`
 * show that `MvPolynomial σ R ≃ₐ[R] ⨁ i, homogeneousSubmodule σ R i`
 -/
+
+/-- The degree of a monomial. -/
+def degree (d : σ →₀ ℕ) := ∑ i in d.support, d i
+
+theorem weightedDegree_one (d : σ →₀ ℕ) :
+    weightedDegree 1 d = degree d := by
+  simp [weightedDegree, degree, Finsupp.total, Finsupp.sum]
+
 /-- A multivariate polynomial `φ` is homogeneous of degree `n`
 if all monomials occurring in `φ` have degree `n`. -/
 def IsHomogeneous [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) :=
-  ∀ ⦃d⦄, coeff d φ ≠ 0 → ∑ i in d.support, d i = n
+  IsWeightedHomogeneous 1 φ n
 #align mv_polynomial.is_homogeneous MvPolynomial.IsHomogeneous
 
+variable [CommSemiring R]
+
+theorem weightedTotalDegree_one (φ : MvPolynomial σ R) :
+    weightedTotalDegree (1 : σ → ℕ) φ = φ.totalDegree := by
+  simp only [totalDegree, weightedTotalDegree, weightedDegree, LinearMap.toAddMonoidHom_coe,
+    Finsupp.total, Pi.one_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
+    id.def, Algebra.id.smul_eq_mul, mul_one]
+
 variable (σ R)
 
 /-- The submodule of homogeneous `MvPolynomial`s of degree `n`. -/
-def homogeneousSubmodule [CommSemiring R] (n : ℕ) : Submodule R (MvPolynomial σ R) where
+def homogeneousSubmodule (n : ℕ) : Submodule R (MvPolynomial σ R) where
   carrier := { x | x.IsHomogeneous n }
   smul_mem' r a ha c hc := by
     rw [coeff_smul] at hc
@@ -68,6 +84,10 @@ def homogeneousSubmodule [CommSemiring R] (n : ℕ) : Submodule R (MvPolynomial
     · exact hb h
 #align mv_polynomial.homogeneous_submodule MvPolynomial.homogeneousSubmodule
 
+@[simp]
+lemma weightedHomogeneousSubmodule_one (n : ℕ) :
+    weightedHomogeneousSubmodule R 1 n = homogeneousSubmodule σ R n := rfl
+
 variable {σ R}
 
 @[simp]
@@ -79,66 +99,41 @@ variable (σ R)
 
 /-- While equal, the former has a convenient definitional reduction. -/
 theorem homogeneousSubmodule_eq_finsupp_supported [CommSemiring R] (n : ℕ) :
-    homogeneousSubmodule σ R n = Finsupp.supported _ R { d | ∑ i in d.support, d i = n } := by
-  ext
-  rw [Finsupp.mem_supported, Set.subset_def]
-  simp only [Finsupp.mem_support_iff, Finset.mem_coe]
-  rfl
+    homogeneousSubmodule σ R n = Finsupp.supported _ R { d | degree d = n } := by
+  simp_rw [← weightedDegree_one]
+  exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n
 #align mv_polynomial.homogeneous_submodule_eq_finsupp_supported MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
 
 variable {σ R}
 
 theorem homogeneousSubmodule_mul [CommSemiring R] (m n : ℕ) :
-    homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n) := by
-  rw [Submodule.mul_le]
-  intro φ hφ ψ hψ c hc
-  classical
-  rw [coeff_mul] at hc
-  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
-  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
-    contrapose! H
-    by_cases h : coeff d φ = 0 <;>
-      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
-  specialize hφ aux.1
-  specialize hψ aux.2
-  rw [Finset.mem_antidiagonal] at hde
-  classical
-  have hd' : d.support ⊆ d.support ∪ e.support := Finset.subset_union_left _ _
-  have he' : e.support ⊆ d.support ∪ e.support := Finset.subset_union_right _ _
-  rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd',
-    Finset.sum_subset he', ← Finset.sum_add_distrib]
-  · congr
-  all_goals intro _ _; apply Finsupp.not_mem_support_iff.mp
+    homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n) :=
+  weightedHomogeneousSubmodule_mul 1 m n
 #align mv_polynomial.homogeneous_submodule_mul MvPolynomial.homogeneousSubmodule_mul
 
 section
 
 variable [CommSemiring R]
 
-theorem isHomogeneous_monomial (d : σ →₀ ℕ) (r : R) (n : ℕ) (hn : ∑ i in d.support, d i = n) :
+theorem isHomogeneous_monomial {d : σ →₀ ℕ} (r : R) {n : ℕ} (hn : degree d = n) :
     IsHomogeneous (monomial d r) n := by
-  intro c hc
-  classical
-  rw [coeff_monomial] at hc
-  split_ifs at hc with h
-  · subst c
-    exact hn
-  · contradiction
+  simp_rw [← weightedDegree_one] at hn
+  exact isWeightedHomogeneous_monomial 1 d r hn
 #align mv_polynomial.is_homogeneous_monomial MvPolynomial.isHomogeneous_monomial
 
 variable (σ)
 
-theorem isHomogeneous_of_totalDegree_zero {p : MvPolynomial σ R} (hp : p.totalDegree = 0) :
-    IsHomogeneous p 0 := by
-  erw [totalDegree, Finset.sup_eq_bot_iff] at hp
-  -- we have to do this in two steps to stop simp changing bot to zero
-  simp_rw [mem_support_iff] at hp
-  exact hp
+theorem totalDegree_zero_iff_isHomogeneous {p : MvPolynomial σ R} :
+    p.totalDegree = 0 ↔ IsHomogeneous p 0 := by
+  rw [← weightedTotalDegree_one,
+    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
+
+alias ⟨isHomogeneous_of_totalDegree_zero, _⟩ := totalDegree_zero_iff_isHomogeneous
 #align mv_polynomial.is_homogeneous_of_total_degree_zero MvPolynomial.isHomogeneous_of_totalDegree_zero
 
 theorem isHomogeneous_C (r : R) : IsHomogeneous (C r : MvPolynomial σ R) 0 := by
   apply isHomogeneous_monomial
-  simp only [Finsupp.zero_apply, Finset.sum_const_zero]
+  simp only [degree, Finsupp.zero_apply, Finset.sum_const_zero]
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.is_homogeneous_C MvPolynomial.isHomogeneous_C
 
@@ -156,7 +151,7 @@ variable {σ}
 
 theorem isHomogeneous_X (i : σ) : IsHomogeneous (X i : MvPolynomial σ R) 1 := by
   apply isHomogeneous_monomial
-  rw [Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton]
+  rw [degree, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton]
   exact Finsupp.single_eq_same
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.is_homogeneous_X MvPolynomial.isHomogeneous_X
@@ -167,11 +162,10 @@ namespace IsHomogeneous
 
 variable [CommSemiring R] [CommSemiring S] {φ ψ : MvPolynomial σ R} {m n : ℕ}
 
-theorem coeff_eq_zero (hφ : IsHomogeneous φ n) (d : σ →₀ ℕ) (hd : ∑ i in d.support, d i ≠ n) :
+theorem coeff_eq_zero (hφ : IsHomogeneous φ n) {d : σ →₀ ℕ} (hd : degree d ≠ n) :
     coeff d φ = 0 := by
-  have aux := mt (@hφ d) hd
-  classical
-  rwa [Classical.not_not] at aux
+  simp_rw [← weightedDegree_one] at hd
+  exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd
 #align mv_polynomial.is_homogeneous.coeff_eq_zero MvPolynomial.IsHomogeneous.coeff_eq_zero
 
 theorem inj_right (hm : IsHomogeneous φ m) (hn : IsHomogeneous φ n) (hφ : φ ≠ 0) : m = n := by
@@ -239,7 +233,8 @@ lemma eval₂ (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ
   apply IsHomogeneous.mul (hf _) _
   convert IsHomogeneous.prod _ _ (fun k ↦ n * i k) _
   · rw [Finsupp.mem_support_iff] at hi
-    rw [← Finset.mul_sum, hφ hi]
+    rw [← Finset.mul_sum, ← hφ hi, weightedDegree_apply]
+    simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]
   · rintro k -
     apply (hg k).pow
 
@@ -271,38 +266,48 @@ lemma totalDegree_le (hφ : IsHomogeneous φ n) : φ.totalDegree ≤ n := by
   apply Finset.sup_le
   intro d hd
   rw [mem_support_iff] at hd
-  rw [Finsupp.sum, hφ hd]
+  rw [Finsupp.sum, ← hφ hd, weightedDegree_apply]
+  simp only [Pi.one_apply, smul_eq_mul, mul_one]
+  exact Nat.le.refl
 
 theorem totalDegree (hφ : IsHomogeneous φ n) (h : φ ≠ 0) : totalDegree φ = n := by
   apply le_antisymm hφ.totalDegree_le
   obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
   simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]
   replace hd := Finsupp.mem_support_iff.mpr hd
+  simp only [weightedDegree_apply,Pi.one_apply, smul_eq_mul, mul_one, ge_iff_le]
   -- Porting note: Original proof did not define `f`
   exact Finset.le_sup (f := fun s ↦ ∑ x in s.support, s x) hd
 #align mv_polynomial.is_homogeneous.total_degree MvPolynomial.IsHomogeneous.totalDegree
 
 theorem rename_isHomogeneous {f : σ → τ} (h : φ.IsHomogeneous n):
     (rename f φ).IsHomogeneous n := by
   rw [← φ.support_sum_monomial_coeff, map_sum]; simp_rw [rename_monomial]
-  exact IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _ _
-    ((Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans <| h <| mem_support_iff.mp hd)
+  apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _
+  intro d hd
+  apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans
+  convert h (mem_support_iff.mp hd)
+  simp only [weightedDegree_apply, AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one]
 
 theorem rename_isHomogeneous_iff {f : σ → τ} (hf : f.Injective) :
     (rename f φ).IsHomogeneous n ↔ φ.IsHomogeneous n := by
   refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
   convert ← @h (d.mapDomain f) _
-  · exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf
+  · simp only [weightedDegree_apply, Pi.one_apply, smul_eq_mul, mul_one]
+    exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf
   · rwa [coeff_rename_mapDomain f hf]
 
 lemma finSuccEquiv_coeff_isHomogeneous {N : ℕ} {φ : MvPolynomial (Fin (N+1)) R} {n : ℕ}
     (hφ : φ.IsHomogeneous n) (i j : ℕ) (h : i + j = n) :
     ((finSuccEquiv _ _ φ).coeff i).IsHomogeneous j := by
   intro d hd
   rw [finSuccEquiv_coeff_coeff] at hd
-  have aux : 0 ∉ Finset.map (Fin.succEmb N).toEmbedding d.support := by simp [Fin.succ_ne_zero]
-  simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
-    (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), Finset.sum_insert aux, ← h] using hφ hd
+  have h' : (weightedDegree 1) (Finsupp.cons i d) = i + j := by
+    simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
+     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd
+  simp only [weightedDegree_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum_cons,
+    add_right_inj] at h' ⊢
+  exact h'
 
 -- TODO: develop API for `optionEquivLeft` and get rid of the `[Fintype σ]` assumption
 lemma coeff_isHomogeneous_of_optionEquivLeft_symm
@@ -336,7 +341,7 @@ lemma exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux
     intro i hi
     rw [Finset.mem_range] at hi
     apply (hF.finSuccEquiv_coeff_isHomogeneous i (n-i) (by omega)).coeff_eq_zero
-    simp only [Finsupp.support_zero, Finsupp.coe_zero, Pi.zero_apply, Finset.sum_const_zero]
+    simp only [degree, Finsupp.support_zero, Finsupp.coe_zero, Pi.zero_apply, Finset.sum_const_zero]
     omega
   simp_rw [eval_eq_eval_mv_eval', eval_one_map, Polynomial.eval_eq_sum_range' hdeg,
     eval_zero, one_pow, mul_one, map_sum, Finset.sum_range_succ, Finset.sum_eq_zero aux, zero_add]
@@ -350,6 +355,7 @@ lemma exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux
     rw [Finsupp.coe_zero, Pi.zero_apply]
     by_cases hi : i ∈ d.support
     · have := hF.finSuccEquiv_coeff_isHomogeneous n 0 (add_zero _) hd
+      simp only [weightedDegree_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum] at this
       rw [Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ zero_le')] at this
       exact this i hi
     · simpa using hi
@@ -468,7 +474,7 @@ open Finset
 See `sum_homogeneousComponent` for the statement that `φ` is equal to the sum
 of all its homogeneous components. -/
 def homogeneousComponent [CommSemiring R] (n : ℕ) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R :=
-  (Submodule.subtype _).comp <| Finsupp.restrictDom _ _ { d | ∑ i in d.support, d i = n }
+  weightedHomogeneousComponent 1 n
 #align mv_polynomial.homogeneous_component MvPolynomial.homogeneousComponent
 
 section HomogeneousComponent
@@ -478,54 +484,45 @@ open Finset
 variable [CommSemiring R] (n : ℕ) (φ ψ : MvPolynomial σ R)
 
 theorem coeff_homogeneousComponent (d : σ →₀ ℕ) :
-    coeff d (homogeneousComponent n φ) = if (∑ i in d.support, d i) = n then coeff d φ else 0 :=
-  Finsupp.filter_apply (fun d : σ →₀ ℕ => ∑ i in d.support, d i = n) φ d
+    coeff d (homogeneousComponent n φ) = if (degree d) = n then coeff d φ else 0 := by
+  simp_rw [← weightedDegree_one]
+  convert coeff_weightedHomogeneousComponent n φ d
 #align mv_polynomial.coeff_homogeneous_component MvPolynomial.coeff_homogeneousComponent
 
 theorem homogeneousComponent_apply :
     homogeneousComponent n φ =
-      ∑ d in φ.support.filter fun d => ∑ i in d.support, d i = n, monomial d (coeff d φ) :=
-  Finsupp.filter_eq_sum (fun d : σ →₀ ℕ => ∑ i in d.support, d i = n) φ
+      ∑ d in φ.support.filter fun d => degree d = n, monomial d (coeff d φ) := by
+  simp_rw [← weightedDegree_one]
+  convert weightedHomogeneousComponent_apply n φ
 #align mv_polynomial.homogeneous_component_apply MvPolynomial.homogeneousComponent_apply
 
-theorem homogeneousComponent_isHomogeneous : (homogeneousComponent n φ).IsHomogeneous n := by
-  intro d hd
-  contrapose! hd
-  rw [coeff_homogeneousComponent, if_neg hd]
+theorem homogeneousComponent_isHomogeneous : (homogeneousComponent n φ).IsHomogeneous n :=
+  weightedHomogeneousComponent_isWeightedHomogeneous n φ
 #align mv_polynomial.homogeneous_component_is_homogeneous MvPolynomial.homogeneousComponent_isHomogeneous
 
 @[simp]
-theorem homogeneousComponent_zero : homogeneousComponent 0 φ = C (coeff 0 φ) := by
-  ext1 d
-  rcases em (d = 0) with (rfl | hd)
-  classical
-  · simp only [coeff_homogeneousComponent, sum_eq_zero_iff, Finsupp.zero_apply, if_true, coeff_C,
-      eq_self_iff_true, forall_true_iff]
-  · rw [coeff_homogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
-    simp only [DFunLike.ext_iff, Finsupp.zero_apply] at hd
-    simp [hd]
+theorem homogeneousComponent_zero : homogeneousComponent 0 φ = C (coeff 0 φ) :=
+  weightedHomogeneousComponent_zero φ (fun _ => Nat.succ_ne_zero Nat.zero)
 #align mv_polynomial.homogeneous_component_zero MvPolynomial.homogeneousComponent_zero
 
 @[simp]
 theorem homogeneousComponent_C_mul (n : ℕ) (r : R) :
-    homogeneousComponent n (C r * φ) = C r * homogeneousComponent n φ := by
-  simp only [C_mul', LinearMap.map_smul]
+    homogeneousComponent n (C r * φ) = C r * homogeneousComponent n φ :=
+  weightedHomogeneousComponent_C_mul φ n r
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.homogeneous_component_C_mul MvPolynomial.homogeneousComponent_C_mul
 
 theorem homogeneousComponent_eq_zero'
-    (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → ∑ i in d.support, d i ≠ n) :
+    (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → degree d ≠ n) :
     homogeneousComponent n φ = 0 := by
-  rw [homogeneousComponent_apply, sum_eq_zero]
-  intro d hd; rw [mem_filter] at hd
-  exfalso; exact h _ hd.1 hd.2
+  simp_rw [← weightedDegree_one] at h
+  exact weightedHomogeneousComponent_eq_zero' n φ h
 #align mv_polynomial.homogeneous_component_eq_zero' MvPolynomial.homogeneousComponent_eq_zero'
 
 theorem homogeneousComponent_eq_zero (h : φ.totalDegree < n) : homogeneousComponent n φ = 0 := by
   apply homogeneousComponent_eq_zero'
   rw [totalDegree, Finset.sup_lt_iff] at h
-  · intro d hd
-    exact ne_of_lt (h d hd)
+  · intro d hd; exact ne_of_lt (h d hd)
   · exact lt_of_le_of_lt (Nat.zero_le _) h
 #align mv_polynomial.homogeneous_component_eq_zero MvPolynomial.homogeneousComponent_eq_zero
 
@@ -539,17 +536,7 @@ theorem sum_homogeneousComponent :
 
 theorem homogeneousComponent_homogeneous_polynomial (m n : ℕ) (p : MvPolynomial σ R)
     (h : p ∈ homogeneousSubmodule σ R n) : homogeneousComponent m p = if m = n then p else 0 := by
-  simp only [mem_homogeneousSubmodule] at h
-  ext x
-  rw [coeff_homogeneousComponent]
-  by_cases zero_coeff : coeff x p = 0
-  · split_ifs
-    all_goals simp only [zero_coeff, coeff_zero]
-  · rw [h zero_coeff]
-    simp only [show n = m ↔ m = n from eq_comm]
-    split_ifs with h1
-    · rfl
-    · simp only [coeff_zero]
+  convert weightedHomogeneousComponent_weighted_homogeneous_polynomial m n p h
 #align mv_polynomial.homogeneous_component_homogeneous_polynomial MvPolynomial.homogeneousComponent_homogeneous_polynomial
 
 end HomogeneousComponent