Bourbaki elements math alg comm ch IV sec1 no2 prop6

lemma bourbaki_elements_math_alg_comm_chIV_sec1_no2_prop6{R : Type*} [CommRing R] [IsNoetherianRing R]{M : Type*} [AddCommGroup M] [Module R M](S : Submonoid R) (N : Submodule R M) :  (associatedPrimes R N) =    (associatedPrimes R M) \ { p ∈ associatedPrimes R M | p.carrier ∩ S = ∅ } ∧  (associatedPrimes R (M⧸N)) = { p ∈ associatedPrimes R M | p.carrier ∩ S = ∅ }↔ N = LinearMap.ker (LocalizedModule.mkLinearMap S M):= by  constructor  · intro hAss    let K : Submodule R M := LinearMap.ker (LocalizedModule.mkLinearMap S M)    have hNoDisjAssN : ∀ p ∈ associatedPrimes R N, p.carrier ∩ S ≠ ∅ := by      intro p hpN hpDisj      have hpDiff : p ∈ (associatedPrimes R M) \          { p ∈ associatedPrimes R M | p.carrier ∩ S = ∅ } := by        simpa [hAss.1] using hpN      exact hpDiff.2 ⟨hpDiff.1, hpDisj⟩    have hLocAssEmpty :        associatedPrimes (Localization S) (LocalizedModule S N) = ∅ := by      refine Set.Subset.antisymm ?_ (Set.empty_subset _)      intro q hq      have hpre :=        associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule        (S := S) (R' := Localization S)        (f := LocalizedModule.mkLinearMap S N)      have hqComap :          Ideal.comap (algebraMap R (Localization S)) q ∈ associatedPrimes R N := by        have : q ∈ (Ideal.comap (algebraMap R (Localization S))) ⁻¹' (associatedPrimes R N) := by          rw [hpre]          exact hq        exact this      have hqDisjSet :          Disjoint (S : Set R) ((Ideal.comap (algebraMap R (Localization S)) q : Ideal R) : Set R)          :=        (IsLocalization.disjoint_under_iff S (Localization S) q).mpr hq.1.ne_top      have hqDisj : (Ideal.comap (algebraMap R (Localization S)) q).carrier ∩ S = ∅ :=        by simpa [Set.inter_comm] using Set.disjoint_iff_inter_eq_empty.mp hqDisjSet      exact False.elim ((hNoDisjAssN _ hqComap) hqDisj)    have hSubLocN : Subsingleton (LocalizedModule S N) := by      by_contra hns      haveI : Nontrivial (LocalizedModule S N) := not_subsingleton_iff_nontrivial.mp hns      obtain ⟨q, hq⟩ := associatedPrimes.nonempty (Localization S) (LocalizedModule S N)      exact Set.notMem_empty q (hLocAssEmpty ▸ hq)    have hNleK : N ≤ K := by      intro x hxN      have hx0N : LocalizedModule.mkLinearMap S N ⟨x, hxN⟩ = 0 :=        @Subsingleton.elim (LocalizedModule S N) hSubLocN _ _      have hxKerN : ⟨x, hxN⟩ ∈ LinearMap.ker (LocalizedModule.mkLinearMap S N) := by        simpa [LinearMap.mem_ker] using hx0N      rcases (LocalizedModule.mem_ker_mkLinearMap_iff          (S := S) (m := (⟨x, hxN⟩ : N))).1 hxKerN with ⟨s, hsS, hsxN⟩      have hxKerM : x ∈ LinearMap.ker (LocalizedModule.mkLinearMap S M) :=        (LocalizedModule.mem_ker_mkLinearMap_iff (S := S) (m := x)).2        ⟨s, hsS, congrArg Subtype.val hsxN⟩      simpa [K] using hxKerM    have hKleN : K ≤ N := by      intro x hxK      by_contra hxN      let xq : M ⧸ N := N.mkQ x      have hxq_ne : xq ≠ 0 := by simpa [xq, Submodule.Quotient.mk_eq_zero] using hxN      let C : Submodule R (M ⧸ N) := Submodule.span R ({xq} : Set (M ⧸ N))      have hxq_mem_C : xq ∈ C := Submodule.subset_span (by simp [xq])      have hxq_sub_ne : (⟨xq, hxq_mem_C⟩ : C) ≠ 0 := by        intro h        apply hxq_ne <| Subtype.ext_iff.mp h      have hxq_sub_ne' : (0 : C) ≠ ⟨xq, hxq_mem_C⟩ := by        simpa [eq_comm] using hxq_sub_ne      haveI : Nontrivial C := ⟨⟨0, by simp [C]⟩, ⟨⟨xq, hxq_mem_C⟩, by        exact hxq_sub_ne'⟩⟩      obtain ⟨p, hpC⟩ := associatedPrimes.nonempty R C      have hpMN : p ∈ associatedPrimes R (M ⧸ N) :=        associatedPrimes.subset_of_injective (R := R) (f := C.subtype)          (Submodule.injective_subtype C) hpC      have hpDisj : p.carrier ∩ S = ∅ := by        have hpSet : p ∈ { p ∈ associatedPrimes R M | p.carrier ∩ S = ∅ } := by          simpa [hAss.2] using hpMN        exact hpSet.2      rcases hpC with ⟨hpPrime, y, hy⟩      rcases (LocalizedModule.mem_ker_mkLinearMap_iff (S := S) (m := x)).1 (by simpa [K] using hxK)        with ⟨s, hsS, hsx⟩      have hsxq : s • xq = 0 := by        change N.mkQ (s • x) = 0        simp [hsx]      have hsy : s • y = 0 := by        apply Subtype.ext        change s • (y : M ⧸ N) = 0        rcases Submodule.mem_span_singleton.mp y.2 with ⟨r, hr⟩        have hr' : (y : M ⧸ N) = r • xq := by          simpa [eq_comm] using hr        rw [hr']        calc          s • (r • xq) = (s * r) • xq := by simp [smul_smul]          _ = r • (s • xq) := by simp [smul_smul, mul_comm]          _ = 0 := by simp [hsxq]      have hsP : s ∈ p := by        rw [hy]        rw [Ideal.mem_radical_iff]        refine ⟨1, ?_⟩        rw [Submodule.mem_colon_singleton]        simpa using hsy      exact Set.notMem_empty s (hpDisj ▸ ⟨hsP, hsS⟩)    simpa [K] using le_antisymm hNleK hKleN  · intro hN    subst hN    refine ⟨associatedPrimes_ker_mkLinearMap_eq (S := S), ?_⟩    refine le_antisymm ?_ (disjoint_associatedPrimes_subset_associatedPrimes_quot_ker_mkLinearMap      (S := S))    intro p hp    refine ⟨?_, associatedPrimes_quot_ker_mkLinearMap_subset_disjoint (S := S) hp⟩    exact mem_associatedPrimes_of_mem_associatedPrimes_quot_ker_mkLinearMap_of_disjoint      (S := S) hp <| associatedPrimes_quot_ker_mkLinearMap_subset_disjoint (S := S) hp