Localizations of localizations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Implementation notes #
See src/ring_theory/localization/basic.lean for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
Localizing wrt M ⊆ R and then wrt N ⊆ S = M⁻¹R is equal to the localization of R wrt this
module. See localization_localization_is_localization.
Equations
- is_localization.localization_localization_submodule M N = submonoid.comap (algebra_map R S) (N ⊔ submonoid.map (algebra_map R S) M)
Given submodules M ⊆ R and N ⊆ S = M⁻¹R, with f : R →+* S the localization map, we have
N ⁻¹ S = T = (f⁻¹ (N • f(M))) ⁻¹ R. I.e., the localization of a localization is a localization.
Given submodules M ⊆ R and N ⊆ S = M⁻¹R, with f : R →+* S the localization map, if
N contains all the units of S, then N ⁻¹ S = T = (f⁻¹ N) ⁻¹ R. I.e., the localization of a
localization is a localization.
Given a submodule M ⊆ R and a prime ideal p of S = M⁻¹R, with f : R →+* S the localization
map, then T = Sₚ is the localization of R at f⁻¹(p).
Given a submodule M ⊆ R and a prime ideal p of M⁻¹R, with f : R →+* S the localization
map, then (M⁻¹R)ₚ is isomorphic (as an R-algebra) to the localization of R at f⁻¹(p).
Equations
Given submonoids M ≤ N of R, this is the canonical algebra structure
of M⁻¹S acting on N⁻¹S.
Equations
If M ≤ N are submonoids of R, then the natural map M⁻¹S →+* N⁻¹S commutes with the
localization maps
If M ≤ N are submonoids of R, then N⁻¹S is also the localization of M⁻¹S at N.
If M ≤ N are submonoids of R such that ∀ x : N, ∃ m : R, m * x ∈ M, then the
localization at N is equal to the localizaton of M.