SchemeTheory.nativeNormalizationRingMap
The actual map on integral closures, retaining only its native ring map. The restriction is defined by the existing preservation of integral elements.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u vLean source · statement
def nativeNormalizationRingMap {A : Type u} [CommRing A]
(R : CommAlgCat.{v} A) (S : CommAlgCat.{v} A) (f : R →ₐ[A] S) :
normalizationCommAlgCat A R →+* normalizationCommAlgCat A S