feat(MvPolynomial/Expand): more lemmas (#28833)

Author: yury-harmonic

Mathlib/Algebra/MvPolynomial/Eval.lean

@@ -558,11 +558,15 @@ theorem aeval_eq_eval₂Hom (p : MvPolynomial σ R) : aeval f p = eval₂Hom (al
   rfl
 
 @[simp]
-lemma coe_aeval_eq_eval : RingHomClass.toRingHom (MvPolynomial.aeval f) = MvPolynomial.eval f :=
+lemma coe_aeval_eq_eval :
+    RingHomClass.toRingHom (aeval f : MvPolynomial σ S₁ →ₐ[S₁] S₁) = eval f :=
   rfl
 
 @[simp]
-theorem aeval_X (s : σ) : aeval f (X s : MvPolynomial _ R) = f s :=
+lemma aeval_eq_eval : (aeval f : MvPolynomial σ S₁ → S₁) = eval f := rfl
+
+@[simp]
+theorem aeval_X (s : σ) : aeval f (X s : MvPolynomial σ R) = f s :=
   eval₂_X _ _ _
 
 theorem aeval_C (r : R) : aeval f (C r) = algebraMap R S₁ r :=

Mathlib/Algebra/MvPolynomial/Expand.lean

@@ -26,8 +26,7 @@ variable {σ τ R S : Type*} [CommSemiring R] [CommSemiring S]
 
 See also `Polynomial.expand`. -/
 noncomputable def expand (p : ℕ) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R :=
-  { (eval₂Hom C fun i ↦ X i ^ p : MvPolynomial σ R →+* MvPolynomial σ R) with
-    commutes' := fun _ ↦ eval₂Hom_C _ _ _ }
+  bind₁ fun i ↦ X i ^ p
 
 theorem expand_C (p : ℕ) (r : R) : expand p (C r : MvPolynomial σ R) = C r :=
   eval₂Hom_C _ _ _
@@ -38,22 +37,31 @@ theorem expand_X (p : ℕ) (i : σ) : expand p (X i : MvPolynomial σ R) = X i ^
 
 @[simp]
 theorem expand_monomial (p : ℕ) (d : σ →₀ ℕ) (r : R) :
-    expand p (monomial d r) = C r * ∏ i ∈ d.support, (X i ^ p) ^ d i :=
-  bind₁_monomial _ _ _
+    expand p (monomial d r) = monomial (p • d) r := by
+  rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]
+  · simp [pow_mul]
+  · simp
 
-theorem expand_one_apply (f : MvPolynomial σ R) : expand 1 f = f := by
-  simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, AlgHom.coe_mk, RingHom.id_apply]
+@[simp]
+lemma expand_zero :
+    expand 0 (σ := σ) (R := R) = .comp (Algebra.ofId R _) (MvPolynomial.aeval (1 : σ → R)) := by
+  ext1 i
+  simp
+
+lemma expand_zero_apply (p : MvPolynomial σ R) : expand 0 p = .C (MvPolynomial.eval 1 p) := by
+  simp
 
 @[simp]
 theorem expand_one : expand 1 = AlgHom.id R (MvPolynomial σ R) := by
-  ext1 f
-  rw [expand_one_apply, AlgHom.id_apply]
+  ext1 i
+  simp
+
+theorem expand_one_apply (f : MvPolynomial σ R) : expand 1 f = f := by simp
 
 theorem expand_comp_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) :
     (expand p).comp (bind₁ f) = bind₁ fun i ↦ expand p (f i) := by
-  apply algHom_ext
-  intro i
-  simp only [AlgHom.comp_apply, bind₁_X_right]
+  ext1 i
+  simp
 
 theorem expand_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
     expand p (bind₁ f φ) = bind₁ (fun i ↦ expand p (f i)) φ := by
@@ -63,16 +71,76 @@ theorem expand_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomi
 theorem map_expand (f : R →+* S) (p : ℕ) (φ : MvPolynomial σ R) :
     map f (expand p φ) = expand p (map f φ) := by simp [expand, map_bind₁]
 
