# mathlibdocumentation

ring_theory.localization.localization_localization

# Localizations of localizations #

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

@[nolint]
def is_localization.localization_localization_submodule {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) :

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
@[simp]
theorem is_localization.mem_localization_localization_submodule {R : Type u_1} [comm_ring R] {M : submonoid R} {S : Type u_2} [comm_ring S] [ S] {N : submonoid S} {x : R} :
∃ (y : N) (z : M), S) x = y * S) z
theorem is_localization.localization_localization_map_units {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ S] [ T]  :
theorem is_localization.localization_localization_surj {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ S] [ T] (x : T) :
∃ (y : , x * T) (y.snd) = T) y.fst
theorem is_localization.localization_localization_eq_iff_exists {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ S] [ T] (x y : R) :
T) x = T) y ∃ (c : , x * c = y * c
theorem is_localization.localization_localization_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ 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 is_localization.localization_localization_is_localization_of_has_all_units {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (N : submonoid S) (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ S] [ T] (H : ∀ (x : S), x 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.

theorem is_localization.is_localization_is_localization_at_prime_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] (T : Type u_4) [comm_ring T] [ T] [ T] [ T] [ S] (p : ideal S) [Hp : p.is_prime]  :
(ideal.comap 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).

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

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

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

Equations
theorem is_localization.localization_is_scalar_tower_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (T : Type u_4) [comm_ring T] [ T] (M N : submonoid R) (h : M N) [ S] [ T] :
T

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

@[protected, instance]
noncomputable def is_localization.localization.algebra {R : Type u_1} [comm_ring R] (x : ideal R) [H : x.is_prime] [is_domain R] :
Equations
theorem is_localization.is_localization_of_submonoid_le {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (T : Type u_4) [comm_ring T] [ T] (M N : submonoid R) (h : M N) [ S] [ T] [ T] [ T] :
T

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

theorem is_localization.is_localization_of_is_exists_mul_mem {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [ S] (M N : submonoid R) [ S] (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 is_fraction_ring.is_fraction_ring_of_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) (T : Type u_3) [comm_ring S] [comm_ring T] [ S] [ T] [ T] [ T] [ S] [ T] (hM : M ) :
theorem is_fraction_ring.is_fraction_ring_of_is_domain_of_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) [is_domain R] (S : Type u_2) (T : Type u_3) [comm_ring S] [comm_ring T] [ S] [ T] [ T] [ T] [ S] [ T] :