Localizations of localizations #
Implementation notes #
See Mathlib/RingTheory/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_isLocalization
.
Equations
- IsLocalization.localizationLocalizationSubmodule M N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)
Instances For
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)
.
Equations
- IsLocalization.instAlgebraAtPrimeLocalization M p = inferInstance
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
- One or more equations did not get rendered due to their size.
Instances For
Given submonoids M ≤ N
of R
, this is the canonical algebra structure
of M⁻¹S
acting on N⁻¹S
.
Equations
- IsLocalization.localizationAlgebraOfSubmonoidLe S T M N h = (IsLocalization.lift ⋯).toAlgebra
Instances For
If M ≤ N
are submonoids of R
, then the natural map M⁻¹S →+* N⁻¹S
commutes with the
localization maps
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
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
.