feat(algebra/squarefree): x is squarefree iff (x) is radical in gcd_monoid (#17002)

Define the notions of radical ideals and radical elements. Show that (under minimal assumptions):

+ an element is radical iff the ideal it generates is radical;

+ an ideal is radical iff the quotient by the ideal is reduced;

+ a ring is reduced iff 0 is a radical element.

These are useful glues for #16998.

The main theorem is `is_radical_iff_squarefree_or_zero`. The "if" direction only requires `cancel_comm_monoid_with_zero` as noted by @erdOne, and the "only if" direction depends on Cauchy induction #15880 (used to prove `is_radical_iff_pow_one_lt`).

Since UFDs are GCDs, we use the main theorem to golf `unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree` whose conclusion essentially says that (x) is radical. Some unnecessary `normalization_monoid` and `nontrivial` assumptions are also removed from *squarefree.lean*.

An earlier version of the PR only proved the main theorem for UFDs, and `le_dedup_self` and `normalized_factors_prod_eq` are remnants from that previous attempt; they are not used to prove the main theorem but are definitely useful lemmas to have.

- [x] depends on: #15880



Co-authored-by: Shimon Schlessinger <shimonschlessinger@Eitans-MacBook-Air.local>
Co-authored-by: Shimonschlessinger <Shimonschlessinger@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author: 3 people

src/algebra/squarefree.lean

@@ -177,18 +177,53 @@ end
 
 end irreducible
 
+section is_radical
+
+variables [cancel_comm_monoid_with_zero R]
+
+theorem is_radical.squarefree {x : R} (h0 : x ≠ 0) (h : is_radical x) : squarefree x :=
+begin
+  rintro z ⟨w, rfl⟩,
+  specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩,
+  rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at h,
+  rw [mul_assoc, mul_ne_zero_iff] at h0, exact h0.2,
+end
+
+variable [gcd_monoid R]
+
+theorem squarefree.is_radical {x : R} (hx : squarefree x) : is_radical x :=
+(is_radical_iff_pow_one_lt 2 one_lt_two).2 $ λ y hy, and.right $ (dvd_gcd_iff x x y).1
+begin
+  by_cases gcd x y = 0, { rw h, apply dvd_zero },
+  replace hy := ((dvd_gcd_iff x x _).2 ⟨dvd_rfl, hy⟩).trans gcd_pow_right_dvd_pow_gcd,
+  obtain ⟨z, hz⟩ := gcd_dvd_left x y,
+  nth_rewrite 0 hz at hy ⊢,
+  rw [pow_two, mul_dvd_mul_iff_left h] at hy,
+  obtain ⟨w, hw⟩ := hy,
+  exact (hx z ⟨w, by rwa [mul_right_comm, ←hw]⟩).mul_right_dvd.2 dvd_rfl,
+end
+
+theorem is_radical_iff_squarefree_or_zero {x : R} : is_radical x ↔ squarefree x ∨ x = 0 :=
+⟨λ hx, (em $ x = 0).elim or.inr (λ h, or.inl $ hx.squarefree h),
+  or.rec squarefree.is_radical $ by { rintro rfl, rw zero_is_radical_iff, apply_instance }⟩
+
+theorem is_radical_iff_squarefree_of_ne_zero {x : R} (h : x ≠ 0) : is_radical x ↔ squarefree x :=
+⟨is_radical.squarefree h, squarefree.is_radical⟩
+
+end is_radical
+
 namespace unique_factorization_monoid
-variables [cancel_comm_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R]
-variables [normalization_monoid R]
+variables [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R]
 
-lemma squarefree_iff_nodup_normalized_factors [decidable_eq R] {x : R} (x0 : x ≠ 0) :
-  squarefree x ↔ multiset.nodup (normalized_factors x) :=
+lemma squarefree_iff_nodup_normalized_factors [normalization_monoid R] [decidable_eq R] {x : R}
+  (x0 : x ≠ 0) : squarefree x ↔ multiset.nodup (normalized_factors x) :=
 begin
   have drel : decidable_rel (has_dvd.dvd : R → R → Prop),
   { classical,
     apply_instance, },
   haveI := drel,
   rw [multiplicity.squarefree_iff_multiplicity_le_one, multiset.nodup_iff_count_le_one],
+  haveI := nontrivial_of_ne x 0 x0,
   split; intros h a,
   { by_cases hmem : a ∈ normalized_factors x,
     { have ha := irreducible_of_normalized_factor _ hmem,
@@ -212,15 +247,8 @@ lemma dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : squarefree x) (h0
   x ∣ y ^ n ↔ x ∣ y :=
 begin
   classical,
-  by_cases hx : x = 0,
-  { simp [hx, pow_eq_zero_iff (nat.pos_of_ne_zero h0)] },
-  by_cases hy : y = 0,
-  { simp [hy, zero_pow (nat.pos_of_ne_zero h0)] },
-  refine ⟨λ h, _, λ h, h.pow h0⟩,
-  rw [dvd_iff_normalized_factors_le_normalized_factors hx (pow_ne_zero n hy),
-    normalized_factors_pow,
-    ((squarefree_iff_nodup_normalized_factors hx).1 hsq).le_nsmul_iff_le h0] at h,
-  rwa dvd_iff_normalized_factors_le_normalized_factors hx hy,
+  haveI := unique_factorization_monoid.to_gcd_monoid R,
+  exact ⟨hsq.is_radical n y, λ h, h.pow h0⟩,
 end
 
 end unique_factorization_monoid

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -359,15 +359,14 @@ lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
 by rw [← is_open_compl_iff, is_open_iff, compl_compl]
 
 lemma is_closed_iff_zero_locus_ideal (Z : set (prime_spectrum R)) :
-  is_closed Z ↔ ∃ (s : ideal R), Z = zero_locus s :=
+  is_closed Z ↔ ∃ (I : ideal R), Z = zero_locus I :=
 (is_closed_iff_zero_locus _).trans
-  ⟨λ x, ⟨_, x.some_spec.trans (zero_locus_span _).symm⟩, λ x, ⟨_, x.some_spec⟩⟩
+  ⟨λ ⟨s, hs⟩, ⟨_, (zero_locus_span s).substr hs⟩, λ ⟨I, hI⟩, ⟨I, hI⟩⟩
 
 lemma is_closed_iff_zero_locus_radical_ideal (Z : set (prime_spectrum R)) :
-  is_closed Z ↔ ∃ (s : ideal R), s.radical = s ∧ Z = zero_locus s :=
+  is_closed Z ↔ ∃ (I : ideal R), I.is_radical ∧ Z = zero_locus I :=
 (is_closed_iff_zero_locus_ideal _).trans
-  ⟨λ x, ⟨_, ideal.radical_idem _, x.some_spec.trans (zero_locus_radical _).symm⟩,
-    λ x, ⟨_, x.some_spec.2⟩⟩
+  ⟨λ ⟨I, hI⟩, ⟨_, I.radical_is_radical, (zero_locus_radical I).substr hI⟩, λ ⟨I, _, hI⟩, ⟨I, hI⟩⟩
 
 lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=
@@ -442,7 +441,7 @@ end
 
 local notation `Z(` a `)` := zero_locus (a : set R)
 
-lemma is_irreducible_zero_locus_iff_of_radical (I : ideal R) (hI : I.radical = I) :
+lemma is_irreducible_zero_locus_iff_of_radical (I : ideal R) (hI : I.is_radical) :
   is_irreducible (zero_locus (I : set R)) ↔ I.is_prime :=
 begin
   rw [ideal.is_prime_iff, is_irreducible],
@@ -454,22 +453,21 @@ begin
       { rintros h x y, exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩ },
       { rintros h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩, exact h x y } },
     { simp_rw [← zero_locus_inf, subset_zero_locus_iff_le_vanishing_ideal,
-        vanishing_ideal_zero_locus_eq_radical, hI],
+        vanishing_ideal_zero_locus_eq_radical, hI.radical],
       split,
       { intros h x y h',
         simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← ideal.span_le],
         apply h,
-        rw [← hI, ← ideal.radical_le_radical_iff, ideal.radical_inf, ← ideal.radical_mul,
-          ideal.radical_le_radical_iff, hI, ideal.span_mul_span],
-        simpa [ideal.span_le] using h' },
+        simpa [← hI.radical_le_iff, ideal.radical_inf, ← ideal.radical_mul,
+          hI.radical_le_iff, ideal.span_mul_span, ideal.span_le] using h' },
       { simp_rw [or_iff_not_imp_left, set_like.not_le_iff_exists],
         rintros h s t h' ⟨x, hx, hx'⟩ y hy,
         exact h (h' ⟨ideal.mul_mem_right _ _ hx, ideal.mul_mem_left _ _ hy⟩) hx' } } }
 end
 
 lemma is_irreducible_zero_locus_iff (I : ideal R) :
   is_irreducible (zero_locus (I : set R)) ↔ I.radical.is_prime :=
-(zero_locus_radical I) ▸ is_irreducible_zero_locus_iff_of_radical _ I.radical_idem
+(zero_locus_radical I) ▸ is_irreducible_zero_locus_iff_of_radical _ I.radical_is_radical
 
 instance [is_domain R] : irreducible_space (prime_spectrum R) :=
 begin
@@ -484,12 +482,12 @@ begin
   rw [← h₂.closure_eq, ← zero_locus_vanishing_ideal_eq_closure,
     is_irreducible_zero_locus_iff] at h₁,
   use ⟨_, h₁⟩,
-  obtain ⟨s, hs, rfl⟩ := (is_closed_iff_zero_locus_radical_ideal _).mp h₂,
+  obtain ⟨I, hI, rfl⟩ := (is_closed_iff_zero_locus_radical_ideal _).mp h₂,
   rw is_generic_point_iff_forall_closed h₂,
   intros Z hZ hxZ,
   obtain ⟨t, rfl⟩ := (is_closed_iff_zero_locus_ideal _).mp hZ,
-  exact zero_locus_anti_mono (by simpa [hs] using hxZ),
-  simp [hs]
+  exact zero_locus_anti_mono (by simpa [hI.radical] using hxZ),
+  simp [hI.radical]
 end
 
 section comap

src/data/multiset/dedup.lean

@@ -71,6 +71,9 @@ theorem le_dedup {s t : multiset α} : s ≤ dedup t ↔ s ≤ t ∧ nodup s :=
 ⟨λ h, ⟨le_trans h (dedup_le _), nodup_of_le h (nodup_dedup _)⟩,
  λ ⟨l, d⟩, (le_iff_subset d).2 $ subset.trans (subset_of_le l) (subset_dedup _)⟩
 
+theorem le_dedup_self {s : multiset α} : s ≤ dedup s ↔ nodup s :=
+by rw [le_dedup, and_iff_right le_rfl]
+
 theorem dedup_ext {s t : multiset α} : dedup s = dedup t ↔ ∀ a, a ∈ s ↔ a ∈ t :=
 by simp [nodup.ext]
 

src/ring_theory/ideal/operations.lean

@@ -644,9 +644,18 @@ def radical (I : ideal R) : ideal R :=
         (pow_add x m (c-m)).symm ▸ I.mul_mem_right _ hxmi)⟩,
   smul_mem' := λ r s ⟨n, hsni⟩, ⟨n, (mul_pow r s n).symm ▸ I.mul_mem_left (r^n) hsni⟩ }
 
+/-- An ideal is radical if it contains its radical. -/
+def is_radical (I : ideal R) : Prop := I.radical ≤ I
+
 theorem le_radical : I ≤ radical I :=
 λ r hri, ⟨1, (pow_one r).symm ▸ hri⟩
 
+/-- An ideal is radical iff it is equal to its radical. -/
+theorem radical_eq_iff : I.radical = I ↔ I.is_radical :=
+by rw [le_antisymm_iff, and_iff_left le_radical, is_radical]
+
+alias radical_eq_iff ↔ _ is_radical.radical
+
 variables (R)
 theorem radical_top : (radical ⊤ : ideal R) = ⊤ :=
 (eq_top_iff_one _).2 ⟨0, submodule.mem_top⟩
@@ -656,26 +665,34 @@ theorem radical_mono (H : I ≤ J) : radical I ≤ radical J :=
 λ r ⟨n, hrni⟩, ⟨n, H hrni⟩
 
 variables (I)
+
+theorem radical_is_radical : (radical I).is_radical :=
+λ r ⟨n, k, hrnki⟩, ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩
+
 @[simp] theorem radical_idem : radical (radical I) = radical I :=
-le_antisymm (λ r ⟨n, k, hrnki⟩, ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩) le_radical
+(radical_is_radical I).radical
+
 variables {I}
 
