Relative Normalization #

Given a qcqs morphism f : X ⟶ Y, we define the relative normalization f.normalization, along with the maps that f factor into:

f.toNormalization : X ⟶ f.normalization: a dominant morphism
f.fromNormalization : f.normalization ⟶ Y: an integral morphism

It satisfies the universal property: For any factorization X ⟶ T ⟶ Y with T ⟶ Y integral, the map X ⟶ T factors through f.normalization uniquely. The factorization map is AlgebraicGeometry.Scheme.Hom.normalizationDesc, and the uniqueness result is AlgebraicGeometry.Scheme.Hom.normalization.hom_ext.

We also show that normalization commutes with disjoint unions and smooth base change.

source

🔸 coverage

def AlgebraicGeometry.Scheme.Hom.normalizationDiagram {X Y : Scheme} (f : X ⟶ Y) :

CategoryTheory.Functor Y.Opensᵒᵖ CommRingCat

Given a morphism f : X ⟶ Y, this is the presheaf of integral closure of Y in X.

Instances For

source

🔸 coverage

def AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap {X Y : Scheme} (f : X ⟶ Y) :

Y.presheaf ⟶ normalizationDiagram f

The inclusion from the structure presheaf of Y to the integral closure of Y in X.

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

CategoryTheory.NatTrans.Coequifibered ((AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

source

📐 coverage

@[deprecated AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap (since := "2026-02-01")]

theorem AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

CategoryTheory.NatTrans.Coequifibered ((AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

Alias of AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap.

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationGlueData {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

Cover.RelativeGluingData (AffineZariskiSite.directedCover Y)

The diagram of affine schemes that we glue to form the normalization.

Instances For

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

((normalizationGlueData f).functor.comp forget).IsLocallyDirected

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.normalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

Scheme

Given f : X ⟶ Y, f.normalization is the relative normalization of Y in X.

Instances For

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationOpenCover {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

(normalization f).OpenCover

This is the open cover of f.normalization by Spec of integral closures of Γ(Y, U) in Γ(X, f ⁻¹ U) where U ranges over all affine opens.

Instances For

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

X ⟶ normalization f

The dominant morphism into the relative normalization.

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.ι_toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :

CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι (toNormalization f) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom)) ((normalizationOpenCover f).f U))

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) {Z : Scheme} (h : normalization f ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι (CategoryTheory.CategoryStruct.comp (toNormalization f) h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom)) (CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) h))

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

normalization f ⟶ Y

The morphism from the relative normalization to itself. This map is integral.

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.ι_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :

CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) (fromNormalization f) = CategoryTheory.CategoryStruct.comp (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))) (IsAffineOpen.fromSpec ⋯)

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) {Z : Scheme} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) (CategoryTheory.CategoryStruct.comp (fromNormalization f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))) (IsAffineOpen.fromSpec ⋯)) h

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :

(TopologicalSpace.Opens.map (fromNormalization f).base).obj ↑U = opensRange ((normalizationOpenCover f).f U)

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

CategoryTheory.CategoryStruct.comp (toNormalization f) (fromNormalization f) = f

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {Z : Scheme} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (fromNormalization f) h) = CategoryTheory.CategoryStruct.comp f h

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

IsIntegralHom (fromNormalization f)

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationObjIso {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U : Y.Opens} (hU : IsAffineOpen U) :

(normalization f).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (fromNormalization f).base).obj U)) ≅ CommRingCat.of ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))))

The sections of the relative normalization on the preimage of an affine open is isomorphic to the integral closure.

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :

let this := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra; app (toNormalization f) ((TopologicalSpace.Opens.map (fromNormalization f).base).obj ↑U) = CategoryTheory.CategoryStruct.comp (normalizationObjIso f ⋯).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.fromNormalization_app {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U : Y.Opens} (hU : IsAffineOpen U) :

app (fromNormalization f) U = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))))) (normalizationObjIso f hU).inv

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U : Y.Opens} (hU : IsAffineOpen U) {Z : CommRingCat} (h : (normalization f).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (fromNormalization f).base).obj U)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (app (fromNormalization f) U) h = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))))) (CategoryTheory.CategoryStruct.comp (normalizationObjIso f hU).inv h)

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U : Y.Opens} (hU : IsAffineOpen U) :

CategoryTheory.CategoryStruct.comp (normalizationObjIso f hU).hom (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))).val.toRingHom) = appLE (toNormalization f) ((TopologicalSpace.Opens.map (fromNormalization f).base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsIntegralHom f] :

CategoryTheory.IsIso (toNormalization f)

Stacks Tag 03GP

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsAffineHomToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsAffineHom f] :

IsAffineHom (toNormalization f)

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instQuasiCompactToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

QuasiCompact (toNormalization f)

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instQuasiSeparatedToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

QuasiSeparated (toNormalization f)

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.ker_toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

ker (toNormalization f) = ⊥

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :

IsDominant (toNormalization f)

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsReducedNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsReduced X] :

IsReduced (normalization f)

Stacks Tag 0AXN

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsIntegralNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsIntegral X] :

IsIntegral (normalization f)

source

🔸 coverage

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationDesc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) :

normalization f ⟶ T

Given an qcqs morphism f : X ⟶ Y, which factors into X ⟶ T ⟶ Y with T ⟶ Y integral, the map X ⟶ T factors through f.normalization uniquely. (See normalization.hom_ext for the uniqueness result)

Instances For

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) :

CategoryTheory.CategoryStruct.comp (toNormalization f) (normalizationDesc f f₁ f₂ H) = f₁

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) {Z : Scheme} (h : T ⟶ Z) :

CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (normalizationDesc f f₁ f₂ H) h) = CategoryTheory.CategoryStruct.comp f₁ h

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) :

CategoryTheory.CategoryStruct.comp (normalizationDesc f f₁ f₂ H) f₂ = fromNormalization f

source

📐 coverage

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) {Z : Scheme} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (normalizationDesc f f₁ f₂ H) (CategoryTheory.CategoryStruct.comp f₂ h) = CategoryTheory.CategoryStruct.comp (fromNormalization f) h

source

📐 coverage

instance AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationDesc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) :

IsIntegralHom (normalizationDesc f f₁ f₂ H)

source

theorem AlgebraicGeometry.Scheme.Hom.normalization.hom_ext {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {T : Scheme} (f₁ f₂ : normalization f ⟶ T) (g : T ⟶ Y) [IsAffineHom g] (H₁ : CategoryTheory.CategoryStruct.comp (toNormalization f) f₁ = CategoryTheory.CategoryStruct.comp (toNormalization f) f₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ g = fromNormalization f) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ g = fromNormalization f) :

f₁ = f₂

The uniqueness part of the universal property for relative normalization. Suppose f : X ⟶ Y is qcqs and factors into X ⟶ T ⟶ Y with T ⟶ Y affine, then there is at most one map f.normalization ⟶ T that commutes with them.

source

🔸 coverage