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}
[CommSemiring R]
(M : Submonoid R)
{S : Type u_2}
[CommSemiring 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_isLocalization.
Equations
- IsLocalization.localizationLocalizationSubmodule M N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)
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_map_units
{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]
(y : ↥(IsLocalization.localizationLocalizationSubmodule M N))
:
IsUnit ((algebraMap R T) ↑y)
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 y : R)
:
(algebraMap R T) x = (algebraMap R T) y →
∃ (c : ↥(IsLocalization.localizationLocalizationSubmodule M N)), ↑c * x = ↑c * y
theorem
IsLocalization.localization_localization_isLocalization
{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]
:
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}
[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]
(H : ∀ (x : S), IsUnit x → x ∈ N)
:
IsLocalization (Submonoid.comap (algebraMap R S) 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
IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
(T : Type u_4)
[CommSemiring T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
[IsLocalization M S]
(p : Ideal S)
[Hp : p.IsPrime]
[IsLocalization.AtPrime T p]
:
IsLocalization.AtPrime T (Ideal.comap (algebraMap R 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).
instance
IsLocalization.instAlgebraAtPrimeLocalization
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(p : Ideal (Localization M))
[p.IsPrime]
:
Algebra R (Localization.AtPrime p)
Equations
- IsLocalization.instAlgebraAtPrimeLocalization M p = inferInstance
instance
IsLocalization.instIsScalarTowerLocalizationAtPrime
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(p : Ideal (Localization M))
[p.IsPrime]
:
IsScalarTower R (Localization M) (Localization.AtPrime p)
Equations
- ⋯ = ⋯
instance
IsLocalization.localization_localization_atPrime_is_localization
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(p : Ideal (Localization M))
[p.IsPrime]
:
IsLocalization.AtPrime (Localization.AtPrime p) (Ideal.comap (algebraMap R (Localization M)) p)
Equations
- ⋯ = ⋯
noncomputable def
IsLocalization.localizationLocalizationAtPrimeIsoLocalization
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(p : Ideal (Localization M))
[p.IsPrime]
:
Localization.AtPrime (Ideal.comap (algebraMap R (Localization M)) p) ≃ₐ[R] Localization.AtPrime 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 N : Submonoid R)
(h : M ≤ N)
[IsLocalization M S]
[IsLocalization N T]
:
Algebra S T
Given submonoids M ≤ N of R, this is the canonical algebra structure
of M⁻¹S acting on N⁻¹S.
Equations
- IsLocalization.localizationAlgebraOfSubmonoidLe S T M N h = (IsLocalization.lift ⋯).toAlgebra
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 N : Submonoid R)
(h : M ≤ N)
[IsLocalization M S]
[IsLocalization N T]
:
IsScalarTower R S T
If M ≤ N are submonoids of R, then the natural map M⁻¹S →+* N⁻¹S commutes with the
localization maps
noncomputable instance
IsLocalization.instAlgebraAtPrimeLocalizationNonZeroDivisorsOfIsDomain
{R : Type u_1}
[CommSemiring R]
(x : Ideal R)
[H : x.IsPrime]
[IsDomain R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
IsLocalization.instIsScalarTowerAtPrimeFractionRing
{R : Type u_5}
[CommRing R]
[IsDomain R]
(p : Ideal R)
[p.IsPrime]
:
IsScalarTower R (Localization.AtPrime p) (FractionRing R)
Equations
- ⋯ = ⋯
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 N : Submonoid R)
(h : M ≤ N)
[IsLocalization M S]
[IsLocalization N T]
[Algebra S T]
[IsScalarTower R S T]
:
IsLocalization (Submonoid.map (algebraMap R S) N) 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 N : Submonoid R)
[IsLocalization M S]
(h : M ≤ N)
(h' : ∀ (x : ↥N), ∃ (m : R), m * ↑x ∈ M)
:
IsLocalization N S
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 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)
:
IsFractionRing S T
theorem
IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
[IsDomain 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]
:
IsFractionRing S T