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.

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

AffineZariskiSite.PreservesLocalization ((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)) ((AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

source

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

((((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.comp Scheme.Spec).comp forget).IsLocallyDirected

source

instance AlgebraicGeometry.Scheme.Hom.instIsOpenImmersionMapAffineZariskiSiteCompOppositeCommRingCatRightOpOpensOpToOpensFunctorNormalizationDiagramSpec {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Y.AffineZariskiSite} (i : U ⟶ V) :

IsOpenImmersion ((((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.comp Scheme.Spec).map i)

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

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

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

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 (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))) (CategoryTheory.CategoryStruct.comp (IsAffineOpen.fromSpec ⋯) h)

source

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

@[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

@[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

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

IsIntegralHom (fromNormalization f)

source

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 ((normalization f).presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.CategoryStruct.comp (appIso ((normalizationOpenCover f).f U) ⊤).hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso (Opposite.unop (((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.obj U))).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

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

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

IsAffineHom (toNormalization f)

source

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

QuasiCompact (toNormalization f)

source

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

QuasiSeparated (toNormalization f)

source

@[simp]

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

ker (toNormalization f) = ⊥

source

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

IsDominant (toNormalization f)

source

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

IsReduced (normalization f)

Stacks Tag 0AXN

source

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

IsIntegral (normalization f)

source

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)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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

@[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

@[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

@[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

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