Module

NormalizationFiniteFactor.lean

Nyll.SchemeTheory.Morphisms.NormalizationFiniteFactor

11 declarations indexed from sourceView source ↗

Module documentation

Finite open factors in a normalization fiber

For a quasi-finite separated morphism of finite type, Zariski's main theorem embeds its source into its relative normalization. After arbitrary base change, an open subscheme finite over the new base is both open and closed in the base change of that normalization. The map into the normalization fiber is constructed from the canonical normalization map.

Imports3

Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.CategoryTheory.MorphismProperty.Limits

Imported by1

Nyll.SchemeTheory.Morphisms.All

def

normalizationBaseChange

L35 ↗

AlgebraicGeometry.Scheme.Hom.normalizationBaseChange

Documentation

The base change of the canonical map into the relative normalization.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

def normalizationBaseChange :
    pullback f g ⟶ pullback f.fromNormalization g

lemma

normalizationBaseChange_fst

L42 ↗

AlgebraicGeometry.Scheme.Hom.normalizationBaseChange_fst

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

lemma normalizationBaseChange_fst :
    normalizationBaseChange f g ≫ pullback.fst f.fromNormalization g =
      pullback.fst f g ≫ f.toNormalization

lemma

normalizationBaseChange_snd

L48 ↗

AlgebraicGeometry.Scheme.Hom.normalizationBaseChange_snd

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

lemma normalizationBaseChange_snd :
    normalizationBaseChange f g ≫ pullback.snd f.fromNormalization g =
      pullback.snd f g

instance

isOpenImmersion_normalizationBaseChange

L53 ↗

AlgebraicGeometry.Scheme.Hom.isOpenImmersion_normalizationBaseChange

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

instance isOpenImmersion_normalizationBaseChange
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] :
    IsOpenImmersion (normalizationBaseChange f g)

def

normalizationFiniteFactor

L64 ↗

AlgebraicGeometry.Scheme.Hom.normalizationFiniteFactor

Documentation

An open factor of the base-changed source maps canonically into the base change of the relative normalization.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

def normalizationFiniteFactor (i : T ⟶ pullback f g) :
    T ⟶ pullback f.fromNormalization g

lemma

normalizationFiniteFactor_fst

L69 ↗

AlgebraicGeometry.Scheme.Hom.normalizationFiniteFactor_fst

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

lemma normalizationFiniteFactor_fst (i : T ⟶ pullback f g) :
    normalizationFiniteFactor f g i ≫ pullback.fst f.fromNormalization g =
      i ≫ pullback.fst f g ≫ f.toNormalization

lemma

normalizationFiniteFactor_snd

L75 ↗

AlgebraicGeometry.Scheme.Hom.normalizationFiniteFactor_snd

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

lemma normalizationFiniteFactor_snd (i : T ⟶ pullback f g) :
    normalizationFiniteFactor f g i ≫ pullback.snd f.fromNormalization g =
      i ≫ pullback.snd f g

instance

isOpenImmersion_normalizationFiniteFactor

L80 ↗

AlgebraicGeometry.Scheme.Hom.isOpenImmersion_normalizationFiniteFactor

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

instance isOpenImmersion_normalizationFiniteFactor
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    (i : T ⟶ pullback f g) [IsOpenImmersion i] :
    IsOpenImmersion (normalizationFiniteFactor f g i)

instance

isFinite_normalizationFiniteFactor

L89 ↗

AlgebraicGeometry.Scheme.Hom.isFinite_normalizationFiniteFactor

Documentation

Finiteness over the base implies finiteness of the map into the normalization fiber, since that fiber is separated over the base.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

instance isFinite_normalizationFiniteFactor (i : T ⟶ pullback f g)
    [IsFinite (i ≫ pullback.snd f g)] :
    IsFinite (normalizationFiniteFactor f g i)

instance

isClosedImmersion_normalizationFiniteFactor

L100 ↗

AlgebraicGeometry.Scheme.Hom.isClosedImmersion_normalizationFiniteFactor

Documentation

A finite open factor is closed in the normalization fiber.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

instance isClosedImmersion_normalizationFiniteFactor
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    (i : T ⟶ pullback f g) [IsOpenImmersion i]
    [IsFinite (i ≫ pullback.snd f g)] :
    IsClosedImmersion (normalizationFiniteFactor f g i)

lemma

isClopen_range_normalizationFiniteFactor

L109 ↗

AlgebraicGeometry.Scheme.Hom.isClopen_range_normalizationFiniteFactor

Documentation

The canonical image of a finite open factor is a clopen subset of the normalization fiber.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.Scheme.Hom
variable {X S Z T : Scheme.{u}} (f : X ⟶ S) (g : Z ⟶ S)
    [QuasiCompact f] [IsSeparated f]

Lean source · statement

lemma isClopen_range_normalizationFiniteFactor
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    (i : T ⟶ pullback f g) [IsOpenImmersion i]
    [IsFinite (i ≫ pullback.snd f g)] :
    IsClopen (Set.range (normalizationFiniteFactor f g i))

Module documentation

Finite open factors in a normalization fiber

Declarations