NYLL
Module

NormalizationRemainder.lean

Nyll.SchemeTheory.Etale.NormalizationRemainder
7 declarations indexed from sourceView source ↗

Module documentation

The étale complement of the normalization graph

For a quasi-compact separated étale morphism f : U ⟶ X, Zariski's main theorem embeds U as an open subscheme of its relative normalization Y. The graph of this embedding in U ×[X] Y is both open and closed. Its complement therefore gives an actual étale scheme over Y.

If f is surjective, the image of this complementary scheme contains every point of Y outside U. This supplies the geometric complement used in the induction of Stacks, Tag 09Z0: https://stacks.math.columbia.edu/tag/09Z0

Uniform bounds on geometric fibers, their decrease under specialization, and finite-stage descent are separate inputs. No finite refinement theorem or bound is assumed or asserted here.

Imports13
  • Nyll.SchemeTheory.Morphisms.QuasiFinite
  • Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.AlgebraicGeometry.Morphisms.FlatMono
  • Mathlib.AlgebraicGeometry.Morphisms.Separated
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.AlgebraicGeometry.Normalization
  • Mathlib.AlgebraicGeometry.OpenImmersion
  • Mathlib.AlgebraicGeometry.PullbackCarrier
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.AlgebraicGeometry.ZariskisMainTheorem
  • Mathlib.CategoryTheory.EpiMono
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Imported by2

Declarations

def

normalizationEtaleGraph

L51 ↗
AlgebraicGeometry.Scheme.Hom.normalizationEtaleGraph
Documentation

The graph of the canonical map into the relative normalization.

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 {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
Lean source · statement
def normalizationEtaleGraph : U ⟶ pullback f f.fromNormalization
lemma

normalizationEtaleGraph_fst

L56 ↗
AlgebraicGeometry.Scheme.Hom.normalizationEtaleGraph_fst
Documentation

The first projection retracts the normalization graph.

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 {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
Lean source · statement
lemma normalizationEtaleGraph_fst :
    normalizationEtaleGraph f ≫ pullback.fst f f.fromNormalization = 𝟙 U
lemma

normalizationEtaleGraph_snd

L61 ↗
AlgebraicGeometry.Scheme.Hom.normalizationEtaleGraph_snd
Documentation

The second projection of the graph is the 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 {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
Lean source · statement
lemma normalizationEtaleGraph_snd :
    normalizationEtaleGraph f ≫ pullback.snd f f.fromNormalization = f.toNormalization
theorem

isClopen_range_normalizationEtaleGraph

L67 ↗
AlgebraicGeometry.Scheme.Hom.isClopen_range_normalizationEtaleGraph
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
variable [Etale f]
Lean source · statement
theorem isClopen_range_normalizationEtaleGraph :
    IsClopen (Set.range (normalizationEtaleGraph f))
def

etaleNormalizationRemainder

L91 ↗
AlgebraicGeometry.Scheme.Hom.etaleNormalizationRemainder
Documentation

The open complement of the normalization graph. Composing its inclusion with the second projection is étale by the existing base-change and composition instances.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
variable [Etale f]
Lean source · statement
def etaleNormalizationRemainder : (pullback f f.fromNormalization).Opens
theorem

etaleNormalizationRemainder_isClosed

L96 ↗
AlgebraicGeometry.Scheme.Hom.etaleNormalizationRemainder_isClosed
Documentation

The normalization remainder is also closed in the base-changed cover.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
variable [Etale f]
Lean source · statement
theorem etaleNormalizationRemainder_isClosed :
    IsClosed (etaleNormalizationRemainder f : Set (pullback f f.fromNormalization : Scheme.{u}))
theorem

normalization_boundary_subset_remainder_image

L102 ↗
AlgebraicGeometry.Scheme.Hom.normalization_boundary_subset_remainder_image
Documentation

The normalization remainder covers the entire boundary of the original étale source in its normalization. The cover need not be finite étale.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f]
variable [Etale f]
Lean source · statement
theorem normalization_boundary_subset_remainder_image [Surjective f] :
    (Set.range f.toNormalization)ᶜ ⊆
      Set.range ((etaleNormalizationRemainder f).ι ≫ pullback.snd f f.fromNormalization)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.