Zulip Chat Archive
Stream: Is there code for X?
Topic: Localization of modules
Antoine Chambert-Loir (Jul 03 2023 at 19:36):
Mathlib has a lot of stuff about Localization of rings, but apparently very little about localization of modules…
Or did I miss something?
Riccardo Brasca (Jul 03 2023 at 19:59):
I guess that all we have is in Mathlib.Algebra.Module.LocalizedModule.
Jack J Garzella (Jul 10 2023 at 21:33):
@Calvin Lee and myself were hoping to do some stuff in this direction for the adjunction formula, it'll be necessary there.
Eric Wieser (Jul 10 2023 at 21:46):
I had planned to generalize these to be defeq, but the port caught up so I stopped
Jack J Garzella (Jul 11 2023 at 14:45):
Oh I guess I should mention that https://github.com/leanprover-community/mathlib4/pull/5766 will hit at some point, that's something at least
Last updated: Dec 20 2023 at 11:08 UTC