[Merged by Bors] - feat: add a version of Ideal.associatesEquivIsPrincipal for generators that are non-zero-divisors

Mathlib/RingTheory/Ideal/IsPrincipal.lean

@@ -16,24 +16,31 @@ This file deals with the set of principal ideals of a `CommRing R`.
 
 * `Ideal.isPrincipalSubmonoid`: the submonoid of `Ideal R` formed by the principal ideals of `R`.
 
+* `Ideal.isPrincipalNonZeroDivisorSubmonoid`: the submonoid of `(Ideal R)⁰` formed by the
+non-zero-divisors principal ideals of `R`.
+
 * `Ideal.associatesMulEquivIsPrincipal`: the `MulEquiv` between the monoid of `Associates R` and
 the submonoid of principal ideals of `R`.
 
+* `Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal`: the `MulEquiv` between the monoid of
+`Associates R⁰` and the submonoid of non-zero-divisors principal ideals of `R`.
 -/
 
 variable {R : Type*} [CommRing R]
 
 namespace Ideal
 
-open Submodule
+open Submodule Associates
+
+open scoped nonZeroDivisors
 
 variable (R) in
 /-- The principal ideals of `R` form a submonoid of `Ideal R`. -/
 def isPrincipalSubmonoid : Submonoid (Ideal R) where
   carrier := {I | IsPrincipal I}
   mul_mem' := by
     rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
-    exact ⟨x * y, Ideal.span_singleton_mul_span_singleton x y⟩
+    exact ⟨x * y, span_singleton_mul_span_singleton x y⟩
   one_mem' := ⟨1, one_eq_span⟩
 
 theorem mem_isPrincipalSubmonoid_iff {I : Ideal R} :
@@ -42,6 +49,16 @@ theorem mem_isPrincipalSubmonoid_iff {I : Ideal R} :
 theorem span_singleton_mem_isPrincipalSubmonoid (a : R) :
     span {a} ∈ isPrincipalSubmonoid R := mem_isPrincipalSubmonoid_iff.mpr ⟨a, rfl⟩
 
+variable (R) in
+/-- The non-zero-divisors principal ideals of `R` form a submonoid of `(Ideal R)⁰`. -/
+def isPrincipalNonZeroDivisorsSubmonoid : Submonoid (Ideal R)⁰ where
+  carrier := {I | IsPrincipal I.val}
+  mul_mem' := by
+    rintro ⟨_, _⟩ ⟨_, _⟩ ⟨x, rfl⟩ ⟨y, rfl⟩
+    exact ⟨x * y, by
+      simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]⟩
+  one_mem' := ⟨1, by simp⟩
+
 variable [IsDomain R]
 
 variable (R) in
