From e72937a78c85e2f4335925d63482279f748edd35 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 16 Jan 2024 15:36:10 +0000 Subject: [PATCH] refactor(MonoidAlgebra/Support): reformulate `support_mul` (#8953) Use pointwise multiplication/addition of `Finset`s in `MonoidAlgebra.support_mul` and `AddMonoidAlgebra.support_mul`. --- Mathlib/Algebra/MonoidAlgebra/Degree.lean | 14 ++--- Mathlib/Algebra/MonoidAlgebra/Grading.lean | 15 ++---- Mathlib/Algebra/MonoidAlgebra/Support.lean | 63 ++++++++++------------ Mathlib/Data/MvPolynomial/Basic.lean | 28 +++------- Mathlib/Data/MvPolynomial/Variables.lean | 23 +++----- Mathlib/Data/Polynomial/Coeff.lean | 12 ++--- 6 files changed, 57 insertions(+), 98 deletions(-) diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean index 1503775afe947..3e5043ad13f6b 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Degree.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Degree.lean @@ -102,19 +102,15 @@ variable [Add A] [Add B] [Add T] [CovariantClass B B (· + ·) (· ≤ ·)] theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b) (f g : R[A]) : - (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by - refine' (Finset.sup_mono <| support_mul _ _).trans _ - simp_rw [Finset.sup_biUnion, Finset.sup_singleton] - refine' Finset.sup_le fun fd fds => Finset.sup_le fun gd gds => degbm.trans <| add_le_add _ _ <;> - exact Finset.le_sup ‹_› + (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := + (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦ + degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds) #align add_monoid_algebra.sup_support_mul_le AddMonoidAlgebra.sup_support_mul_le theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b)) (f g : R[A]) : - f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt := by - refine' OrderDual.ofDual_le_ofDual.mpr <| sup_support_mul_le _ f g - intros a b - exact OrderDual.ofDual_le_ofDual.mp degtm + f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt := + sup_support_mul_le (B := Tᵒᵈ) degtm f g #align add_monoid_algebra.le_inf_support_mul AddMonoidAlgebra.le_inf_support_mul end AddOnly diff --git a/Mathlib/Algebra/MonoidAlgebra/Grading.lean b/Mathlib/Algebra/MonoidAlgebra/Grading.lean index f5c16d37fc29e..2c27e0a171d4e 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Grading.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Grading.lean @@ -100,17 +100,12 @@ instance gradeBy.gradedMonoid [AddMonoid M] [AddMonoid ι] [CommSemiring R] (f : SetLike.GradedMonoid (gradeBy R f : ι → Submodule R R[M]) where one_mem m h := by rw [one_def] at h - by_cases H : (1 : R) = (0 : R) - · rw [H, single, Finsupp.single_zero] at h - cases h - · rw [Finsupp.support_single_ne_zero _ H, Finset.mem_singleton] at h - rw [h, AddMonoidHom.map_zero] + obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h + apply map_zero mul_mem i j a b ha hb c hc := by - set h := support_mul a b hc - simp only [Finset.mem_biUnion] at h - rcases h with ⟨ma, ⟨hma, ⟨mb, ⟨hmb, hmc⟩⟩⟩⟩ - rw [← ha ma hma, ← hb mb hmb, Finset.mem_singleton.mp hmc] - apply AddMonoidHom.map_add + obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c := + Finset.mem_add.1 <| support_mul a b hc + rw [map_add, ha ma hma, hb mb hmb] #align add_monoid_algebra.grade_by.graded_monoid AddMonoidAlgebra.gradeBy.gradedMonoid instance grade.gradedMonoid [AddMonoid M] [CommSemiring R] : diff --git a/Mathlib/Algebra/MonoidAlgebra/Support.lean b/Mathlib/Algebra/MonoidAlgebra/Support.lean index b56b9d6eda8ef..b4964b5c57347 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Support.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Support.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ import Mathlib.Algebra.MonoidAlgebra.Basic +import Mathlib.Data.Finset.Pointwise #align_import algebra.monoid_algebra.support from "leanprover-community/mathlib"@"16749fc4661828cba18cd0f4e3c5eb66a8e80598" @@ -11,6 +12,7 @@ import Mathlib.Algebra.MonoidAlgebra.Basic # Lemmas about the support of a finitely supported function -/ +open scoped Pointwise universe u₁ u₂ u₃ @@ -20,36 +22,23 @@ open Finset Finsupp variable {k : Type u₁} {G : Type u₂} [Semiring k] +theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) : + (a * b).support ⊆ a.support * b.support := + support_sum.trans <| biUnion_subset.2 fun _x hx ↦ + support_sum.trans <| biUnion_subset.2 fun _y hy ↦ + support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy +#align monoid_algebra.support_mul MonoidAlgebra.support_mul + theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) : - (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support := by - intro x hx - contrapose hx - have : ∀ y, a * y = x → f y = 0 := by - simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, - Classical.not_not] using hx - simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, - Classical.not_not] - exact - Finset.sum_eq_zero - (by - simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def, - ite_eq_right_iff, eq_self_iff_true, imp_true_iff]) + (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support := + (support_mul _ _).trans <| (Finset.image₂_subset_right support_single_subset).trans <| by + rw [Finset.image₂_singleton_left] #align monoid_algebra.support_single_mul_subset MonoidAlgebra.support_single_mul_subset theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) : - (f * single a r).support ⊆ Finset.image (· * a) f.support := by - intro x hx - contrapose hx - have : ∀ y, y * a = x → f y = 0 := by - simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, - Classical.not_not] using hx - simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, - Classical.not_not] - exact - Finset.sum_eq_zero - (by - simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff, - eq_self_iff_true, imp_true_iff, zero_mul]) + (f * single a r).support ⊆ Finset.image (· * a) f.support := + (support_mul _ _).trans <| (Finset.image₂_subset_left support_single_subset).trans <| by + rw [Finset.image₂_singleton_right] #align monoid_algebra.support_mul_single_subset MonoidAlgebra.support_mul_single_subset theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k} @@ -72,13 +61,6 @@ theorem support_mul_single_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k Finsupp.sum_ite_eq', Ne.def, not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff] #align monoid_algebra.support_mul_single_eq_image MonoidAlgebra.support_mul_single_eq_image -theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) : - (a * b).support ⊆ a.support.biUnion fun a₁ => b.support.biUnion fun a₂ => {a₁ * a₂} := - Subset.trans support_sum <| - biUnion_mono fun _ _ => - Subset.trans support_sum <| biUnion_mono fun _a₂ _ => support_single_subset -#align monoid_algebra.support_mul MonoidAlgebra.support_mul - theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) : (f * single x r).support = f.support.map (mulRightEmbedding x) := by @@ -97,6 +79,13 @@ theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) ( mem_map, mulLeftEmbedding_apply] #align monoid_algebra.support_single_mul MonoidAlgebra.support_single_mul +lemma support_one_subset [One G] : (1 : MonoidAlgebra k G).support ⊆ 1 := + Finsupp.support_single_subset + +@[simp] +lemma support_one [One G] [NeZero (1 : k)] : (1 : MonoidAlgebra k G).support = 1 := + Finsupp.support_single_ne_zero _ one_ne_zero + section Span variable [MulOneClass G] @@ -118,7 +107,7 @@ open Finset Finsupp MulOpposite variable {k : Type u₁} {G : Type u₂} [Semiring k] theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) : - (a * b).support ⊆ a.support.biUnion fun a₁ => b.support.biUnion fun a₂ => {a₁ + a₂} := + (a * b).support ⊆ a.support + b.support := @MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _ #align add_monoid_algebra.support_mul AddMonoidAlgebra.support_mul @@ -134,6 +123,12 @@ theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k) MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _ #align add_monoid_algebra.support_single_mul AddMonoidAlgebra.support_single_mul +lemma support_one_subset [Zero G] : (1 : k[G]).support ⊆ 0 := Finsupp.support_single_subset + +@[simp] +lemma support_one [Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0 := + Finsupp.support_single_ne_zero _ one_ne_zero + section Span /-- An element of `k[G]` is in the submodule generated by its support. -/ diff --git a/Mathlib/Data/MvPolynomial/Basic.lean b/Mathlib/Data/MvPolynomial/Basic.lean index 1082e4484dd74..3f20a5cc316ba 100644 --- a/Mathlib/Data/MvPolynomial/Basic.lean +++ b/Mathlib/Data/MvPolynomial/Basic.lean @@ -71,14 +71,10 @@ polynomial, multivariate polynomial, multivariable polynomial set_option autoImplicit true - noncomputable section -open BigOperators - open Set Function Finsupp AddMonoidAlgebra - -open BigOperators +open scoped BigOperators Pointwise universe u v w x @@ -597,8 +593,8 @@ theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ #align mv_polynomial.sum_def MvPolynomial.sum_def theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) : - (p * q).support ⊆ p.support.biUnion fun a => q.support.biUnion fun b => {a + b} := by - convert AddMonoidAlgebra.support_mul p q + (p * q).support ⊆ p.support + q.support := + AddMonoidAlgebra.support_mul p q #align mv_polynomial.support_mul MvPolynomial.support_mul @[ext] @@ -772,23 +768,15 @@ theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPo theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 := by classical - obtain rfl | hr := eq_or_ne r 0 - · simp only [monomial_zero, coeff_zero, mul_zero, ite_self] - haveI : Nontrivial R := nontrivial_of_ne _ _ hr split_ifs with h · conv_rhs => rw [← coeff_mul_monomial _ s] congr with t rw [tsub_add_cancel_of_le h] - · rw [← not_mem_support_iff] - intro hm - apply h - have H := support_mul _ _ hm - simp only [Finset.mem_biUnion] at H - rcases H with ⟨j, _hj, i', hi', H⟩ - rw [support_monomial, if_neg hr, Finset.mem_singleton] at hi' - subst i' - rw [Finset.mem_singleton] at H - subst m + · contrapose! h + rw [← mem_support_iff] at h + obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by + simpa [Finset.add_singleton] + using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h exact le_add_left le_rfl #align mv_polynomial.coeff_mul_monomial' MvPolynomial.coeff_mul_monomial' diff --git a/Mathlib/Data/MvPolynomial/Variables.lean b/Mathlib/Data/MvPolynomial/Variables.lean index 384db34fd52d0..e7cb03688a252 100644 --- a/Mathlib/Data/MvPolynomial/Variables.lean +++ b/Mathlib/Data/MvPolynomial/Variables.lean @@ -159,29 +159,18 @@ theorem degrees_sum {ι : Type*} [DecidableEq σ] (s : Finset ι) (f : ι → Mv theorem degrees_mul (p q : MvPolynomial σ R) : (p * q).degrees ≤ p.degrees + q.degrees := by classical - refine' Finset.sup_le fun b hb => _ - have := support_mul p q hb - simp only [Finset.mem_biUnion, Finset.mem_singleton] at this - rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩ + refine (Finset.sup_mono <| support_mul p q).trans <| Finset.sup_add_le.2 fun a ha b hb ↦ ?_ rw [Finsupp.toMultiset_add] - exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂) + exact add_le_add (Finset.le_sup ha) (Finset.le_sup hb) #align mv_polynomial.degrees_mul MvPolynomial.degrees_mul theorem degrees_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) : - (∏ i in s, f i).degrees ≤ ∑ i in s, (f i).degrees := by - classical - refine' s.induction _ _ - · simp only [Finset.prod_empty, Finset.sum_empty, degrees_one, le_refl] - · intro i s his ih - rw [Finset.prod_insert his, Finset.sum_insert his] - exact le_trans (degrees_mul _ _) (add_le_add_left ih _) + (∏ i in s, f i).degrees ≤ ∑ i in s, (f i).degrees := + Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ degrees) degrees_one degrees_mul _ _ #align mv_polynomial.degrees_prod MvPolynomial.degrees_prod -theorem degrees_pow (p : MvPolynomial σ R) : ∀ n : ℕ, (p ^ n).degrees ≤ n • p.degrees - | 0 => by rw [pow_zero, degrees_one]; exact Multiset.zero_le _ - | n + 1 => by - rw [pow_succ, add_smul, add_comm, one_smul] - exact le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow _ n) _) +theorem degrees_pow (p : MvPolynomial σ R) (n : ℕ) : (p ^ n).degrees ≤ n • p.degrees := by + simpa using degrees_prod (Finset.range n) fun _ ↦ p #align mv_polynomial.degrees_pow MvPolynomial.degrees_pow theorem mem_degrees {p : MvPolynomial σ R} {i : σ} : diff --git a/Mathlib/Data/Polynomial/Coeff.lean b/Mathlib/Data/Polynomial/Coeff.lean index 450ed1e3c4e83..f75c5db1b26f8 100644 --- a/Mathlib/Data/Polynomial/Coeff.lean +++ b/Mathlib/Data/Polynomial/Coeff.lean @@ -66,17 +66,13 @@ theorem support_smul [Monoid S] [DistribMulAction S R] (r : S) (p : R[X]) : simp [hi] #align polynomial.support_smul Polynomial.support_smul +open scoped Pointwise in theorem card_support_mul_le : (p * q).support.card ≤ p.support.card * q.support.card := by calc (p * q).support.card _ = (p.toFinsupp * q.toFinsupp).support.card := by rw [← support_toFinsupp, toFinsupp_mul] - _ ≤ _ := Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp) - _ ≤ _ := by - apply Finset.card_biUnion_le_card_mul - intro _ _ - rw [← mul_one q.support.card] - apply Finset.card_biUnion_le_card_mul - intro _ _ - exact (Finset.card_singleton _) ▸ le_rfl + _ ≤ (p.toFinsupp.support + q.toFinsupp.support).card := + Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp) + _ ≤ p.support.card * q.support.card := Finset.card_image₂_le .. /-- `Polynomial.sum` as a linear map. -/ @[simps]