+theorem is_radical.radical_le_iff (hJ : J.is_radical) : radical I ≤ J ↔ I ≤ J :=
+⟨le_trans le_radical, λ h, hJ.radical ▸ radical_mono h⟩
+
 theorem radical_le_radical_iff : radical I ≤ radical J ↔ I ≤ radical J :=
-⟨λ h, le_trans le_radical h, λ h, radical_idem J ▸ radical_mono h⟩
+(radical_is_radical J).radical_le_iff
 
 theorem radical_eq_top : radical I = ⊤ ↔ I = ⊤ :=
 ⟨λ h, (eq_top_iff_one _).2 $ let ⟨n, hn⟩ := (eq_top_iff_one _).1 h in
   @one_pow R _ n ▸ hn, λ h, h.symm ▸ radical_top R⟩
 
-theorem is_prime.radical (H : is_prime I) : radical I = I :=
-le_antisymm (λ r ⟨n, hrni⟩, H.mem_of_pow_mem n hrni) le_radical
+theorem is_prime.is_radical (H : is_prime I) : I.is_radical :=
+λ r ⟨n, hrni⟩, H.mem_of_pow_mem n hrni
+
+theorem is_prime.radical (H : is_prime I) : radical I = I := H.is_radical.radical
 
 variables (I J)
 theorem radical_sup : radical (I ⊔ J) = radical (radical I ⊔ radical J) :=
 le_antisymm (radical_mono $ sup_le_sup le_radical le_radical) $
