Module

ConnectedNormalizationExtension.lean

Nyll.EtaleFundamentalGroups.Purity.ConnectedNormalizationExtension

3 declarations indexed from sourceView source ↗

Module documentation

Packaging connected normalization extensions

For a connected finite-etale cover on a smooth monomorphism, the relative normalization of the ambient scheme in the cover's function field already has a canonical restriction isomorphism. Thus a proof that this one canonical normalization morphism is finite etale packages the desired extension object without making any further choice.

Imports1

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumConnectedRestriction

Imported by5

def

connectedCoverNormalizationExtension

L33 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverNormalizationExtension

Documentation

The canonical relative normalization, packaged as a finite-etale cover once its finite etaleness has been proved.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X S : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]

Lean source · statement

def connectedCoverNormalizationExtension
    (W : FiniteEtale X) [IsConnected W]
    (j : X ⟶ S) [Mono j] [Smooth j] [QuasiCompact j]
    [QuasiSeparated j]
    (hEtale : IsFiniteEtale
      (connectedCoverGenericComposite W ≫ j).fromNormalization) :
    FiniteEtale S

def

connectedCoverNormalizationExtensionRestrictionIso

L45 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverNormalizationExtensionRestrictionIso

Documentation

The canonical normalization extension restricts to the original connected finite-etale cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X S : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]

Lean source · statement

def connectedCoverNormalizationExtensionRestrictionIso
    (W : FiniteEtale X) [IsConnected W]
    (j : X ⟶ S) [Mono j] [Smooth j] [QuasiCompact j]
    [QuasiSeparated j]
    (hEtale : IsFiniteEtale
      (connectedCoverGenericComposite W ≫ j).fromNormalization) :
    (pullback j).obj
        (connectedCoverNormalizationExtension W j hEtale) ≅ W

def

connectedCoverExtensionOfNormalization

L61 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverExtensionOfNormalization

Documentation

Finite etaleness of the canonical normalization is the only remaining input needed to produce an actual extension and its pullback isomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X S : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]

Lean source · statement

def connectedCoverExtensionOfNormalization
    (W : FiniteEtale X) [IsConnected W]
    (j : X ⟶ S) [Mono j] [Smooth j] [QuasiCompact j]
    [QuasiSeparated j]
    (hEtale : IsFiniteEtale
      (connectedCoverGenericComposite W ≫ j).fromNormalization) :
    Σ Z : FiniteEtale S, (pullback j).obj Z ≅ W

Module documentation

Packaging connected normalization extensions

Declarations

connectedCoverNormalizationExtension

connectedCoverNormalizationExtensionRestrictionIso

connectedCoverExtensionOfNormalization