The source is the actual native principal localization. The target and its coefficient map are the existing native prime-localization owners. The single localization proof below closes the coefficient equation in an R/C-only scope. The base equation then uses only that proved equation and an ordinary coefficient-ring square, supplied in applications by the original inclusion.
The actual native principal localization, bundled with its native ring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wdef principalLocalizationCommRingCat (R : Type v) [CommRing R] (d : R) :
CommRingCat.{v}The native coefficient map into the actual principal localization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wdef principalLocalizationCoefficientMap (R : Type v) [CommRing R] (d : R) :
R →+* principalLocalizationCommRingCat R dA coefficient outside the actual prime becomes a unit under the computed native prime-localization map. This closes the target localization algebra before the principal-localization lift is used.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wtheorem primeLocalizationCoefficientMap_comp_isUnit
{R : Type v} {C : Type w} [CommRing R] [CommRing C]
(f : R →+* C) (d : R) (Q : Ideal C) [Q.IsPrime] (h : f d ∉ Q) :
IsUnit (((primeLocalizationCoefficientMap C Q).comp f) d)The native principal-localization lift of the actual coefficient map.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wdef principalLocalizationToPrimeMap
{R : Type v} {C : Type w} [CommRing R] [CommRing C]
(f : R →+* C) (d : R) (Q : Ideal C) [Q.IsPrime] (h : f d ∉ Q) :
principalLocalizationCommRingCat R d →+* primeLocalizationCommRingCat C QThe native coefficient equation, retained as an equality of computed RingHoms so later applications do not reopen the localization algebras.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wtheorem principalLocalizationToPrimeMap_comp_coefficient
{R : Type v} {C : Type w} [CommRing R] [CommRing C]
(f : R →+* C) (d : R) (Q : Ideal C) [Q.IsPrime] (h : f d ∉ Q) :
(principalLocalizationToPrimeMap f d Q h).comp
(principalLocalizationCoefficientMap R d) =
(primeLocalizationCoefficientMap C Q).comp fThe original base-ring map into the actual principal localization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wdef principalLocalizationBaseMap (A : Type u) (R : Type v)
[CommRing A] [CommRing R] [Algebra A R] (d : R) :
A →+* principalLocalizationCommRingCat R dThe computed base map is the existing principal-localization algebra map. The scalar tower is the native one; no new action is installed.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wtheorem principalLocalizationBaseMap_eq_algebraMap
(A : Type u) (R : Type v) [CommRing A] [CommRing R] [Algebra A R] (d : R) :
principalLocalizationBaseMap A R d =
algebraMap A (localizationAwayCommAlgCat A R d)An ordinary base square on the coefficient rings gives the closed base square for the actual principal-localization lift.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v wtheorem principalLocalizationToPrimeMap_comp_base
(A : Type u) {R : Type v} {C : Type w}
[CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
(f : R →+* C) (d : R) (Q : Ideal C) [Q.IsPrime] (h : f d ∉ Q)
(hbase : f.comp (algebraMap A R) = algebraMap A C) :
(principalLocalizationToPrimeMap f d Q h).comp
(principalLocalizationBaseMap A R d) =
primeLocalizationBaseMap A C Q