1st commit

Mathlib/RingTheory/Ideal/Basic.lean

@@ -518,25 +518,6 @@ theorem span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain 
   apply and_congr <;> rw [span_singleton_le_span_singleton]
 #align ideal.span_singleton_eq_span_singleton Ideal.span_singleton_eq_span_singleton
 
-/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the
-class of `x` to the principal ideal generated by `x`. -/
-noncomputable def associatesEquivIsPrincipal (R : Type*) [CommRing R] [IsDomain R] :
-    Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I} := by
-  refine Equiv.ofBijective (fun x ↦ ⟨Ideal.span {Quot.out x}, ⟨Quot.out x, rfl⟩⟩)
-    ⟨fun  _ _ h ↦ ?_, fun ⟨I, hI⟩ ↦ ?_⟩
-  · rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton] at h
-    exact Quotient.out_equiv_out.mp h
-  · obtain ⟨x, hx⟩ := hI
-    refine ⟨⟦x⟧, ?_⟩
-    rw [Subtype.mk_eq_mk, hx, submodule_span_eq, span_singleton_eq_span_singleton]
-    exact Associates.mk_quot_out x
-
-@[simp]
-theorem associatesEquivIsPrincipal_apply (R : Type*) [CommRing R] [IsDomain R] (x : R) :
-    associatesEquivIsPrincipal R ⟦x⟧ = Ideal.span {x} := by
-  rw [associatesEquivIsPrincipal, Equiv.ofBijective_apply, span_singleton_eq_span_singleton]
-  exact Associates.mk_quot_out x
-
 theorem span_singleton_mul_right_unit {a : α} (h2 : IsUnit a) (x : α) :
     span ({x * a} : Set α) = span {x} := by rw [mul_comm, span_singleton_mul_left_unit h2]
 #align ideal.span_singleton_mul_right_unit Ideal.span_singleton_mul_right_unit

Mathlib/RingTheory/Ideal/Maps.lean

@@ -911,3 +911,69 @@ lemma coe_ideal_map (I : Ideal A) :
     Ideal.map f I = Ideal.map (f : A →+* B) I := rfl
 
 end AlgHom
