chore(data/polynomial/induction): cleanup (#15918)

Even ignoring the confusion with `data/polynomial/inductions.lean` (out of scope for this PR), this file is a bit of a mess:

* The coeff and summation lemmas are out of place
* Some lemmas use a weird `inverse` naming to refer to `set.preimage`.
* Some lemmas use `submodule.span` instead of `ideal.span`.

This PR moves, renames, and restates the lemmas above as necessary.
Some proofs have been golfed to enable the shuffling, but all lemma statements are defeq to the originals.

src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean

@@ -37,11 +37,11 @@ end
 
 /-- If a point of `Spec R[x]` is not contained in the vanishing set of `f`, then its image in
 `Spec R` is contained in the open set where at least one of the coefficients of `f` is non-zero.
-This lemma is a reformulation of `exists_coeff_not_mem_C_inverse`. -/
+This lemma is a reformulation of `exists_C_coeff_not_mem`. -/
 lemma comap_C_mem_image_of_Df {I : prime_spectrum R[X]}
   (H : I ∈ (zero_locus {f} : set (prime_spectrum R[X]))ᶜ ) :
   prime_spectrum.comap (polynomial.C : R →+* R[X]) I ∈ image_of_Df f :=
-exists_coeff_not_mem_C_inverse (mem_compl_zero_locus_iff_not_mem.mp H)
+exists_C_coeff_not_mem (mem_compl_zero_locus_iff_not_mem.mp H)
 
 /-- The open set `image_of_Df f` coincides with the image of `basic_open f` under the
 morphism `C⁺ : Spec R[x] → Spec R`. -/

src/data/polynomial/basic.lean

@@ -666,6 +666,12 @@ begin
   simpa [sum, support, coeff] using finsupp.sum_smul_index hf,
 end
 
+lemma sum_monomial_eq : ∀ p : R[X], p.sum (λ n a, monomial n a) = p
+| ⟨p⟩ := (of_finsupp_sum _ _).symm.trans (congr_arg _ $ finsupp.sum_single _)
+
+lemma sum_C_mul_X_eq (p : R[X]) : p.sum (λn a, C a * X^n) = p :=
+by simp_rw [←monomial_eq_C_mul_X, sum_monomial_eq]
+
 /-- `erase p n` is the polynomial `p` in which the `X^n` term has been erased. -/
 @[irreducible] definition erase (n : ℕ) : R[X] → R[X]
 | ⟨p⟩ := ⟨p.erase n⟩

src/data/polynomial/coeff.lean

@@ -205,6 +205,24 @@ by simpa only [pow_one] using coeff_mul_X_pow p 1 n
 @[simp] theorem coeff_X_mul (p : R[X]) (n : ℕ) :
   coeff (X * p) (n + 1) = coeff p n := by rw [(commute_X p).eq, coeff_mul_X]
 
+theorem coeff_mul_monomial (p : R[X]) (n d : ℕ) (r : R) :
+  coeff (p * monomial n r) (d + n) = coeff p d * r :=
+by rw [monomial_eq_C_mul_X, ←X_pow_mul, ←mul_assoc, coeff_mul_C, coeff_mul_X_pow]
+
+theorem coeff_monomial_mul (p : R[X]) (n d : ℕ) (r : R) :
+  coeff (monomial n r * p) (d + n) = r * coeff p d :=
+by rw [monomial_eq_C_mul_X, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
+
+-- This can already be proved by `simp`.
+theorem coeff_mul_monomial_zero (p : R[X]) (d : ℕ) (r : R) :
+  coeff (p * monomial 0 r) d = coeff p d * r :=
+coeff_mul_monomial p 0 d r
+
+-- This can already be proved by `simp`.
+theorem coeff_monomial_zero_mul (p : R[X]) (d : ℕ) (r : R) :
+  coeff (monomial 0 r * p) d = r * coeff p d :=
+coeff_monomial_mul p 0 d r
+
 theorem mul_X_pow_eq_zero {p : R[X]} {n : ℕ}
   (H : p * X ^ n = 0) : p = 0 :=
 ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n)

src/data/polynomial/induction.lean

@@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.coeff
+import ring_theory.ideal.basic
 
 /-!
-# Theory of univariate polynomials
+# Induction on polynomials
 
-The main results are `induction_on` and `as_sum`.
+This file contains lemmas dealing with different flavours of induction on polynomials.
+See also `data/polynomial/inductions.lean` (with an `s`!).
+
+The main result is `polynomial.induction_on`.
 -/
 
 noncomputable theory
@@ -24,17 +28,6 @@ variables {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A :
 section semiring
 variables [semiring R] {p q r : R[X]}
 
-lemma sum_C_mul_X_eq (p : R[X]) : p.sum (λn a, C a * X^n) = p :=
-begin
-  ext n,
-  simp only [polynomial.sum, X_pow_eq_monomial, coeff_monomial, mul_one, finset_sum_coeff,
-    C_mul_monomial, not_not, mem_support_iff, finset.sum_ite_eq', ite_eq_left_iff],
-  exact λ h, h.symm
-end
-
-lemma sum_monomial_eq (p : R[X]) : p.sum (λn a, monomial n a) = p :=
-by simp only [monomial_eq_C_mul_X, sum_C_mul_X_eq]
-
 @[elab_as_eliminator] protected lemma induction_on {M : R[X] → Prop} (p : R[X])
   (h_C : ∀a, M (C a))
   (h_add : ∀p q, M p → M q → M (p + q))
@@ -66,45 +59,22 @@ and it holds for monomials.
 polynomial.induction_on p (h_monomial 0) h_add
 (λ n a h, by { rw ← monomial_eq_C_mul_X at ⊢, exact h_monomial _ _ })
 
-section coeff
-
-theorem coeff_mul_monomial (p : R[X]) (n d : ℕ) (r : R) :
-  coeff (p * monomial n r) (d + n) = coeff p d * r :=
-by rw [monomial_eq_C_mul_X, ←X_pow_mul, ←mul_assoc, coeff_mul_C, coeff_mul_X_pow]
-
-theorem coeff_monomial_mul (p : R[X]) (n d : ℕ) (r : R) :
-  coeff (monomial n r * p) (d + n) = r * coeff p d :=
-by rw [monomial_eq_C_mul_X, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
-
--- This can already be proved by `simp`.
-theorem coeff_mul_monomial_zero (p : R[X]) (d : ℕ) (r : R) :
-  coeff (p * monomial 0 r) d = coeff p d * r :=
-coeff_mul_monomial p 0 d r
-
--- This can already be proved by `simp`.
-theorem coeff_monomial_zero_mul (p : R[X]) (d : ℕ) (r : R) :
-  coeff (monomial 0 r * p) d = r * coeff p d :=
-coeff_monomial_mul p 0 d r
-
-end coeff
 
 open submodule polynomial set
-variables {f : R[X]} {I : submodule R[X] R[X]}
+variables {f : R[X]} {I : ideal R[X]}
 
-/--  If the coefficients of a polynomial belong to n ideal contains the submodule span of the
-coefficients of a polynomial. -/
-lemma span_le_of_coeff_mem_C_inverse (cf : ∀ (i : ℕ), f.coeff i ∈ (C ⁻¹' I.carrier)) :
-  (span R[X] {g | ∃ i, g = C (f.coeff i)}) ≤ I :=
+/--  If the coefficients of a polynomial belong to an ideal, then that ideal contains
+the ideal spanned by the coefficients of the polynomial. -/
+lemma span_le_of_C_coeff_mem (cf : ∀ (i : ℕ), C (f.coeff i) ∈ I) :
+  ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I :=
 begin
-  refine bInter_subset_of_mem _,
-  rintros _ ⟨i, rfl⟩,
-  exact set_like.mem_coe.mpr (cf i),
+  simp only [@eq_comm _ _ (C _)] {single_pass := tt},
+  exact (ideal.span_le.trans range_subset_iff).mpr cf,
 end
 
-lemma mem_span_C_coeff :
-  f ∈ span R[X] {g : R[X] | ∃ i : ℕ, g = (C (coeff f i))} :=
+lemma mem_span_C_coeff : f ∈ ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)} :=
 begin
-  let p := span R[X] {g : R[X] | ∃ i : ℕ, g = (C (coeff f i))},
+  let p := ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)},
   nth_rewrite 0 (sum_C_mul_X_eq f).symm,
   refine submodule.sum_mem _ (λ n hn, _),
   dsimp,
@@ -115,10 +85,8 @@ begin
   rw monomial_eq_C_mul_X,
 end
 
-lemma exists_coeff_not_mem_C_inverse :
-  f ∉ I → ∃ i : ℕ , coeff f i ∉ (C ⁻¹'  I.carrier) :=
-imp_of_not_imp_not _ _
-  (λ cf, not_not.mpr ((span_le_of_coeff_mem_C_inverse (not_exists_not.mp cf)) mem_span_C_coeff))
+lemma exists_C_coeff_not_mem : f ∉ I → ∃ i : ℕ, C (coeff f i) ∉ I :=
+not.imp_symm $ λ cf, span_le_of_C_coeff_mem (not_exists_not.mp cf) mem_span_C_coeff
 
 end semiring