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.

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.

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.

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))

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

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.

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

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.

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.

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.

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))

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))

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.

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 ⋯)

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)

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)

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

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

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

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)) ≅ { carrier := ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))), commRing := (integralClosure ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))).toCommRing }

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

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))

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

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)

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) ⋯

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

Stacks Tag 03GP

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

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

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

@[simp]

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

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

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

Stacks Tag 0AXN

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

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)

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

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

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

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

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)

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.

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿ normalization (CategoryTheory.CategoryStruct.comp iV f) ≅ normalization f

The normalization of Y in a coproduct is isomorphic to the coproduct of the normalizations in each of the components.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iU f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (normalizationCoprodIso f e).hom) = CategoryTheory.CategoryStruct.comp iU (toNormalization f)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : normalization f ⟶ Z) : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iU f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom h)) = CategoryTheory.CategoryStruct.comp iU (CategoryTheory.CategoryStruct.comp (toNormalization f) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iV f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (normalizationCoprodIso f e).hom) = CategoryTheory.CategoryStruct.comp iV (toNormalization f)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : normalization f ⟶ Z) : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iV f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom h)) = CategoryTheory.CategoryStruct.comp iV (CategoryTheory.CategoryStruct.comp (toNormalization f) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp iU (CategoryTheory.CategoryStruct.comp (toNormalization f) (normalizationCoprodIso f e).inv) = CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iU f)) CategoryTheory.Limits.coprod.inl

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿ normalization (CategoryTheory.CategoryStruct.comp iV f) ⟶ Z) : CategoryTheory.CategoryStruct.comp iU (CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).inv h)) = CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iU f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp iV (CategoryTheory.CategoryStruct.comp (toNormalization f) (normalizationCoprodIso f e).inv) = CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iV f)) CategoryTheory.Limits.coprod.inr

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿ normalization (CategoryTheory.CategoryStruct.comp iV f) ⟶ Z) : CategoryTheory.CategoryStruct.comp iV (CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).inv h)) = CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.CategoryStruct.comp iV f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom (fromNormalization f)) = fromNormalization (CategoryTheory.CategoryStruct.comp iU f)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom (CategoryTheory.CategoryStruct.comp (fromNormalization f) h)) = CategoryTheory.CategoryStruct.comp (fromNormalization (CategoryTheory.CategoryStruct.comp iU f)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom (fromNormalization f)) = fromNormalization (CategoryTheory.CategoryStruct.comp iV f)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).hom (CategoryTheory.CategoryStruct.comp (fromNormalization f) h)) = CategoryTheory.CategoryStruct.comp (fromNormalization (CategoryTheory.CategoryStruct.comp iV f)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] : CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).inv (CategoryTheory.Limits.coprod.desc (fromNormalization (CategoryTheory.CategoryStruct.comp iU f)) (fromNormalization (CategoryTheory.CategoryStruct.comp iV f))) = fromNormalization f

theorem AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Scheme} {iU : U ⟶ X} {iV : V ⟶ X} (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV)) [QuasiCompact iU] [QuasiSeparated iU] [QuasiCompact iV] [QuasiSeparated iV] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalizationCoprodIso f e).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (fromNormalization (CategoryTheory.CategoryStruct.comp iU f)) (fromNormalization (CategoryTheory.CategoryStruct.comp iV f))) h) = CategoryTheory.CategoryStruct.comp (fromNormalization f) h

noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationPullback {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] : normalization (CategoryTheory.Limits.pullback.snd f g) ⟶ CategoryTheory.Limits.pullback (fromNormalization f) g

The comparison lemma between the normalization of the pullback to the pullback of the normalization. This is an isomorphism when g is smooth.

instance AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationPullback {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] : IsIntegralHom (normalizationPullback f g)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] : CategoryTheory.CategoryStruct.comp (normalizationPullback f g) (CategoryTheory.Limits.pullback.snd (fromNormalization f) g) = fromNormalization (CategoryTheory.Limits.pullback.snd f g)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd_assoc {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalizationPullback f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fromNormalization f) g) h) = CategoryTheory.CategoryStruct.comp (fromNormalization (CategoryTheory.Limits.pullback.snd f g)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.Limits.pullback.snd f g)) (CategoryTheory.CategoryStruct.comp (normalizationPullback f g) (CategoryTheory.Limits.pullback.fst (fromNormalization f) g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (toNormalization f)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst_assoc {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] {Z : Scheme} (h : normalization f ⟶ Z) : CategoryTheory.CategoryStruct.comp (toNormalization (CategoryTheory.Limits.pullback.snd f g)) (CategoryTheory.CategoryStruct.comp (normalizationPullback f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fromNormalization f) g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp (toNormalization f) h)

instance AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth {X S Y : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiCompact f] [QuasiSeparated f] [Smooth g] : CategoryTheory.IsIso (normalizationPullback f g)

Normalization commutes with smooth base change.