Commit 2020-05-22 07:28 80ad9edc
View on Github →refactor(ring_theory/localization): characterise ring localizations up to isomorphism (#2714)
Beginnings of ring_theory/localization refactor from #2675.
It's a bit sad that using the characteristic predicate means Lean can't infer the R-algebra structure of the localization. I've tried to get round this, but I'm not using •, and I've duplicated some fairly random lemmas about modules & algebras to take f as an explicit argument - mostly just what I needed to make fractional_ideal work. Should I duplicate more?
My comments in the fractional_ideal docs about 'preserving definitional equalities' wrt getting an R-module structure from an R-algebra structure: do they make sense? I had some errors about definitional equality of instances which I think I fixed after making sure the R-module structure always came from the R-algebra structure, as well as doing a few other things. I never chased up exactly what the errors were or how they went away, so I'm just guessing at my explanation.
Things I've got left to PR to ring_theory/localization after this:
away(localization at submonoid generated by one element)- localization as a quotient type & proof it satisfies the char pred
- localization at the complement of a prime ideal and the fact this is a local ring
- more lemmas about fields of fractions
- the order embedding for ideals of the localization vs. ideals of the original ring