feat(RingTheory/Polynomial/ContentIdeal): more theorems (#25960)

We prove more facts about `contentIdeal`.
For instance we prove that
`(p * q).contentIdeal $\le$ p.contentIdeal * q.contentIdeal $\le$ (p * q).contentIdeal.radical`
which implies the following result, often called Gauss' Lemma
```
Polynomial.contentIdeal_mul_eq_top_of_contentIdeal_eq_top {p q : R[X]} (hp : p.contentIdeal = ⊤) 
(hq : q.contentIdeal = ⊤) : (p * q).contentIdeal = ⊤
```

Zulip discussion [here](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/contentIdeal/with/522432790)



Co-authored-by: Johan Commelin <[email protected]>

Author: fbarroero

Mathlib/Algebra/Module/PID.lean

@@ -218,7 +218,8 @@ theorem torsion_by_prime_power_decomposition (hM : Module.IsTorsion' M (Submonoi
       rw [Submodule.map_span, Submodule.map_top, range_mkQ] at hs'; simp only [mkQ_apply] at hs'
       simp only [s']; rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove]
       rw [← Set.range_comp, ← Set.insert_image_compl_eq_range _ j, Function.comp_apply,
-        (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _), span_insert_zero] at hs'
+        (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _),
+        Submodule.span_insert_zero] at hs'
       exact hs'
 
 end PTorsion

Mathlib/RingTheory/Ideal/Span.lean

@@ -125,6 +125,10 @@ theorem span_singleton_ne_top {α : Type*} [CommSemiring α] {x : α} (hx : ¬Is
 @[simp]
 theorem span_zero : span (0 : Set α) = ⊥ := by rw [← Set.singleton_zero, span_singleton_eq_bot]
 
+@[simp]
+theorem span_insert_zero {s : Set α} : span (insert (0 : α) s) = span s :=
+  Submodule.span_insert_zero
+
 @[simp]
 theorem span_one : span (1 : Set α) = ⊤ := by rw [← Set.singleton_one, span_singleton_one]
 

Mathlib/RingTheory/Polynomial/ContentIdeal.lean

@@ -5,7 +5,7 @@ Authors: Fabrizio Barroero
 -/
 
 import Mathlib.Order.CompletePartialOrder
-import Mathlib.RingTheory.Ideal.BigOperators
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Polynomial.Content
 
 /-!
@@ -19,12 +19,19 @@ Let `p : R[X]`.
 - `p.contentIdeal` is the `Ideal R` generated by the coefficients of `p`.
 
 ## Main Results
+- `Polynomial.contentIdeal_mul_le_mul_contentIdeal`: the content ideal of the product of two
+  polynomials is contained in the product of their content ideals.
 - `Polynomial.isPrimitive_of_contentIdeal_eq_top`: if the content ideal of `p` is the whole ring,
   then `p` is primitive.
 - `Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top`: in case the content ideal of `p` is
   principal, `p` is primitive if and only if its content ideal is the whole ring.
+- `Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul`: the product of the content ideals of
+  two polynomials is contained in the radical of the content ideal of their product.
 - `Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal`: if the content ideal of `p`
   is principal, then it is equal to the ideal generated by the content of `p`.
+- `contentIdeal_mul_eq_top_of_contentIdeal_eq_top`: if the content ideals of two
+  polynomials are the whole ring, then the content ideal of their product is the whole ring. This
+  is also often called Gauss' Lemma.
 
 ## TODO
 
@@ -36,7 +43,7 @@ namespace Polynomial
 
 open Ideal
 
-variable {R : Type*} [Semiring R] (p : R[X])
+variable {R S : Type*} [Semiring R] [Semiring S] (p : R[X])
 
 /-- The content ideal of a polynomial `p` is the ideal generated by its coefficients. -/
 def contentIdeal := span p.coeffs.toSet
@@ -71,22 +78,36 @@ theorem contentIdeal_C (r : R) : (C r).contentIdeal = span {r} := by
   rw [← monomial_zero_left]
   exact contentIdeal_monomial 0 r
 
+@[simp]
+theorem contentIdeal_one : (1 : R[X]).contentIdeal = ⊤ := by
+  rw [← span_singleton_one, ← contentIdeal_C 1, C_1]
+
 theorem contentIdeal_FG : p.contentIdeal.FG := ⟨p.coeffs, rfl⟩
 
+theorem contentIdeal_map_eq_map_contentIdeal (f : R →+* S) :
+    (p.map f).contentIdeal = p.contentIdeal.map f := by
+  suffices span ((map f p).coeffs ∪ {0}) = span (f '' p.coeffs ∪ {0}) by
+    simpa [contentIdeal_def, map_span]
+  congr 1
+  ext s
+  by_cases hs : s = 0
+  · simp [hs]
+  · aesop (add simp mem_coeffs_iff)
+
+theorem contentIdeal_mul_le_mul_contentIdeal (q : R[X]) :
+    (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal := by
+  rw [contentIdeal_def, span_le]
+  simp only [Set.subset_def, Finset.mem_coe, mem_coeffs_iff]
+  rintro r ⟨n, _, rfl⟩
+  simp [coeff_mul, _root_.sum_mem, Submodule.mul_mem_mul, coeff_mem_contentIdeal]
+
 section CommSemiring
 
 variable {R : Type*} [CommSemiring R] {p q : R[X]}
 
-theorem contentIdeal_le_contentIdeal_of_dvd (hpq : p ∣ q) :
-    q.contentIdeal ≤ p.contentIdeal := by
-  rw [contentIdeal_def, span_le]
-  intro _ h1
-  rw [Finset.mem_coe, mem_coeffs_iff] at h1
-  obtain ⟨_, _, h2⟩ := h1
-  obtain ⟨_, h3⟩ := hpq
-  rw [h3, coeff_mul] at h2
-  rw [h2]
-  exact Ideal.sum_mem _ <| fun _ _ ↦ mul_mem_right _ _ <| coeff_mem_contentIdeal p _
+theorem contentIdeal_le_contentIdeal_of_dvd (hpq : p ∣ q) : q.contentIdeal ≤ p.contentIdeal := by
+  obtain ⟨p', rfl⟩ := hpq
+  exact le_trans (p.contentIdeal_mul_le_mul_contentIdeal p') mul_le_right
 
 theorem _root_.Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
     (h_prin : p.contentIdeal.IsPrincipal) (n : ℕ) : h_prin.generator ∣ p.coeff n := by
@@ -131,8 +152,38 @@ theorem _root_.Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top
   use h_prin.generator, h_prin.contentIdeal_generator_dvd
   simp_all [← Ideal.span_singleton_eq_top]
 
+theorem contentIdeal_eq_top_of_contentIdeal_mul_eq_top
+    (h : (p * q).contentIdeal = ⊤) : p.contentIdeal = ⊤ := by
+  apply le_antisymm le_top
+  calc
+  ⊤ = (p * q).contentIdeal := h.symm
+  _ ≤ p.contentIdeal * q.contentIdeal := contentIdeal_mul_le_mul_contentIdeal p q
+  _ ≤ p.contentIdeal := mul_le_right
+
 end CommSemiring
 
+section Ring
+
+variable {R : Type*} [CommRing R] {p q : R[X]}
+
+theorem mul_contentIdeal_le_radical_contentIdeal_mul :
+    p.contentIdeal * q.contentIdeal ≤ ((p * q).contentIdeal).radical := by
+  rw [radical_eq_sInf, le_sInf_iff]
+  intro P ⟨hpq, hPprime⟩
+  rw [hPprime.mul_le]
+  rw [← Ideal.mk_ker (I := P)] at hpq ⊢
+  simpa only [← map_eq_bot_iff_le_ker, ← contentIdeal_map_eq_map_contentIdeal, Polynomial.map_mul,
+    contentIdeal_eq_bot_iff, mul_eq_zero] using hpq
+
+theorem contentIdeal_mul_eq_top_of_contentIdeal_eq_top (hp : p.contentIdeal = ⊤)
+    (hq : q.contentIdeal = ⊤)  : (p * q).contentIdeal = ⊤ := by
+  rw [← Ideal.radical_eq_top]
+  apply le_antisymm le_top
+  calc
+    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
+    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul
+
+end Ring
 section NormalizedGCDMonoid
 
 variable {R : Type*} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : R[X]}