+
+noncomputable section IsPrincipal
+
+namespace Ideal
+
+open nonZeroDivisors Submodule
+
+variable (R : Type*) [CommRing R] [IsDomain R]
+
+/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the
+class of `x` to the principal ideal generated by `x`. -/
+noncomputable def associatesEquivIsPrincipal :
+    Associates R ≃ {I : Ideal R // IsPrincipal I} := by
+  refine Equiv.ofBijective (fun x ↦ ⟨Ideal.span {Quot.out x}, ⟨Quot.out x, rfl⟩⟩)
+    ⟨fun  _ _ h ↦ ?_, fun ⟨I, hI⟩ ↦ ?_⟩
+  · rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton] at h
+    exact Quotient.out_equiv_out.mp h
+  · obtain ⟨x, hx⟩ := hI
+    refine ⟨⟦x⟧, ?_⟩
+    rw [Subtype.mk_eq_mk, hx, submodule_span_eq, span_singleton_eq_span_singleton]
+    exact Associates.mk_quot_out x
+
+@[simp]
+theorem associatesEquivIsPrincipal_apply (x : R) :
+    associatesEquivIsPrincipal R ⟦x⟧ = Ideal.span {x} := by
+  rw [associatesEquivIsPrincipal, Equiv.ofBijective_apply, span_singleton_eq_span_singleton]
+  exact Associates.mk_quot_out x
+
+theorem associatesEquivIsPrincipal_mem_nonZeroDivisors {x : R} :
+    ↑(Ideal.associatesEquivIsPrincipal R ⟦x⟧) ∈ (Ideal R)⁰ ↔ x ∈ R⁰ := by
+  rw [Ideal.associatesEquivIsPrincipal_apply, mem_nonZeroDivisors_iff, mem_nonZeroDivisors_iff,
+    ← not_iff_not]
+  push_neg
+  refine ⟨fun ⟨I, hI₁, hI₂⟩ ↦ ?_, fun ⟨y, hy₁, hy₂⟩ ↦ ?_⟩
+  · rw [Ideal.zero_eq_bot, Submodule.ne_bot_iff] at hI₂
+    refine ⟨hI₂.choose, ?_, hI₂.choose_spec.2⟩
+    · suffices hI₂.choose * x ∈ I * Ideal.span {x} by
+        rwa [hI₁] at this
+      rw [Ideal.mem_mul_span_singleton]
+      exact ⟨hI₂.choose, hI₂.choose_spec.1, rfl⟩
+  · refine ⟨Ideal.span {y}, ?_, ?_⟩
+    · rw [Ideal.span_singleton_mul_span_singleton, hy₁, Set.singleton_zero, Ideal.span_zero,
+      Ideal.zero_eq_bot]
+    · rw [Ideal.zero_eq_bot, Submodule.ne_bot_iff]
+      exact ⟨y, Ideal.mem_span_singleton_self y, hy₂⟩
+
+/-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisor generators. -/
+def associatesNonZeroDivisorsEquivIsPrincipal :
+    Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} :=
+  calc Associates R⁰ ≃ (Associates R)⁰ := (AssociatesNonZeroDivisorsMulEquiv R).toEquiv
+    _ ≃ {I : {I : Ideal R // IsPrincipal I} // I.1 ∈ (Ideal R)⁰} :=
+      Equiv.subtypeEquiv (Ideal.associatesEquivIsPrincipal R)
+        (fun x ↦ by rw [← Associates.quot_out x, Associates_mk_mem_nonZeroDivisors_iff,
+          Ideal.associatesEquivIsPrincipal_mem_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⁰) :
+    Ideal.associatesNonZeroDivisorsEquivIsPrincipal R ⟦x⟧  = Ideal.span {(x : R)} := by
+  rw [← Ideal.associatesEquivIsPrincipal_apply]
+  rfl
+
+end Ideal

Mathlib/RingTheory/Ideal/Operations.lean

@@ -1388,105 +1388,3 @@ lemma span_smul_eq
   rw [← coe_set_smul, coe_span_smul]
 
 end Submodule
-
-namespace RingHom
-
-variable {A B C : Type*} [Ring A] [Ring B] [Ring C]
-variable (f : A →+* B) (f_inv : B → A)
-
-/-- Auxiliary definition used to define `liftOfRightInverse` -/
-def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : A →+* C)
-    (hg : RingHom.ker f ≤ RingHom.ker g) :
-    B →+* C :=
-  { AddMonoidHom.liftOfRightInverse f.toAddMonoidHom f_inv hf ⟨g.toAddMonoidHom, hg⟩ with
-    toFun := fun b => g (f_inv b)
-    map_one' := by
-      rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker g]
-      apply hg
-      rw [mem_ker f, map_sub f, sub_eq_zero, map_one f]
-      exact hf 1
-    map_mul' := by
-      intro x y
-      rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker g]
-      apply hg
-      rw [mem_ker f, map_sub f, sub_eq_zero, map_mul f]
-      simp only [hf _] }
-#align ring_hom.lift_of_right_inverse_aux RingHom.liftOfRightInverseAux
-
-@[simp]
-theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : A →+* C)
-    (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) :
-    (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a :=
-  f.toAddMonoidHom.liftOfRightInverse_comp_apply f_inv hf ⟨g.toAddMonoidHom, hg⟩ a
-#align ring_hom.lift_of_right_inverse_aux_comp_apply RingHom.liftOfRightInverseAux_comp_apply
-
-/-- `liftOfRightInverse f hf g hg` is the unique ring homomorphism `φ`
-
-* such that `φ.comp f = g` (`RingHom.liftOfRightInverse_comp`),
-* where `f : A →+* B` has a right_inverse `f_inv` (`hf`),
-* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.
-
-See `RingHom.eq_liftOfRightInverse` for the uniqueness lemma.
-
-```
-   A .
-   |  \
- f |   \ g
-   |    \
-   v     \⌟
-   B ----> C
-      ∃!φ
-```
--/
-def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
-    { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) where
-  toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
-  invFun φ := ⟨φ.comp f, fun x hx => (mem_ker _).mpr <| by simp [(mem_ker _).mp hx]⟩
-  left_inv g := by
-    ext
-    simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk]
-  right_inv φ := by
-    ext b
-    simp [liftOfRightInverseAux, hf b]
-#align ring_hom.lift_of_right_inverse RingHom.liftOfRightInverse
-
-/-- A non-computable version of `RingHom.liftOfRightInverse` for when no computable right
-inverse is available, that uses `Function.surjInv`. -/
-@[simp]
-noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) :
-    { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) :=
-  f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf)
-#align ring_hom.lift_of_surjective RingHom.liftOfSurjective
-
-theorem liftOfRightInverse_comp_apply (hf : Function.RightInverse f_inv f)
-    (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) (x : A) :
-    (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x :=
-  f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x
-#align ring_hom.lift_of_right_inverse_comp_apply RingHom.liftOfRightInverse_comp_apply
-
-theorem liftOfRightInverse_comp (hf : Function.RightInverse f_inv f)
-    (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) :
-    (f.liftOfRightInverse f_inv hf g).comp f = g :=
-  RingHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g
-#align ring_hom.lift_of_right_inverse_comp RingHom.liftOfRightInverse_comp
-
-theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : A →+* C)
-    (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C) (hh : h.comp f = g) :
-    h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩ := by
-  simp_rw [← hh]
-  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm
-#align ring_hom.eq_lift_of_right_inverse RingHom.eq_liftOfRightInverse
-
-end RingHom
-
-namespace AlgHom
-
-variable {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
-    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B)
-
-lemma coe_ker : RingHom.ker f = RingHom.ker (f : A →+* B) := rfl
-
-lemma coe_ideal_map (I : Ideal A) :
-    Ideal.map f I = Ideal.map (f : A →+* B) I := rfl
-
-end AlgHom