-λ r ⟨n, hrnij⟩, let ⟨s, hs, t, ht, hst⟩ := submodule.mem_sup.1 hrnij in
-@radical_idem _ _ (I ⊔ J) ▸ ⟨n, hst ▸ ideal.add_mem _
-  (radical_mono le_sup_left hs) (radical_mono le_sup_right ht)⟩
+  radical_le_radical_iff.2 $ sup_le (radical_mono le_sup_left) (radical_mono le_sup_right)
 
 theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
 le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
@@ -685,11 +702,11 @@ le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
 theorem radical_mul : radical (I * J) = radical I ⊓ radical J :=
 le_antisymm (radical_inf I J ▸ radical_mono $ @mul_le_inf _ _ I J)
 (λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩)
+
 variables {I J}
 
-theorem is_prime.radical_le_iff (hj : is_prime J) :
-  radical I ≤ J ↔ I ≤ J :=
-⟨le_trans le_radical, λ hij r ⟨n, hrni⟩, hj.mem_of_pow_mem n $ hij hrni⟩
+theorem is_prime.radical_le_iff (hJ : is_prime J) :
+  radical I ≤ J ↔ I ≤ J := hJ.is_radical.radical_le_iff
 
 theorem radical_eq_Inf (I : ideal R) :
   radical I = Inf { J : ideal R | I ≤ J ∧ is_prime J } :=
@@ -717,9 +734,12 @@ have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial
       (m.mul_mem_left _ hxym))⟩⟩,
 hrm $ this.radical.symm ▸ (Inf_le ⟨him, this⟩ : Inf {J : ideal R | I ≤ J ∧ is_prime J} ≤ m) hr
 
-@[simp] lemma radical_bot_of_is_domain {R : Type u} [comm_semiring R] [no_zero_divisors R] :
+lemma is_radical_bot_of_no_zero_divisors {R} [comm_semiring R] [no_zero_divisors R] :
+  (⊥ : ideal R).is_radical := λ x hx, hx.rec_on (λ n hn, pow_eq_zero hn)
+
+@[simp] lemma radical_bot_of_no_zero_divisors {R : Type u} [comm_semiring R] [no_zero_divisors R] :
   radical (⊥ : ideal R) = ⊥ :=
-eq_bot_iff.2 (λ x hx, hx.rec_on (λ n hn, pow_eq_zero hn))
+eq_bot_iff.2 is_radical_bot_of_no_zero_divisors
 
 instance : comm_semiring (ideal R) := submodule.comm_semiring
 
@@ -1401,17 +1421,20 @@ protected theorem map_pow (n : ℕ) : map f (I^n) = (map f I)^n :=
 map_pow (map_hom f) I n
 
 theorem comap_radical : comap f (radical K) = radical (comap f K) :=
-le_antisymm (λ r ⟨n, hfrnk⟩, ⟨n, show f (r ^ n) ∈ K,
-  from (map_pow f r n).symm ▸ hfrnk⟩)
-(λ r ⟨n, hfrnk⟩, ⟨n, map_pow f r n ▸ hfrnk⟩)
+by { ext, simpa only [radical, mem_comap, map_pow] }
+
+variable {K}
+theorem is_radical.comap (hK : K.is_radical) : (comap f K).is_radical :=
+by { rw [←hK.radical, comap_radical], apply radical_is_radical }
+
 omit rc
 
 @[simp] lemma map_quotient_self :
   map (quotient.mk I) I = ⊥ :=
 eq_bot_iff.2 $ ideal.map_le_iff_le_comap.2 $ λ x hx,
 (submodule.mem_bot (R ⧸ I)).2 $ ideal.quotient.eq_zero_iff_mem.2 hx
 
-variables {I J K L}
+variables {I J L}
 
 include rc
 theorem map_radical_le : map f (radical I) ≤ radical (map f I) :=