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

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} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {N : Submonoid S} {x : R} :
    x IsLocalization.localizationLocalizationSubmodule M N ∃ (y : N) (z : M), (algebraMap R S) x = y * (algebraMap R S) z
    theorem IsLocalization.localization_localization_surj {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_4) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (x : T) :
    ∃ (y : R × (IsLocalization.localizationLocalizationSubmodule M N)), x * (algebraMap R T) y.2 = (algebraMap R T) y.1
    theorem IsLocalization.localization_localization_exists_of_eq {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid S) (T : Type u_4) [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (x : R) (y : R) :
    (algebraMap R T) x = (algebraMap R T) y∃ (c : (IsLocalization.localizationLocalizationSubmodule M N)), c * x = c * y

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def IsLocalization.localizationAlgebraOfSubmonoidLe {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_4) [CommSemiring T] [Algebra R T] (M : Submonoid R) (N : Submonoid R) (h : M N) [IsLocalization M S] [IsLocalization N T] :

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

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        theorem IsLocalization.isLocalization_of_submonoid_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_4) [CommSemiring T] [Algebra R T] (M : Submonoid R) (N : Submonoid R) (h : M N) [IsLocalization M S] [IsLocalization N T] [Algebra S T] [IsScalarTower R 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} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (M : Submonoid R) (N : Submonoid R) [IsLocalization 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 IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_4) [CommSemiring T] [Algebra R T] {M : Submonoid R} {N : Submonoid R} (h : M N) [IsLocalization M S] [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] (x : R) (y : M) :
        IsLocalization.mk' T x y, = (algebraMap S T) (IsLocalization.mk' S x y)
        theorem IsFractionRing.isFractionRing_of_isLocalization {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_3) (T : Type u_4) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T] (hM : M nonZeroDivisors R) :
        Equations
        • =