mathlib documentation

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]

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

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

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] [algebra R S] (T : Type u_4) [comm_ring T] [algebra R T] (M N : submonoid R) (h : M N) [is_localization M S] [is_localization N 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] [algebra R S] (T : Type u_4) [comm_ring T] [algebra R T] (M N : submonoid R) (h : M N) [is_localization M S] [is_localization N T] :

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

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