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

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] [algebra R S] (N : submonoid S) (T : Type u_4) [comm_ring T] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization M S] [is_localization N T] (H : ∀ (x : S), is_unit xx 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.

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.

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] [algebra R S] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization M S] [is_fraction_ring R T] (hM : M non_zero_divisors R) :
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] [algebra R S] [algebra R T] [algebra S T] [is_scalar_tower R S T] [is_localization M S] [is_fraction_ring R T] :