Commit 2020-09-02 13:18 96c80e24

feat(ring_theory/localization): Localizations of integral extensions (#3942) The main definition is the algebra induced by localization at an algebra. Given an algebra R → S and a submonoid M of R, as well as localization maps f : R → Rₘ and g : S → Sₘ, there is a natural algebra Rₘ → Sₘ that makes the entire square commute, and this is defined as localization_algebra. The two main theorems are similar but distinct statements about integral elements and localizations:

• is_integral_localization_at_leading_coeff says that if an element x is algebraic over algebra R S, then if we localize to a submonoid containing the leading coefficient the image of x will be integral.
• is_integral_localization says that if R → S is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension.