# 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

source
def IsLocalization.localizationLocalizationSubmodule {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) :
Submonoid R

Localizing w.r.t. `M ⊆ R` and then w.r.t. `N ⊆ S = M⁻¹R` is equal to the localization of `R` w.r.t. 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

source
@[simp]
theorem IsLocalization.mem_localizationLocalizationSubmodule {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {N : Submonoid S} {x : R} :
x ∈ localizationLocalizationSubmodule M N ↔ ∃ (y : ↥N) (z : ↥M), (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
source
theorem IsLocalization.localization_localization_map_units {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (y : ↥(localizationLocalizationSubmodule M N)) :
IsUnit ((algebraMap R T) ↑y)
source
theorem IsLocalization.localization_localization_surj {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (x : T) :
∃ (y : R × ↥(localizationLocalizationSubmodule M N)), x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
source
theorem IsLocalization.localization_localization_exists_of_eq {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (x y : R) :
(algebraMap R T) x = (algebraMap R T) y → ∃ (c : ↥(localizationLocalizationSubmodule M N)), ↑c * x = ↑c * y
source
theorem IsLocalization.localization_localization_isLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] :
IsLocalization (localizationLocalizationSubmodule M N) T

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.

source
theorem IsLocalization.localization_localization_isLocalization_of_has_all_units {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (H : ∀ (x : S), IsUnit x → x ∈ N) :
IsLocalization (Submonoid.comap (algebraMap R S) N) T

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.

source
theorem IsLocalization.isLocalization_isLocalization_atPrime_isLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] (p : Ideal S) [Hp : p.IsPrime] [IsLocalization.AtPrime T p] :
IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)

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)`.

source
instance IsLocalization.instAlgebraAtPrimeLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [p.IsPrime] :
Algebra R (Localization.AtPrime p)
Equations

- IsLocalization.instAlgebraAtPrimeLocalization M p = inferInstance

source
instance IsLocalization.instIsScalarTowerLocalizationAtPrime {R : Type u_1} [CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [p.IsPrime] :
IsScalarTower R (Localization M) (Localization.AtPrime p)
source
instance IsLocalization.isLocalization_atPrime_localization_atPrime {R : Type u_1} [CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [p.IsPrime] :
IsLocalization.AtPrime (Localization.AtPrime p) (Ideal.comap (algebraMap R (Localization M)) p)
source
noncomputable def IsLocalization.localizationLocalizationAtPrimeIsoLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [p.IsPrime] :
Localization.AtPrime (Ideal.comap (algebraMap R (Localization M)) p) ≃ₐ[R] Localization.AtPrime 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

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
noncomputable abbrev IsLocalization.localizationAlgebraOfSubmonoidLe {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] :
Algebra S T

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

source
theorem IsLocalization.localization_isScalarTower_of_submonoid_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] :
IsScalarTower R S T

If `M ≤ N` are submonoids of `R`, then the natural map `M⁻¹S →+* N⁻¹S` commutes with the localization maps

source
noncomputable instance IsLocalization.instAlgebraLocalizationAtPrime {R : Type u_1} [CommSemiring R] (x : Ideal R) [H : x.IsPrime] [IsDomain R] :
Algebra (Localization.AtPrime x) (Localization (nonZeroDivisors R))
Equations

- IsLocalization.instAlgebraLocalizationAtPrime x = IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.AtPrime x) (Localization (nonZeroDivisors R)) x.primeCompl (nonZeroDivisors R) ⋯

source
instance IsLocalization.instIsScalarTowerAtPrimeFractionRing {R : Type u_4} [CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime] :
IsScalarTower R (Localization.AtPrime p) (FractionRing R)
source
theorem IsLocalization.isLocalization_of_submonoid_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] :
IsLocalization (Submonoid.map (algebraMap R S) N) T

If `M ≤ N` are submonoids of `R`, then `N⁻¹S` is also the localization of `M⁻¹S` at `N`.

source
theorem IsLocalization.isLocalization_of_is_exists_mul_mem {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (M N : Submonoid R) [IsLocalization M S] (h : M ≤ N) (h' : ∀ (x : ↥N), ∃ (m : R), m * ↑x ∈ M) :
IsLocalization N S

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 localization of `M`.

source
theorem IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] {M N : Submonoid R} (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] (x : R) (y : ↥M) :
mk' T x ⟨↑y, ⋯⟩ = (algebraMap S T) (mk' S x y)
source
theorem IsFractionRing.isFractionRing_of_isLocalization {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) (T : Type u_3) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T] (hM : M ≤ nonZeroDivisors R) :
IsFractionRing S T
source
theorem IsFractionRing.isFractionRing_of_isDomain_of_isLocalization {R : Type u_1} [CommRing R] (M : Submonoid R) [IsDomain R] (S : Type u_2) (T : Type u_3) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T] :
IsFractionRing S T
source
instance IsFractionRing.instAtPrimeFractionRing {R : Type u_2} [CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime] :
IsFractionRing (Localization.AtPrime p) (FractionRing R)