feat(ring_theory): equality of ideals from locally at each maximal id…

…eal (#18142)

This PR shows that an ideal is equal to another if all localizations at each maximal ideal are equal, by showing an ideal is included in another if this holds locally at each maximal ideal. This generalizes `ideal_eq_zero_of_localization`.

The proof is inspired somewhat by the one for `maximal_spectrum.infi_localization_eq_bot`, although I couldn't find out a neat way to prove it from the new results since it talks about slightly different maps. It would also require readjusting the imports.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Equality.20of.20ideals.20from.20local.20equality





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/group_theory/group_action/sub_mul_action.lean

@@ -70,6 +70,13 @@ lemma mk_smul_mk (r : R) (x : M) (hx : x ∈ s) :
 
 @[to_additive] lemma smul_def (r : R) (x : s) : r • x = ⟨r • x, smul_mem r x.2⟩ := rfl
 
+omit hS
+
+@[simp] lemma forall_smul_mem_iff {R M S : Type*} [monoid R] [mul_action R M]
+  [set_like S M] [smul_mem_class S R M] {N : S} {x : M} :
+  (∀ (a : R), a • x ∈ N) ↔ x ∈ N :=
+⟨λ h, by simpa using h 1, λ h a, smul_mem_class.smul_mem a h⟩
+
 end set_like
 
 /-- A sub_mul_action is a set which is closed under scalar multiplication.  -/

src/ring_theory/ideal/operations.lean

@@ -319,6 +319,17 @@ le_antisymm (le_infi $ λ i, le_infi $ λ j, colon_mono (infi_le _ _) (le_supr _
   map_le_iff_le_comap.2 $ mem_colon'.1 $ have _ := ((mem_infi _).1 H i),
   have _ := ((mem_infi _).1 this j), this)
 
+@[simp] lemma mem_colon_singleton {N : submodule R M} {x : M} {r : R} :
+  r ∈ N.colon (submodule.span R {x}) ↔ r • x ∈ N :=
+calc r ∈ N.colon (submodule.span R {x}) ↔ ∀ (a : R), r • (a • x) ∈ N :
+  by simp [submodule.mem_colon, submodule.mem_span_singleton]
+                                    ... ↔ r • x ∈ N :
+  by { simp_rw [smul_comm r]; exact set_like.forall_smul_mem_iff }
+
+@[simp] lemma _root_.ideal.mem_colon_singleton {I : ideal R} {x r : R} :
+  r ∈ I.colon (ideal.span {x}) ↔ r * x ∈ I :=
+by simp [← ideal.submodule_span_eq, submodule.mem_colon_singleton, smul_eq_mul]
+
 end comm_ring
 
 end submodule

src/ring_theory/local_properties.lean

@@ -29,7 +29,7 @@ In this file, we provide the proofs of various local properties.
 The following properties are covered:
 
 * The triviality of an ideal or an element:
-  `ideal_eq_zero_of_localization`, `eq_zero_of_localization`
+  `ideal_eq_bot_of_localization`, `eq_zero_of_localization`
 * `is_reduced` : `localization_is_reduced`, `is_reduced_of_localization_maximal`.
 * `finite`: `localization_finite`, `finite_of_localization_span`
 * `finite_type`: `localization_finite_type`, `finite_type_of_localization_span`
@@ -221,43 +221,66 @@ end properties
 
 section ideal
 
--- This proof should work for all modules, but we do not know how to localize a module yet.
-/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/
-lemma ideal_eq_zero_of_localization (I : ideal R)
-   (h : ∀ (J : ideal R) (hJ : J.is_maximal),
-      by exactI is_localization.coe_submodule (localization.at_prime J) I = 0) : I = 0 :=
+open_locale non_zero_divisors
+
+/-- Let `I J : ideal R`. If the localization of `I` at each maximal ideal `P` is included in
+the localization of `J` at `P`, then `I ≤ J`. -/
+lemma ideal.le_of_localization_maximal {I J : ideal R}
+  (h : ∀ (P : ideal R) (hP : P.is_maximal),
+    ideal.map (algebra_map R (by exactI localization.at_prime P)) I ≤
+      ideal.map (algebra_map R (by exactI localization.at_prime P)) J) :
+  I ≤ J :=
 begin
-  by_contradiction hI, change I ≠ ⊥ at hI,
-  obtain ⟨x, hx, hx'⟩ := set_like.exists_of_lt hI.bot_lt,
-  rw [submodule.mem_bot] at hx',
-  have H : (ideal.span ({x} : set R)).annihilator ≠ ⊤,
-  { rw [ne.def, submodule.annihilator_eq_top_iff],
-    by_contra,
-    apply hx',
-    rw [← set.mem_singleton_iff, ← @submodule.bot_coe R, ← h],
-    exact ideal.subset_span (set.mem_singleton x) },
-  obtain ⟨p, hp₁, hp₂⟩ := ideal.exists_le_maximal _ H,
-  resetI,
-  specialize h p hp₁,
-  have : algebra_map R (localization.at_prime p) x = 0,
-  { rw ← set.mem_singleton_iff,
-    change algebra_map R (localization.at_prime p) x ∈ (0 : submodule R (localization.at_prime p)),
-    rw ← h,
-    exact submodule.mem_map_of_mem hx },
-  rw is_localization.map_eq_zero_iff p.prime_compl at this,
-  obtain ⟨m, hm⟩ := this,
-  apply m.prop,
-  refine hp₂ _,
-  erw submodule.mem_annihilator_span_singleton,
-  rwa mul_comm at hm,
+  intros x hx,
+  suffices : J.colon (ideal.span {x}) = ⊤,
+  { simpa using submodule.mem_colon.mp
+      (show (1 : R) ∈ J.colon (ideal.span {x}), from this.symm ▸ submodule.mem_top)
+      x (ideal.mem_span_singleton_self x) },
+  refine not.imp_symm (J.colon (ideal.span {x})).exists_le_maximal _,
+  push_neg,
+  introsI P hP le,
+  obtain ⟨⟨⟨a, ha⟩, ⟨s, hs⟩⟩, eq⟩ := (is_localization.mem_map_algebra_map_iff P.prime_compl _).mp
+    (h P hP (ideal.mem_map_of_mem _ hx)),
+  rw [← _root_.map_mul, ← sub_eq_zero, ← map_sub] at eq,
+  obtain ⟨⟨m, hm⟩, eq⟩ := (is_localization.map_eq_zero_iff P.prime_compl _ _).mp eq,
+  refine hs ((hP.is_prime.mem_or_mem (le (ideal.mem_colon_singleton.mpr _))).resolve_right hm),
+  simp only [subtype.coe_mk, sub_mul, sub_eq_zero, mul_assoc] at eq,
+  simpa only [eq, mul_comm] using J.mul_mem_right m ha
 end
 
+/-- Let `I J : ideal R`. If the localization of `I` at each maximal ideal `P` is equal to
+the localization of `J` at `P`, then `I = J`. -/
+theorem ideal.eq_of_localization_maximal {I J : ideal R}
+  (h : ∀ (P : ideal R) (hP : P.is_maximal),
+    ideal.map (algebra_map R (by exactI localization.at_prime P)) I =
+      ideal.map (algebra_map R (by exactI localization.at_prime P)) J) :
+  I = J :=
+le_antisymm
+  (ideal.le_of_localization_maximal (λ P hP, (h P hP).le))
+  (ideal.le_of_localization_maximal (λ P hP, (h P hP).ge))
+
+/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/
+lemma ideal_eq_bot_of_localization' (I : ideal R)
+   (h : ∀ (J : ideal R) (hJ : J.is_maximal),
+      ideal.map (algebra_map R (by exactI (localization.at_prime J))) I = ⊥) : I = ⊥ :=
+ideal.eq_of_localization_maximal (λ P hP, (by simpa using h P hP))
+
+-- TODO: This proof should work for all modules, once we have enough material on submodules of
+-- localized modules.
+/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/
+lemma ideal_eq_bot_of_localization (I : ideal R)
+   (h : ∀ (J : ideal R) (hJ : J.is_maximal),
+      by exactI is_localization.coe_submodule (localization.at_prime J) I = ⊥) : I = ⊥ :=
+ideal_eq_bot_of_localization' _ (λ P hP, (ideal.map_eq_bot_iff_le_ker _).mpr (λ x hx,
+  by { rw [ring_hom.mem_ker, ← submodule.mem_bot R, ← h P hP, is_localization.mem_coe_submodule],
+       exact ⟨x, hx, rfl⟩ }))
+
 lemma eq_zero_of_localization (r : R)
    (h : ∀ (J : ideal R) (hJ : J.is_maximal),
       by exactI algebra_map R (localization.at_prime J) r = 0) : r = 0 :=
 begin
   rw ← ideal.span_singleton_eq_bot,
-  apply ideal_eq_zero_of_localization,
+  apply ideal_eq_bot_of_localization,
   intros J hJ,
   delta is_localization.coe_submodule,
   erw [submodule.map_span, submodule.span_eq_bot],