Equality of ideals from local equality

Stream: Is there code for X?

[Anne Baanen]

I want to prove two ideals are equal by showing they are equal when localized at every maximal ideal. So something like the following:

/-- 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 eq_of_localization_maximal [no_zero_divisors R] {I J : ideal R}
  (h : ∀ (P : ideal R) (hJ : P.is_maximal),
    map (algebra_map R (by exactI localization.at_prime P)) I =
      map (algebra_map R (by exactI localization.at_prime P)) J) :
  I = J := sorry

I recall something along these lines in a recent PR, but I can't find it in the docs: am I misremembering, is it not merged yet, or have I misphrased the statement?

[Junyan Xu]

There's docs#infi_localization_eq_bot but it's for the whole ring, not an arbitrary ideal. The argument probably generalizes though...

[Anne Baanen]

Good idea! Looks like we can replace (submodule.span R {1} : submodule R K).colon (submodule.span R {x}) with I.colon (submodule.span R {x}) and with some further fixes this should arrive at the proof I'm looking at right now.

[Anne Baanen]

#18142