[Merged by Bors] - feat(ring_theory/localization): localization of a basis, again

[Vierkantor]

This PR replaces basis.localization with basis.localization_localization, which maps basis ι R S to basis ι Rm Sm, where Rm and Sm are the localizations of R and S at m. This differs from the existing basis.localization by localizing in two places at once, since localizing only the coefficients is probably not useful.

See also: #18150

---

[riccardobrasca]

In my opinion we can delete basis.localization completely, but if you want to keep it (I didn't check if we really use it) can you at least add a comment referring to basis.localization_localization? Thanks!

[Vierkantor]

In my opinion we can delete basis.localization completely, but if you want to keep it (I didn't check if we really use it) can you at least add a comment referring to basis.localization_localization? Thanks!

I can't find it in use but I think it might be useful (at least the linear independent part definitely was useful). Also it turns out you were the one who asked for basis.localization: 239c554 :)

[riccardobrasca]

In my opinion we can delete basis.localization completely, but if you want to keep it (I didn't check if we really use it) can you at least add a comment referring to basis.localization_localization? Thanks!

I can't find it in use but I think it might be useful (at least the linear independent part definitely was useful). Also it turns out you were the one who asked for basis.localization: 239c554 :)

It's definitely my fault, but in my mind I wanted this one and I didn't check carefully the statement 😅

The point is that it is very rare (impossible unless R = Rₛ? I am not sure, but it should be more or less like that, at least for domains) for a Rₛ-module to be free over R, since Rₛ is "too big". For example for ℤ and ℚ it only applies if the vector space is zero-dimensional.

[Vierkantor]

The point is that it is very rare (impossible unless R = Rₛ? I am not sure, but it should be more or less like that, at least for domains) for a Rₛ-module to be free over R, since Rₛ is "too big". For example for ℤ and ℚ it only applies if the vector space is zero-dimensional.

Good point, I've decided to delete basis.localization.

[riccardobrasca]

Thanks!

bors d+

[bors]

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Vierkantor]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests