NYLL
Module

PuncturedSpectrumPurityNormalization.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumPurityNormalization
11 declarations indexed from sourceView source ↗

Module documentation

Canonical normalization under punctured purity

This file compares the canonical function-field normalization attached to a connected punctured cover with an arbitrary finite-etale extension of that cover. Consequently, categorical punctured purity makes the canonical normalization itself finite etale.

Imports5
Imported by4

Declarations

theorem

eqToHom_stalk_eq_stalkCongr

L31 ↗
AlgebraicGeometry.FiniteEtale.eqToHom_stalk_eq_stalkCongr
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · full declaration
theorem eqToHom_stalk_eq_stalkCongr
    (Z : Scheme.{u}) {z z' : Z} (h : z = z') :
    eqToHom (congrArg (fun w ↦ Z.presheaf.stalk w) h) =
      (Z.presheaf.stalkCongr (.of_eq h)).hom := by
  subst z'
  simp
theorem

genericExtensionMorphism_functionFieldMap

L40 ↗
AlgebraicGeometry.FiniteEtale.genericExtensionMorphism_functionFieldMap
Documentation

The generic-point morphism is natural for a dense morphism of integral schemes and the induced literal map on function fields.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem genericExtensionMorphism_functionFieldMap
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
    (f : Y ⟶ X) (hf : DenseRange f) :
    Spec.map (CommRingCat.ofHom (f.functionFieldMap hf)) ≫
        X.genericExtensionMorphism X.functionField =
      Y.genericExtensionMorphism Y.functionField ≫ f
def

normalizationSourceIso

L70 ↗
AlgebraicGeometry.FiniteEtale.normalizationSourceIso
Documentation

Relative normalization is unchanged when the source of the defining morphism is replaced by an isomorphic scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
def normalizationSourceIso
    {Y Y' X : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ X)
    [QuasiCompact f] [QuasiSeparated f] :
    (e.hom ≫ f).normalization ≅ f.normalization
theorem

normalizationSourceIso_hom_fromNormalization

L94 ↗
AlgebraicGeometry.FiniteEtale.normalizationSourceIso_hom_fromNormalization
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem normalizationSourceIso_hom_fromNormalization
    {Y Y' X : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ X)
    [QuasiCompact f] [QuasiSeparated f] :
    (normalizationSourceIso e f).hom ≫ f.fromNormalization =
      (e.hom ≫ f).fromNormalization
def

normalizationSourceIsoOfEq

L102 ↗
AlgebraicGeometry.FiniteEtale.normalizationSourceIsoOfEq
Documentation

Equality-compatible form of normalizationSourceIso.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
def normalizationSourceIsoOfEq
    {Y Y' X : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ X)
    (g : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [QuasiCompact g] [QuasiSeparated g] (h : e.hom ≫ f = g) :
    g.normalization ≅ f.normalization
theorem

normalizationSourceIsoOfEq_hom_fromNormalization

L111 ↗
AlgebraicGeometry.FiniteEtale.normalizationSourceIsoOfEq_hom_fromNormalization
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem normalizationSourceIsoOfEq_hom_fromNormalization
    {Y Y' X : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ X)
    (g : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [QuasiCompact g] [QuasiSeparated g] (h : e.hom ≫ f = g) :
    (normalizationSourceIsoOfEq e f g h).hom ≫
        f.fromNormalization = g.fromNormalization
theorem

isConnected_of_pullback_isConnected_of_isOpenImmersion

L122 ↗
AlgebraicGeometry.FiniteEtale.isConnected_of_pullback_isConnected_of_isOpenImmersion
Documentation

Pullback along a quasi-compact open immersion into an integral scheme reflects connectedness of finite-etale covers.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem isConnected_of_pullback_isConnected_of_isOpenImmersion
    {X U : Scheme.{u}} [IsIntegral X]
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [Nonempty U]
    (Z : FiniteEtale X)
    (hP : IsConnected ((pullback j).obj Z)) : IsConnected Z
theorem

isConnected_of_iso_to_isConnected

L160 ↗
AlgebraicGeometry.FiniteEtale.isConnected_of_iso_to_isConnected
Documentation

Connectedness of a finite-etale cover is transported against an isomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem isConnected_of_iso_to_isConnected
    {X : Scheme.{u}} [ConnectedSpace X]
    (Z W : FiniteEtale X) (e : Z ≅ W) [IsConnected W] : IsConnected Z
theorem

normalization_isFiniteEtale_of_sourceIso_connectedCover

L174 ↗
AlgebraicGeometry.FiniteEtale.normalization_isFiniteEtale_of_sourceIso_connectedCover
Documentation

A morphism obtained from the generic composite of a connected finite-etale cover by replacing its source with an isomorphic scheme has finite-etale relative normalization.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem normalization_isFiniteEtale_of_sourceIso_connectedCover
    {X Y : Scheme.{u}}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (Z : FiniteEtale X) [IsConnected Z] [IsIntegral Z.left]
    (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    (eSource : Y ≅ Spec (.of Z.left.functionField))
    (hSource : eSource.hom ≫ connectedCoverGenericComposite Z = f) :
    IsFiniteEtale f.fromNormalization
theorem

connectedCoverGenericNormalization_isFiniteEtale_of_extension

L221 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalization_isFiniteEtale_of_extension
Documentation

If a connected finite-etale cover of a dense open subscheme has some finite-etale extension, then its canonical function-field normalization is itself finite etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem connectedCoverGenericNormalization_isFiniteEtale_of_extension
    {X U : Scheme.{u}}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
    (j : U ⟶ X) [IsOpenImmersion j]
    (W : FiniteEtale U) [IsConnected W]
    (Z : FiniteEtale X) (e : (pullback j).obj Z ≅ W) :
    IsFiniteEtale
      (connectedCoverGenericComposite W ≫ j).fromNormalization
theorem

connectedPuncturedCoverGenericNormalization_isFiniteEtale_of_hasPuncturedPurity

L302 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverGenericNormalization_isFiniteEtale_of_hasPuncturedPurity
Documentation

Under punctured purity, the canonical function-field normalization of a connected punctured cover is finite etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem connectedPuncturedCoverGenericNormalization_isFiniteEtale_of_hasPuncturedPurity
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsLocalRing R] [IsNoetherianRing R]
    [IsIntegral (Scheme.puncturedSpectrum R)]
    (hpurity : HasPuncturedPurity R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    IsFiniteEtale
      (connectedCoverGenericComposite W ≫
        Scheme.puncturedSpectrumInclusion R).fromNormalization

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