# 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

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

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
Instances For
@[simp]
theorem IsLocalization.mem_localizationLocalizationSubmodule {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {N : } {x : R} :
∃ (y : N) (z : M), () x = y * () z
theorem IsLocalization.localization_localization_map_units {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (N : ) (T : Type u_4) [] [Algebra R T] [Algebra S T] [] [] [] (y : ) :
IsUnit (() y)
theorem IsLocalization.localization_localization_surj {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (N : ) (T : Type u_4) [] [Algebra R T] [Algebra S T] [] [] [] (x : T) :
∃ (y : ), x * () y.2 = () y.1
theorem IsLocalization.localization_localization_exists_of_eq {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (N : ) (T : Type u_4) [] [Algebra R T] [Algebra S T] [] [] [] (x : R) (y : R) :
() x = () y∃ (c : ), c * x = c * y
theorem IsLocalization.localization_localization_isLocalization {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (N : ) (T : Type u_4) [] [Algebra R T] [Algebra S 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.

theorem IsLocalization.localization_localization_isLocalization_of_has_all_units {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (N : ) (T : Type u_4) [] [Algebra R T] [Algebra S T] [] [] [] (H : ∀ (x : S), x N) :

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.

theorem IsLocalization.isLocalization_isLocalization_atPrime_isLocalization {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] (T : Type u_4) [] [Algebra R T] [Algebra S T] [] [] (p : ) [Hp : p.IsPrime] [] :

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

instance IsLocalization.instAlgebraAtPrimeLocalization {R : Type u_1} [] (M : ) (p : ) [p.IsPrime] :
Equations
• = inferInstance
instance IsLocalization.instIsScalarTowerLocalizationAtPrime {R : Type u_1} [] (M : ) (p : ) [p.IsPrime] :
Equations
• =
instance IsLocalization.localization_localization_atPrime_is_localization {R : Type u_1} [] (M : ) (p : ) [p.IsPrime] :
Equations
• =
noncomputable def IsLocalization.localizationLocalizationAtPrimeIsoLocalization {R : Type u_1} [] (M : ) (p : ) [p.IsPrime] :

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
noncomputable def IsLocalization.localizationAlgebraOfSubmonoidLe {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (T : Type u_4) [] [Algebra R T] (M : ) (N : ) (h : M N) [] [] :

Given submonoids M ≤ N of R, this is the canonical algebra structure of M⁻¹S acting on N⁻¹S.

Equations
• = .toAlgebra
Instances For
theorem IsLocalization.localization_isScalarTower_of_submonoid_le {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (T : Type u_4) [] [Algebra R T] (M : ) (N : ) (h : M N) [] [] :

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

noncomputable instance IsLocalization.instAlgebraAtPrimeLocalizationNonZeroDivisorsOfIsDomain {R : Type u_1} [] (x : ) [H : x.IsPrime] [] :
Equations
• One or more equations did not get rendered due to their size.
theorem IsLocalization.isLocalization_of_submonoid_le {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (T : Type u_4) [] [Algebra R T] (M : ) (N : ) (h : M N) [] [] [Algebra S T] [] :

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

theorem IsLocalization.isLocalization_of_is_exists_mul_mem {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (M : ) (N : ) [] (h : M N) (h' : ∀ (x : N), ∃ (m : R), m * x M) :

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.

theorem IsFractionRing.isFractionRing_of_isLocalization {R : Type u_1} [] (M : ) (S : Type u_3) (T : Type u_4) [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] [] [] (hM : ) :
theorem IsFractionRing.isFractionRing_of_isDomain_of_isLocalization {R : Type u_1} [] (M : ) [] (S : Type u_3) (T : Type u_4) [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] [] [] :