Recognizing the relative normalization

Let f : X ⟶ Y be quasi-compact and quasi-separated, and factor it as f = f₁ ≫ f₂ with f₂ : T ⟶ Y integral. The universal property of the relative normalization gives a morphism f.normalizationDesc f₁ f₂ H : f.normalization ⟶ T over Y. This file characterizes when it is an isomorphism, that is, when T is the normalization of Y in X: exactly when, for every affine open U ⊆ Y, the restriction Γ(T, f₂ ⁻¹ U) → Γ(X, f ⁻¹ U) along f₁ is injective with image the integral closure of Γ(Y, U) in Γ(X, f ⁻¹ U).

The main application is to normal schemes. Let T be an integral scheme whose local rings are integrally closed, and g : T ⟶ Y an integral morphism. Then T is the normalization of Y in the function field of T, along the generic point Spec k(T) ⟶ T ⟶ Y. On a nonempty affine open V of T, the ring Γ(T, V) is an integrally closed domain with fraction field k(T) (AlgebraicGeometry.IsAffineOpen.isIntegrallyClosed), and it is integral over Γ(Y, U) when V = g ⁻¹ U, so it is the integral closure of Γ(Y, U) in k(T).

Main results

• AlgebraicGeometry.Scheme.Hom.isIso_normalizationDesc_iff: f.normalizationDesc f₁ f₂ H is an isomorphism if and only if, over every affine open of Y, the sections of T map injectively onto the integral closure.
• AlgebraicGeometry.Scheme.Hom.isIso_fromNormalization_iff: the normalization of Y in X is Y itself if and only if, over every affine open of Y, the sections of Y map injectively onto the integral closure.
• TauCeti.AlgebraicGeometry.isIso_normalizationDesc_fromSpecStalk_genericPoint: an integral scheme with integrally closed local rings, integral over Y, is the normalization of Y in its function field.
• TauCeti.AlgebraicGeometry.isIso_morphismRestrict_fromNormalization_of_isIntegrallyClosed: the normalization of an integral scheme in its function field is an isomorphism over every affine open with integrally closed ring of sections.

References

• The Stacks Project, Tag 035H (relative normalization).

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.normalizationDesc_preimage_preimage {X Y T : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) (U : Y.Opens) : (TopologicalSpace.Opens.map (normalizationDesc f f₁ f₂ H).base).obj ((TopologicalSpace.Opens.map f₂.base).obj U) = (TopologicalSpace.Opens.map (fromNormalization f).base).obj U

The preimage under f.normalizationDesc f₁ f₂ H of the preimage of U under f₂ is the preimage of U in the relative normalization.

theorem AlgebraicGeometry.Scheme.Hom.normalizationDesc_app_normalizationObjIso {X Y T : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) {U : Y.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp (app (normalizationDesc f f₁ f₂ H) ((TopologicalSpace.Opens.map f₂.base).obj U)) (CategoryTheory.CategoryStruct.comp ((normalization f).presheaf.map (CategoryTheory.eqToHom ⋯).op) (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 f₁ ((TopologicalSpace.Opens.map f₂.base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯

Over an affine open U ⊆ Y, the sections of f.normalizationDesc f₁ f₂ H, read in the integral closure of Γ(Y, U) in Γ(X, f ⁻¹ U) through normalizationObjIso, are the restriction maps of f₁.

theorem AlgebraicGeometry.Scheme.Hom.isIso_normalizationDesc_app_iff {X Y T : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) {U : Y.Opens} (hU : IsAffineOpen U) : CategoryTheory.IsIso (app (normalizationDesc f f₁ f₂ H) ((TopologicalSpace.Opens.map f₂.base).obj U)) ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (appLE f₁ ((TopologicalSpace.Opens.map f₂.base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯)) ∧ ∀ (s : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))), (CommRingCat.Hom.hom (app f U)).IsIntegralElem s → s ∈ (CommRingCat.Hom.hom (appLE f₁ ((TopologicalSpace.Opens.map f₂.base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯)).range

Over an affine open U ⊆ Y, the map of sections of f.normalizationDesc f₁ f₂ H is an isomorphism if and only if the restriction Γ(T, f₂ ⁻¹ U) → Γ(X, f ⁻¹ U) along f₁ is injective and its image contains every element integral over Γ(Y, U).

theorem AlgebraicGeometry.Scheme.Hom.isIso_normalizationDesc_iff {X Y T : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂) : CategoryTheory.IsIso (normalizationDesc f f₁ f₂ H) ↔ ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (appLE f₁ ((TopologicalSpace.Opens.map f₂.base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯)) ∧ ∀ (s : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))), (CommRingCat.Hom.hom (app f U)).IsIntegralElem s → s ∈ (CommRingCat.Hom.hom (appLE f₁ ((TopologicalSpace.Opens.map f₂.base).obj U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯)).range

Recognizing the relative normalization. For f = f₁ ≫ f₂ with f₂ integral, the morphism f.normalizationDesc f₁ f₂ H : f.normalization ⟶ T is an isomorphism if and only if, for every affine open U ⊆ Y, the restriction Γ(T, f₂ ⁻¹ U) → Γ(X, f ⁻¹ U) along f₁ is injective and its image contains every element integral over Γ(Y, U). Its image is always contained in the integral closure, since f₂ is integral.

theorem AlgebraicGeometry.Scheme.Hom.isIso_fromNormalization_iff {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] : CategoryTheory.IsIso (fromNormalization f) ↔ ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (app f U)) ∧ ∀ (s : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))), (CommRingCat.Hom.hom (app f U)).IsIntegralElem s → s ∈ (CommRingCat.Hom.hom (app f U)).range

The relative normalization f.normalization ⟶ Y is an isomorphism if and only if, for every affine open U ⊆ Y, the map Γ(Y, U) → Γ(X, f ⁻¹ U) is injective and its image contains every element integral over Γ(Y, U): that is, Y is already the normalization of itself in X.

theorem TauCeti.AlgebraicGeometry.isIso_normalizationDesc_fromSpecStalk_genericPoint {T Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral T] (hT : ∀ (x : ↥T), IsIntegrallyClosed ↑(T.presheaf.stalk x)) (g : T ⟶ Y) [AlgebraicGeometry.IsIntegralHom g] : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.CategoryStruct.comp (T.fromSpecStalk (genericPoint ↥T)) g) (T.fromSpecStalk (genericPoint ↥T)) g ⋯)

A normal scheme integral over Y is the normalization of Y in its function field. If T is an integral scheme whose local rings are integrally closed and g : T ⟶ Y is integral, then the morphism from the relative normalization of Y in Spec k(T), along Spec k(T) ⟶ T ⟶ Y, to T is an isomorphism.

theorem TauCeti.AlgebraicGeometry.isIso_morphismRestrict_fromNormalization_of_isIntegrallyClosed {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral Y] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) [IsIntegrallyClosed ↑(Y.presheaf.obj (Opposite.op U))] : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.fromNormalization (Y.fromSpecStalk (genericPoint ↥Y)) ∣_ U)

The normalization of an integral scheme Y in its function field, along Spec k(Y) ⟶ Y, is an isomorphism over every affine open U whose ring of sections is integrally closed: the integral closure of Γ(Y, U) in its fraction field k(Y) is Γ(Y, U) itself.