@@ -51,45 +68,86 @@ noncomputable def associatesEquivIsPrincipal :
     Associates R ≃ {I : Ideal R // IsPrincipal I} where
   toFun := Quotient.lift (fun x ↦ ⟨span {x}, x, rfl⟩)
     (fun _ _ _ ↦ by simpa [span_singleton_eq_span_singleton])
-  invFun I := Associates.mk I.2.generator
+  invFun I := .mk I.2.generator
   left_inv := Quotient.ind fun _ ↦ by simpa using
     Ideal.span_singleton_eq_span_singleton.mp (@Ideal.span_singleton_generator _ _ _ ⟨_, rfl⟩)
   right_inv I := by simp only [Quotient.lift_mk, span_singleton_generator, Subtype.coe_eta]
 
 @[simp]
 theorem associatesEquivIsPrincipal_apply (x : R) :
-    associatesEquivIsPrincipal R (Associates.mk x) = span {x} := rfl
+    associatesEquivIsPrincipal R (.mk x) = span {x} := rfl
 
 @[simp]
 theorem associatesEquivIsPrincipal_symm_apply {I : Ideal R} (hI : IsPrincipal I) :
-    (associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = Associates.mk hI.generator := rfl
+    (associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = .mk hI.generator := rfl
 
 theorem associatesEquivIsPrincipal_mul (x y : Associates R) :
     (associatesEquivIsPrincipal R (x * y) : Ideal R) =
       (associatesEquivIsPrincipal R x) * (associatesEquivIsPrincipal R y) := by
-  rw [← Associates.quot_out x, ← Associates.quot_out y]
-  simp_rw [Associates.mk_mul_mk, ← Associates.quotient_mk_eq_mk, associatesEquivIsPrincipal_apply,
-    span_singleton_mul_span_singleton]
+  rw [← quot_out x, ← quot_out y]
+  simp_rw [mk_mul_mk, associatesEquivIsPrincipal_apply, span_singleton_mul_span_singleton]
 
 @[simp]
 theorem associatesEquivIsPrincipal_map_zero :
     (associatesEquivIsPrincipal R 0 : Ideal R) = 0 := by
-  rw [← Associates.mk_zero, ← Associates.quotient_mk_eq_mk, associatesEquivIsPrincipal_apply,
-    Set.singleton_zero, span_zero, zero_eq_bot]
+  rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]
 
 @[simp]
 theorem associatesEquivIsPrincipal_map_one :
     (associatesEquivIsPrincipal R 1 : Ideal R) = 1 := by
-  rw [Associates.one_eq_mk_one, ← Associates.quotient_mk_eq_mk, associatesEquivIsPrincipal_apply,
-    span_singleton_one, one_eq_top]
+  rw [one_eq_mk_one, associatesEquivIsPrincipal_apply, span_singleton_one, one_eq_top]
 
 variable (R) in
 /-- The `MulEquiv` version of `Ideal.associatesEquivIsPrincipal`. -/
 noncomputable def associatesMulEquivIsPrincipal :
     Associates R ≃* (isPrincipalSubmonoid R) where
-  __ := Ideal.associatesEquivIsPrincipal R
+  __ := associatesEquivIsPrincipal R
   map_mul' _ _ := by
     erw [Subtype.ext_iff, associatesEquivIsPrincipal_mul]
     rfl
 
+variable (R) in
+/-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisors generators. -/
+noncomputable def associatesNonZeroDivisorsEquivIsPrincipal :
+    Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} :=
+  calc Associates R⁰ ≃ (Associates R)⁰ := associatesNonZeroDivisorsEquiv.toEquiv.symm
+    _ ≃ {I : {I : Ideal R // IsPrincipal I} // I.1 ∈ (Ideal R)⁰} :=
+      Equiv.subtypeEquiv (associatesEquivIsPrincipal R)
+        (fun x ↦ by rw [← quot_out x, mk_mem_nonZeroDivisors_associates,
+          associatesEquivIsPrincipal_apply, span_singleton_nonZeroDivisors])
+    _ ≃ {I : Ideal R // IsPrincipal I ∧ I ∈ (Ideal R)⁰} :=
+      Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal I) (fun I ↦ I ∈ (Ideal R)⁰)
+    _ ≃ {I : Ideal R // I ∈ (Ideal R)⁰ ∧ IsPrincipal I} := Equiv.setCongr (by simp_rw [and_comm])
+    _ ≃ {I : (Ideal R)⁰ // IsPrincipal I.1} := (Equiv.subtypeSubtypeEquivSubtypeInter _ _).symm
+
+@[simp]
+theorem associatesNonZeroDivisorsEquivIsPrincipal_apply (x : R⁰) :
+    associatesNonZeroDivisorsEquivIsPrincipal R (.mk x) = Ideal.span {(x : R)} := rfl
+
+theorem associatesNonZeroDivisorsEquivIsPrincipal_coe (x : Associates R⁰) :
+    (associatesNonZeroDivisorsEquivIsPrincipal R x : Ideal R) =
+      (associatesEquivIsPrincipal R (associatesNonZeroDivisorsEquiv.symm x)) := rfl
+
+theorem associatesNonZeroDivisorsEquivIsPrincipal_mul (x y : Associates R⁰) :
+    (associatesNonZeroDivisorsEquivIsPrincipal R (x * y) : Ideal R) =
+      (associatesNonZeroDivisorsEquivIsPrincipal R x) *
+        (associatesNonZeroDivisorsEquivIsPrincipal R y) := by
+  simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, _root_.map_mul, Submonoid.coe_mul,
+    associatesEquivIsPrincipal_mul]
+
+@[simp]
+theorem associatesNonZeroDivisorsEquivIsPrincipal_map_one :
+    (associatesNonZeroDivisorsEquivIsPrincipal R 1 : Ideal R) = 1 := by
+  rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_one, OneMemClass.coe_one,
+    associatesEquivIsPrincipal_map_one]
+
+variable (R) in
+/-- The `MulEquiv` version of `Ideal.associatesNonZeroDivisorsEquivIsPrincipal`. -/
+noncomputable def associatesNonZeroDivisorsMulEquivIsPrincipal :
+    Associates R⁰ ≃* (isPrincipalNonZeroDivisorsSubmonoid R) where
+  __ := associatesNonZeroDivisorsEquivIsPrincipal R
+  map_mul' _ _ := by
+    erw [Subtype.ext_iff, Subtype.ext_iff, associatesNonZeroDivisorsEquivIsPrincipal_mul]
+    rfl
+
 end Ideal

Mathlib/RingTheory/Ideal/Operations.lean

@@ -1397,6 +1397,14 @@ theorem Associates.mk_ne_zero' {R : Type*} [CommSemiring R] {r : R} :
   rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]
 #align associates.mk_ne_zero' Associates.mk_ne_zero'
 
+open scoped nonZeroDivisors in
+theorem Ideal.span_singleton_nonZeroDivisors {R : Type*} [CommSemiring R] [NoZeroDivisors R]
+    {r : R} : span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰ := by
+  cases subsingleton_or_nontrivial R
+  · exact ⟨fun _ _ _ ↦ Subsingleton.eq_zero _, fun _ _ _ ↦ Subsingleton.eq_zero _⟩
+  · rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
+      span_singleton_eq_bot]
+
 namespace Submodule
 
 variable {R : Type u} {M : Type v}