# Documentation

Mathlib.RingTheory.Localization.LocalizationLocalization

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

Instances For
@[simp]
theorem IsLocalization.mem_localizationLocalizationSubmodule {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] {N : } {x : R} :
y z, ↑() 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.snd = ↑() y.fst
theorem IsLocalization.localization_localization_eq_iff_exists {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 : ] [] :

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

noncomputable def IsLocalization.localizationLocalizationAtPrimeIsoLocalization {R : Type u_1} [] (M : ) (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).

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.

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

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 : { x // x N }), m, 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_4) (T : Type u_5) [] [] [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_4) (T : Type u_5) [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] [] [] :