-@[simp]
-theorem rename_expand (f : σ → τ) (p : ℕ) (φ : MvPolynomial σ R) :
-    rename f (expand p φ) = expand p (rename f φ) := by
-  simp [expand, bind₁_rename, rename_bind₁, Function.comp_def]
-
 @[simp]
 theorem rename_comp_expand (f : σ → τ) (p : ℕ) :
     (rename f).comp (expand p) =
       (expand p).comp (rename f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) := by
-  ext1 φ
-  simp only [rename_expand, AlgHom.comp_apply]
+  ext1 i
+  simp
+
+@[simp]
+theorem rename_expand (f : σ → τ) (p : ℕ) (φ : MvPolynomial σ R) :
+    rename f (expand p φ) = expand p (rename f φ) :=
+  DFunLike.congr_fun (rename_comp_expand f p) φ
+
+lemma eval₂Hom_comp_expand (f : R →+* S) (g : σ → S) (p : ℕ) :
+    (eval₂Hom f g).comp (expand p (σ := σ) (R := R) : MvPolynomial σ R →+* MvPolynomial σ R) =
+      eval₂Hom f (g ^ p) := by
+  ext <;> simp
+
+@[simp]
+lemma eval₂_expand (f : R →+* S) (g : σ → S) (φ : MvPolynomial σ R) (p : ℕ) :
+    eval₂ f g (expand p φ) = eval₂ f (g ^ p) φ :=
+  DFunLike.congr_fun (eval₂Hom_comp_expand f g p) φ
+
+@[simp]
+lemma aeval_comp_expand {A : Type*} [CommSemiring A] [Algebra R A] (f : σ → A) (p : ℕ) :
+    (aeval f).comp (expand p) = aeval (R := R) (f ^ p) := by
+  ext; simp
+
+@[simp]
+lemma aeval_expand {A : Type*} [CommSemiring A] [Algebra R A]
+    (f : σ → A) (φ : MvPolynomial σ R) (p : ℕ) :
+    aeval f (expand p φ) = aeval (f ^ p) φ :=
+  eval₂_expand ..
+
+@[simp]
+lemma eval_expand (f : σ → R) (φ : MvPolynomial σ R) (p : ℕ) :
+    eval f (expand p φ) = eval (f ^ p) φ :=
+  eval₂_expand ..
+
+theorem expand_mul_eq_comp (p q : ℕ) :
+    expand (σ := σ) (R := R) (p * q) = (expand p).comp (expand q) := by
+  ext1 i
+  simp [pow_mul]
+
+theorem expand_mul (p q : ℕ) (φ : MvPolynomial σ R) : φ.expand (p * q) = (φ.expand q).expand p :=
+  DFunLike.congr_fun (expand_mul_eq_comp p q) φ
+
+@[simp]
+lemma coeff_expand_smul (φ : MvPolynomial σ R) {p : ℕ} (hp : p ≠ 0) (m : σ →₀ ℕ) :
+    (expand p φ).coeff (p • m) = φ.coeff m := by
+  classical
+  induction φ using induction_on' <;> simp [*, nsmul_right_inj hp]
+
+lemma support_expand_subset [DecidableEq σ] (φ : MvPolynomial σ R) (p : ℕ) :
+    (expand p φ).support ⊆ φ.support.image (p • ·) := by
+  conv_lhs => rw [φ.as_sum]
+  simp only [map_sum, expand_monomial]
+  refine MvPolynomial.support_sum.trans ?_
+  aesop (add simp Finset.subset_iff)
+
+lemma coeff_expand_of_not_dvd (φ : MvPolynomial σ R) {p : ℕ} {m : σ →₀ ℕ} {i : σ} (h : ¬(p ∣ m i)) :
+    (expand p φ).coeff m = 0 := by
+  classical
+  contrapose! h
+  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
+  rcases h with ⟨a, -, rfl⟩
+  exact ⟨a i, by simp⟩
+
+lemma support_expand [DecidableEq σ] (φ : MvPolynomial σ R) {p : ℕ} (hp : p ≠ 0) :
+    (expand p φ).support = φ.support.image (p • ·) := by
+  refine (support_expand_subset φ p).antisymm ?_
+  simp [Finset.image_subset_iff, hp]
 
 end MvPolynomial