theorem NormalizationVariety.normalization_is_finite (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] [IsIntegrallyClosed A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] (E : Type u_4) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra A E] [IsScalarTower A K E] [Algebra.IsSeparable K E] : Module.Finite A ↥(integralClosure A E)

The integral closure of a normal finitely-generated k-algebra A in a finite separable field extension E/K of its fraction field is a finite A-module: the normalization map Y → X is finite (Proposition 28, Lecture 17).

theorem NormalizationVariety.normalization_finiteType (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] [IsIntegrallyClosed A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K] [IsScalarTower k A K] (E : Type u_4) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra A E] [IsScalarTower A K E] [Algebra k E] [IsScalarTower k A E] [Algebra.IsSeparable K E] : Algebra.FiniteType k ↥(integralClosure A E)

The normalization is itself a finitely-generated k-algebra: composing the finite A-module structure with finite-type A/k gives finite-type Y/k.

theorem NormalizationVariety.normalization_is_normal (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (E : Type u_3) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra A E] [IsScalarTower A K E] : IsIntegrallyClosed ↥(integralClosure A E)

The integral closure of A in a finite extension of its fraction field is integrally closed; that is, the normalization variety is itself normal.

theorem NormalizationVariety.normalization_map_injective (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (E : Type u_3) [Field E] [Algebra K E] [Algebra A E] [IsScalarTower A K E] : Function.Injective ⇑(algebraMap A ↥(integralClosure A E))

The structure map A → (integral closure of A in E) is injective, so the normalization map Y → X is dominant.

theorem NormalizationVariety.normalization_existence (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] [IsIntegrallyClosed A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K] [IsScalarTower k A K] (E : Type u_4) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra A E] [IsScalarTower A K E] [Algebra k E] [IsScalarTower k A E] [Algebra.IsSeparable K E] : Module.Finite A ↥(integralClosure A E) ∧ Algebra.FiniteType k ↥(integralClosure A E) ∧ IsIntegrallyClosed ↥(integralClosure A E) ∧ Function.Injective ⇑(algebraMap A ↥(integralClosure A E))

Existence of the normalization variety (Proposition 28, Lecture 17): there exists a normal variety Y with a finite dominant map Y → X whose coordinate ring is the integral closure of A in E.

theorem NormalizationVariety.normalization_factorization_scheme {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) (AlgebraicGeometry.Scheme.Hom.fromNormalization f) = f

The normalization factorization: any morphism f : X → Y factors as X → Norm(Y) → Y through the normalization.

theorem NormalizationVariety.normalization_fromNormalization_integral {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] : AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Scheme.Hom.fromNormalization f)

The structural map Norm(Y) → Y from the normalization is an integral morphism.

theorem NormalizationVariety.normalization_toNormalization_dominant {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] : AlgebraicGeometry.IsDominant (AlgebraicGeometry.Scheme.Hom.toNormalization f)

The map X → Norm(Y) into the normalization is dominant.

theorem NormalizationVariety.normalization_sections_isIntegralClosure {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : Nonempty ((AlgebraicGeometry.Scheme.Hom.normalization f).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.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)))))

Local description: on an affine open U ⊆ Y, the sections of the normalization over f⁻¹(U) form the integral closure of Γ(Y,U) in Γ(X, f⁻¹(U)).