Commit 2020-09-02 13:18 96c80e24
View on Github →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 elementx
is algebraic overalgebra R S
, then if we localize to a submonoid containing the leading coefficient the image ofx
will be integral.is_integral_localization
says that ifR → S
is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension.