localization of exact sequence

Stream: Is there code for X?

[Yongle Hu]

Let A be a communitive ring, M → N → T be a chain complex of A-modules.

Is there a formalization of "M → N → T is exact if and only if Mₘ → Nₘ → Tₘ is exact for all maximal ideal m of A" in Mathlib now?

I have searched for Mathlib.RingTheory.LocalProperties, but I only found the proof that "the map R → S is surjective if and only if Rₘ → Sₘ is surjective."

[Yongle Hu]

I have found a proof in one direction, specifically in IsLocalizedModule.map_exact, but I still haven't found a proof in the other direction.

[Christian Merten]

I don't think we have it, but docs#LinearMap.toKerLocalized_isLocalizedModule might help.

[Christian Merten]

And I thought we had things about M = 0 being local.

[Christian Merten]

Christian Merten said:

I don't think we have it, but docs#LinearMap.toKerLocalized_isLocalizedModule might help.

You might want to write an analog of docs#LinearMap.localized'_ker_eq_ker_localizedMap for docs#LinearMap.range and then show that equality of submodules (in the sense of docs#Submodule.localized') can be checked at maximal ideals.

[Yongle Hu]

Christian Merten said:

And I thought we had things about M = 0 being local.

Do you mean M = 0 if Mₘ = 0 for all maximal ideals m of A? I couldn't find this theorem either.

[Christian Merten]

Yes, but I can't find it either.

[Yongle Hu]

Christian Merten said:

Yes, but I can't find it either.

OK. I think I will prove it first.