Localizations of commutative rings at the complement of a prime ideal #
Main definitions #
IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*)expresses thatSis a localization at (the complement of) a prime idealP, as an abbreviation ofIsLocalization P.prime_compl S
Main results #
IsLocalization.AtPrime.isLocalRing: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring
Implementation notes #
See RingTheory.Localization.Basic for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
@[reducible, inline]
abbrev
IsLocalization.AtPrime
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
:
Given a prime ideal P, the typeclass IsLocalization.AtPrime S P states that S is
isomorphic to the localization of R at the complement of P.
Equations
Instances For
@[reducible, inline]
abbrev
Localization.AtPrime
{R : Type u_1}
[CommSemiring R]
(P : Ideal R)
[hp : P.IsPrime]
:
Type u_1
Given a prime ideal P, Localization.AtPrime P is a localization of
R at the complement of P, as a quotient type.
Equations
Instances For
theorem
IsLocalization.AtPrime.nontrivial
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
theorem
IsLocalization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
instance
Localization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(P : Ideal R)
[hp : P.IsPrime]
:
The localization of R at the complement of a prime ideal is a local ring.
theorem
IsLocalization.AtPrime.faithfulSMul
(S : Type u_2)
[CommSemiring S]
(R : Type u_4)
[CommRing R]
[NoZeroDivisors R]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
FaithfulSMul R S
instance
Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors
{R : Type u_4}
[CommRing R]
[NoZeroDivisors R]
(P : Ideal R)
[hp : P.IsPrime]
:
theorem
IsLocalization.isDomain_of_atPrime
{A : Type u_4}
[CommRing A]
[IsDomain A]
(S : Type u_5)
[CommSemiring S]
[Algebra A S]
(P : Ideal A)
[P.IsPrime]
[IsLocalization.AtPrime S P]
:
IsDomain S
This is an IsLocalization.AtPrime version for IsLocalization.isDomain_of_local_atPrime.
def
IsLocalization.AtPrime.orderIsoOfPrime
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
:
The prime ideals in the localization of a commutative ring at a prime ideal I are in order-preserving bijection with the prime ideals contained in I.
Equations
Instances For
@[simp]
theorem
IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(a✝ : { p : Ideal R // p.IsPrime ∧ p ≤ I })
:
↑↑((RelIso.symm (orderIsoOfPrime S I)) a✝) = ⋂ (s : Submodule S S),
⋂ (_ :
↑↑((OrderIso.setCongr (fun (p : Ideal R) => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p)
(fun (p : Ideal R) => p.IsPrime ∧ p ≤ I) ⋯).symm
a✝) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s),
↑s
@[simp]
theorem
IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(a✝ : { p : Ideal S // p.IsPrime })
:
def
IsLocalization.AtPrime.primeSpectrumOrderIso
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
:
The prime spectrum of the localization of a commutative ring R at a prime ideal I are in order-preserving bijection with the interval (-∞, I] in the prime spectrum of R.
Equations
Instances For
@[simp]
theorem
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(a✝ : PrimeSpectrum S)
:
@[simp]
theorem
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(a✝ : ↑(Set.Iic { asIdeal := I, isPrime := hI }))
:
↑((RelIso.symm (primeSpectrumOrderIso S I)) a✝).asIdeal = ⋂ (s : Submodule S S),
⋂ (_ :
↑↑((OrderIso.setCongr (fun (p : Ideal R) => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p)
(fun (p : Ideal R) => p.IsPrime ∧ p ≤ I) ⋯).symm
⟨(↑a✝).asIdeal, ⋯⟩) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s),
↑s
theorem
IsLocalization.AtPrime.isUnit_to_map_iff
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
:
theorem
IsLocalization.AtPrime.to_map_mem_maximal_iff
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(h : IsLocalRing S := ⋯)
:
theorem
IsLocalization.AtPrime.comap_maximalIdeal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(h : IsLocalRing S := ⋯)
:
instance
IsLocalization.AtPrime.liesOver_maximalIdeal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(h : IsLocalRing S := ⋯)
:
theorem
IsLocalization.AtPrime.isUnit_mk'_iff
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(y : ↥I.primeCompl)
:
theorem
IsLocalization.AtPrime.mk'_mem_maximal_iff
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(y : ↥I.primeCompl)
(h : IsLocalRing S := ⋯)
:
theorem
Localization.AtPrime.comap_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
The unique maximal ideal of the localization at I.primeCompl lies over the ideal I.
theorem
Localization.AtPrime.map_eq_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
The image of I in the localization at I.primeCompl is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure AtPrime.isLocalRing
theorem
Localization.AtPrime.eq_maximalIdeal_iff_comap_eq
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
{J : Ideal (Localization.AtPrime I)}
:
Ideal.comap (algebraMap R (Localization.AtPrime I)) J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
theorem
Localization.le_comap_primeCompl_iff
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
{I : Ideal R}
[hI : I.IsPrime]
{J : Ideal P}
[J.IsPrime]
{f : R →+* P}
:
noncomputable def
Localization.localRingHom
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
:
For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the
localization of R at J.comap f to the localization of S at J.
To make this definition more flexible, we allow any ideal I of R as input, together with a proof
that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.
Equations
Instances For
@[simp]
theorem
Localization.localRingHom_to_map
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
(x : R)
:
(localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)
@[simp]
theorem
Localization.localRingHom_mk'
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
(x : R)
(y : ↥I.primeCompl)
:
(localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
instance
Localization.isLocalHom_localRingHom
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[hJ : J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
:
IsLocalHom (localRingHom I J f hIJ)
theorem
Localization.localRingHom_unique
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
{j : Localization.AtPrime I →+* Localization.AtPrime J}
(hj : ∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x))
:
@[simp]
theorem
Localization.localRingHom_id
{R : Type u_1}
[CommSemiring R]
(I : Ideal R)
[hI : I.IsPrime]
:
theorem
Localization.localRingHom_comp
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
{S : Type u_4}
[CommSemiring S]
(J : Ideal S)
[hJ : J.IsPrime]
(K : Ideal P)
[hK : K.IsPrime]
(f : R →+* S)
(hIJ : I = Ideal.comap f J)
(g : S →+* P)
(hJK : J = Ideal.comap g K)
:
noncomputable def
Localization.localAlgHom
{R : Type u_1}
[CommSemiring R]
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
{P : Type u_3}
[CommSemiring P]
[Algebra R P]
(I : Ideal S)
[I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : S →ₐ[R] P)
(hIJ : I = Ideal.comap f J)
:
For an algebra hom f : S →ₐ[R] P and a prime ideal J in P, the induced ring hom from the
localization of R at J ∩ S to the localization of P at J.
Equations
Instances For
@[simp]
theorem
Localization.localAlgHom_apply
{R : Type u_1}
[CommSemiring R]
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
{P : Type u_3}
[CommSemiring P]
[Algebra R P]
(I : Ideal S)
[I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : S →ₐ[R] P)
(hIJ : I = Ideal.comap f J)
(x : Localization.AtPrime I)
:
theorem
Localization.localRingHom_bijective_of_saturated_inf_eq_top
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
{P : Ideal S}
[P.IsPrime]
{s : Subalgebra R S}
(H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤)
(p : Ideal ↥s)
[p.IsPrime]
[P.LiesOver p]
:
Function.Bijective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)
instance
Localization.AtPrime.instIsScalarTower_1
{A : Type u_4}
{B : Type u_5}
{C : Type u_6}
[CommRing A]
[CommRing B]
[CommRing C]
[Algebra A B]
[Algebra A C]
[Algebra B C]
[IsScalarTower A B C]
(p : Ideal A)
[p.IsPrime]
(P : Ideal B)
[P.IsPrime]
[P.LiesOver p]
(Q : Ideal C)
[Q.IsPrime]
[Q.LiesOver P]
[Q.LiesOver p]
:
@[reducible, inline]
noncomputable abbrev
Localization.AtPrime.mapPiEvalRingHom
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
Localization.localRingHom specialized to a projection homomorphism from a product ring.
Equations
Instances For
theorem
Localization.AtPrime.mapPiEvalRingHom_bijective
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
theorem
Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
(mapPiEvalRingHom I).comp (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) = (algebraMap (R i) (Localization.AtPrime I)).comp (Pi.evalRingHom R i)
theorem
Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
{r : (i : ι) → R i}
:
(mapPiEvalRingHom I) ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) = (algebraMap (R i) (Localization.AtPrime I)) (r i)
theorem
Ideal.isPrime_map_of_isLocalizationAtPrime
{R : Type u_1}
[CommSemiring R]
(q : Ideal R)
[q.IsPrime]
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S q]
{p : Ideal R}
[p.IsPrime]
(hpq : p ≤ q)
:
(map (algebraMap R S) p).IsPrime
theorem
Ideal.under_map_of_isLocalizationAtPrime
{R : Type u_1}
[CommSemiring R]
(q : Ideal R)
[q.IsPrime]
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S q]
{p : Ideal R}
[p.IsPrime]
(hpq : p ≤ q)
:
theorem
IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes
{R : Type u_5}
[CommSemiring R]
(p : Ideal R)
(hp : p ∈ minimalPrimes R)
(S : Type u_6)
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S p]
:
theorem
IsLocalization.liesOver_of_isPrime_of_disjoint
{R : Type u_1}
[CommSemiring R]
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
{R' : Type u_5}
{S' : Type u_6}
(M : Submonoid R)
(T : Submonoid S)
[CommSemiring R']
[CommSemiring S']
[Algebra R R']
[Algebra S S']
[Algebra R' S']
[Algebra R S']
[IsScalarTower R S S']
[IsScalarTower R R' S']
[IsLocalization M R']
[IsLocalization T S']
(p : Ideal R)
{P : Ideal S}
[P.IsPrime]
[P.LiesOver p]
(disj : Disjoint ↑T ↑P)
:
(Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)
If R' (resp. S') is the localization of R (resp. S) and
P lies over p then the image of P in S' lies over the image of p in R'.
theorem
Ideal.IsMaximal.of_isLocalization_of_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{J : Ideal S}
[(comap (algebraMap R S) J).IsMaximal]
:
theorem
IsLocalization.AtPrime.isPrime_map_of_liesOver
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(p : Ideal R)
[p.IsPrime]
(Sₚ : Type u_5)
[CommSemiring Sₚ]
[Algebra S Sₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
(P : Ideal S)
[P.IsPrime]
[P.LiesOver p]
:
(Ideal.map (algebraMap S Sₚ) P).IsPrime
theorem
IsLocalization.AtPrime.map_eq_maximalIdeal
{R : Type u_1}
[CommSemiring R]
(p : Ideal R)
[p.IsPrime]
(Rₚ : Type u_4)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
:
instance
IsLocalization.AtPrime.isMaximal_map
{R : Type u_1}
[CommSemiring R]
(p : Ideal R)
[p.IsPrime]
(Rₚ : Type u_4)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
:
(Ideal.map (algebraMap R Rₚ) p).IsMaximal
theorem
IsLocalization.AtPrime.comap_map_of_isMaximal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(p : Ideal R)
[p.IsPrime]
(Sₚ : Type u_5)
[CommSemiring Sₚ]
[Algebra S Sₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
(P : Ideal S)
[P.IsMaximal]
[P.LiesOver p]
:
noncomputable def
IsLocalization.AtPrime.equivQuotMaximalIdeal
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
(Rₚ : Type u_8)
[CommRing Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
:
The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies
IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.
Equations
Instances For
@[simp]
theorem
IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
(Rₚ : Type u_8)
[CommRing Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
(x : R)
:
(equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) ((algebraMap R Rₚ) x)
@[simp]
theorem
IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
(Rₚ : Type u_8)
[CommRing Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
(x : R)
(s : ↥p.primeCompl)
:
(equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) (mk' Rₚ x s)) = (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹
@[deprecated IsLocalization.AtPrime.equivQuotMaximalIdeal (since := "2025-11-13")]
def
equivQuotMaximalIdealOfIsLocalization
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
(Rₚ : Type u_8)
[CommRing Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
:
Alias of IsLocalization.AtPrime.equivQuotMaximalIdeal.
The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies
IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.
Equations
Instances For
theorem
IsLocalization.AtPrime.comap_map_eq_map
{S : Type u_6}
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
{Sₚ : Type u_9}
[CommRing S]
[Algebra R S]
[CommRing Sₚ]
[Algebra S Sₚ]
[Algebra R Sₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
[IsScalarTower R S Sₚ]
:
noncomputable def
IsLocalization.AtPrime.equivQuotientMapMaximalIdeal
(S : Type u_6)
{R : Type u_7}
[CommRing R]
(p : Ideal R)
[p.IsMaximal]
(Rₚ : Type u_8)
[CommRing Rₚ]
[Algebra R Rₚ]
[IsLocalization.AtPrime Rₚ p]
[IsLocalRing Rₚ]
(Sₚ : Type u_9)
[CommRing S]
[Algebra R S]
[CommRing Sₚ]
[Algebra S Sₚ]
[Algebra R Sₚ]
[Algebra Rₚ Sₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
[IsScalarTower R S Sₚ]
[IsScalarTower R Rₚ Sₚ]
[p.IsMaximal]
:
S ⧸ Ideal.map (algebraMap R S) p ≃+* Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ)
The isomorphism S ⧸ pS ≃+* Sₚ ⧸ p·Sₚ, where Sₚ is the localization of S at the (image) of
the complement of p