Module

ProperNormalization.lean

Nyll.SchemeTheory.Morphisms.ProperNormalization

8 declarations indexed from sourceView source ↗

Module documentation

Proper relative normalization

The canonical relative normalization of a universally closed qcqs morphism has the same sections as the source above every affine open of the base. Over an affine base this identifies the actual normalization with the spectrum of global sections. In particular, the first morphism of a proper relative normalization is proper and surjective.

These are the geometric and section-theoretic parts of Stacks 03GY and 03H2. Geometric connectedness of the first morphism is not asserted here.

References:

https://stacks.math.columbia.edu/tag/03GY
https://stacks.math.columbia.edu/tag/03H2

Imports2

Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Morphisms.Proper

Imported by8

lemma

isIntegral_app_of_universallyClosed

L38 ↗

AlgebraicGeometry.isIntegral_app_of_universallyClosed

Documentation

Universal closedness makes sections integral above every affine base open.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)

Lean source · statement

lemma isIntegral_app_of_universallyClosed [UniversallyClosed f]
    {U : S.Opens} (hU : IsAffineOpen U) :
    (f.app U).hom.IsIntegral

lemma

integralClosure_eq_top_of_universallyClosed

L57 ↗

AlgebraicGeometry.Scheme.Hom.integralClosure_eq_top_of_universallyClosed

Documentation

The integral closure used to build the normalization is the full section ring for a universally closed morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom

Lean source · full declaration

lemma integralClosure_eq_top_of_universallyClosed [UniversallyClosed f]
    {U : S.Opens} (hU : IsAffineOpen U) :
    let : Algebra Γ(S, U) Γ(X, f ⁻¹ᵁ U) := (f.app U).hom.toAlgebra
    integralClosure Γ(S, U) Γ(X, f ⁻¹ᵁ U) = ⊤ := by
  let : Algebra Γ(S, U) Γ(X, f ⁻¹ᵁ U) := (f.app U).hom.toAlgebra
  rw [integralClosure_eq_top_iff, ← algebraMap_isIntegral_iff,
    RingHom.algebraMap_toAlgebra]
  exact isIntegral_app_of_universallyClosed f hU

instance

isAffine_normalization

L68 ↗

AlgebraicGeometry.Scheme.Hom.isAffine_normalization

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

instance isAffine_normalization [IsAffine S] : IsAffine f.normalization

lemma

isIso_toNormalization_app_of_universallyClosed

L73 ↗

AlgebraicGeometry.Scheme.Hom.isIso_toNormalization_app_of_universallyClosed

Documentation

Above an affine base open, the canonical map to the relative normalization induces an isomorphism on sections.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

lemma isIso_toNormalization_app_of_universallyClosed [UniversallyClosed f]
    {U : S.Opens} (hU : IsAffineOpen U) :
    IsIso (f.toNormalization.app (f.fromNormalization ⁻¹ᵁ U))

instance

isIso_toNormalization_appTop_of_universallyClosed

L88 ↗

AlgebraicGeometry.Scheme.Hom.isIso_toNormalization_appTop_of_universallyClosed

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

instance isIso_toNormalization_appTop_of_universallyClosed
    [UniversallyClosed f] [IsAffine S] : IsIso f.toNormalization.appTop

def

normalizationIsoSpec

L94 ↗

AlgebraicGeometry.Scheme.Hom.normalizationIsoSpec

Documentation

Over an affine base, the native relative normalization of a universally closed qcqs morphism is the spectrum of the source's global sections.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

def normalizationIsoSpec [UniversallyClosed f] [IsAffine S] :
    f.normalization ≅ Spec Γ(X, ⊤)

lemma

toNormalization_normalizationIsoSpec_hom

L102 ↗

AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationIsoSpec_hom

Documentation

The identification with the spectrum of global sections carries the native normalization map to the canonical affinization map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

lemma toNormalization_normalizationIsoSpec_hom
    [UniversallyClosed f] [IsAffine S] :
    f.toNormalization ≫ f.normalizationIsoSpec.hom = X.toSpecΓ

instance

isProper_toNormalization

L110 ↗

AlgebraicGeometry.Scheme.Hom.isProper_toNormalization

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

instance isProper_toNormalization [IsProper f] : IsProper f.toNormalization

Module documentation

Proper relative normalization

Declarations