From 25864f52142f00b5d4424d364a07095db115eee8 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Thu, 11 Jul 2024 10:12:16 +0000 Subject: [PATCH] feat: add a version of `Ideal.associatesEquivIsPrincipal` for generators that are non-zero-divisors (#12780) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR defines the following equiv: ```lean def Ideal.associatesNonZeroDivisorsEquivIsPrincipal : Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} ``` and also a `MulEquiv` version. --- Mathlib/RingTheory/Ideal/IsPrincipal.lean | 84 +++++++++++++++++++---- Mathlib/RingTheory/Ideal/Operations.lean | 8 +++ 2 files changed, 79 insertions(+), 13 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/IsPrincipal.lean b/Mathlib/RingTheory/Ideal/IsPrincipal.lean index 78870f1baf977..b9da1e63ef250 100644 --- a/Mathlib/RingTheory/Ideal/IsPrincipal.lean +++ b/Mathlib/RingTheory/Ideal/IsPrincipal.lean @@ -16,16 +16,23 @@ 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`. -/ @@ -33,7 +40,7 @@ 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 diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 0e89a41781550..b6b1a26686172 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/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}