Module

IntegralOpen.lean

Nyll.SchemeTheory.Normalization.IntegralOpen

5 declarations indexed from sourceView source ↗

Module documentation

Extending an integral morphism from a quasi-compact open

Let p : Z ⟶ V be integral and j : V ⟶ Y a quasi-compact open immersion. The relative normalization of Y in p ≫ j restricts over V to Z. The canonical normalization map embeds Z as exactly the inverse image of the original open.

This generalizes the existing normalization core in FiniteEtaleOpen. That file retains its finite-étale/Noetherian compatibility interface. No Noetherian, finite-type or étale hypothesis on p is used here. The construction is the integral-extension step of Stacks Project, Tag 09Z0; it does not construct a finite-presentation approximation.

Imports7

Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by3

def

integralOpenNormalizationIso

L44 ↗

AlgebraicGeometry.Scheme.Hom.integralOpenNormalizationIso

Documentation

The original integral scheme is the actual restriction of its relative normalization to the open subscheme on which it was defined.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {Z V Y : Scheme.{u}} (p : Z ⟶ V) [IsIntegralHom p]
  (j : V ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]

Lean source · statement

def integralOpenNormalizationIso :
    Z ≅ pullback (p ≫ j).fromNormalization j

theorem

integralOpenNormalizationIso_hom_snd

L58 ↗

AlgebraicGeometry.Scheme.Hom.integralOpenNormalizationIso_hom_snd

Documentation

The comparison preserves the original integral projection to the open.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {Z V Y : Scheme.{u}} (p : Z ⟶ V) [IsIntegralHom p]
  (j : V ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]

Lean source · statement

theorem integralOpenNormalizationIso_hom_snd :
    (integralOpenNormalizationIso p j).hom ≫
      pullback.snd (p ≫ j).fromNormalization j = p

theorem

integralOpenNormalizationIso_hom_fst

L67 ↗

AlgebraicGeometry.Scheme.Hom.integralOpenNormalizationIso_hom_fst

Documentation

The other projection is the actual canonical normalization map.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {Z V Y : Scheme.{u}} (p : Z ⟶ V) [IsIntegralHom p]
  (j : V ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]

Lean source · statement

theorem integralOpenNormalizationIso_hom_fst :
    (integralOpenNormalizationIso p j).hom ≫
      pullback.fst (p ≫ j).fromNormalization j = (p ≫ j).toNormalization

theorem

isOpenImmersion_toNormalization_integral_open

L76 ↗

AlgebraicGeometry.Scheme.Hom.isOpenImmersion_toNormalization_integral_open

Documentation

The integral morphism extends to the ambient scheme with the original source as an actual open subscheme of the extension.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {Z V Y : Scheme.{u}} (p : Z ⟶ V) [IsIntegralHom p]
  (j : V ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]

Lean source · statement

theorem isOpenImmersion_toNormalization_integral_open :
    IsOpenImmersion (p ≫ j).toNormalization

theorem

range_toNormalization_integral_open

L83 ↗

AlgebraicGeometry.Scheme.Hom.range_toNormalization_integral_open

Documentation

The open source is precisely the preimage of the original open under the extended integral morphism.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {Z V Y : Scheme.{u}} (p : Z ⟶ V) [IsIntegralHom p]
  (j : V ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]

Lean source · statement

theorem range_toNormalization_integral_open :
    Set.range (p ≫ j).toNormalization =
      (p ≫ j).fromNormalization ⁻¹' Set.range j

Module documentation

Extending an integral morphism from a quasi-compact open

Declarations

integralOpenNormalizationIso

integralOpenNormalizationIso_hom_snd

integralOpenNormalizationIso_hom_fst

isOpenImmersion_toNormalization_integral_open

range_toNormalization_integral_open