NYLL
Module

FiniteEtaleOpen.lean

Nyll.SchemeTheory.Normalization.FiniteEtaleOpen
12 declarations indexed from sourceView source ↗

Module documentation

Normalization and finite-etale covers of open subschemes

Let U ⟶ X be an open immersion and let W ⟶ U be finite etale. The relative normalization of X in the composite W ⟶ X, restricted back to U, is canonically isomorphic to W. This comparison does not assert that the normalization is etale over all of X; that is the separate purity step.

Imports6
Imported by2

Declarations

theorem

compOpenImmersionQuasiCompact

L35 ↗
AlgebraicGeometry.FiniteEtale.compOpenImmersionQuasiCompact
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
Lean source · statement
theorem compOpenImmersionQuasiCompact
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    QuasiCompact (W.hom ≫ j)
theorem

compOpenImmersionQuasiSeparated

L43 ↗
AlgebraicGeometry.FiniteEtale.compOpenImmersionQuasiSeparated
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
Lean source · statement
theorem compOpenImmersionQuasiSeparated
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    QuasiSeparated (W.hom ≫ j)
theorem

coverCompOpenImmersionIsPullback

L53 ↗
AlgebraicGeometry.FiniteEtale.coverCompOpenImmersionIsPullback
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
Lean source · statement
theorem coverCompOpenImmersionIsPullback
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    IsPullback (𝟙 W.left) W.hom (W.hom ≫ j) j
def

coverCompOpenImmersionPullbackIso

L62 ↗
AlgebraicGeometry.FiniteEtale.coverCompOpenImmersionPullbackIso
Documentation

A finite-etale cover of an open subscheme is canonically unchanged by pulling its composite to the ambient scheme back to that open subscheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
Lean source · statement
def coverCompOpenImmersionPullbackIso
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    W.left ≅ Limits.pullback (W.hom ≫ j) j
lemma

coverCompOpenImmersionPullbackIso_hom_snd

L68 ↗
AlgebraicGeometry.FiniteEtale.coverCompOpenImmersionPullbackIso_hom_snd
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
Lean source · statement
lemma coverCompOpenImmersionPullbackIso_hom_snd
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    (coverCompOpenImmersionPullbackIso j W).hom ≫
        pullback.snd (W.hom ≫ j) j = W.hom
instance

finiteEtaleRespectsIso

L74 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleRespectsIso
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
Lean source · statement
instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
theorem

pullbackSndCompOpenImmersionFiniteEtale

L87 ↗
AlgebraicGeometry.FiniteEtale.pullbackSndCompOpenImmersionFiniteEtale
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
theorem pullbackSndCompOpenImmersionFiniteEtale
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    IsFiniteEtale (pullback.snd (W.hom ≫ j) j)
def

openImmersionNormalizationIso

L101 ↗
AlgebraicGeometry.FiniteEtale.openImmersionNormalizationIso
Documentation

The cover over U is canonically isomorphic to the pullback to U of the relative normalization of X in the composite cover W ⟶ X.

Local Noetherianity supplies quasi-compactness of the open immersion, which is the only finiteness input needed to form the relative normalization.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
def openImmersionNormalizationIso
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    W.left ≅ Limits.pullback (W.hom ≫ j).fromNormalization j
lemma

openImmersionNormalizationIso_hom_snd

L108 ↗
AlgebraicGeometry.FiniteEtale.openImmersionNormalizationIso_hom_snd
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
lemma openImmersionNormalizationIso_hom_snd
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    (openImmersionNormalizationIso j W).hom ≫
        pullback.snd (W.hom ≫ j).fromNormalization j =
      W.hom
lemma

openImmersion_pullback_fromNormalization_isFiniteEtale

L118 ↗
AlgebraicGeometry.FiniteEtale.openImmersion_pullback_fromNormalization_isFiniteEtale
Documentation

The restriction of the relative normalization to the original open is finite etale.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
lemma openImmersion_pullback_fromNormalization_isFiniteEtale
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    IsFiniteEtale (pullback.snd (W.hom ≫ j).fromNormalization j)
def

normalizationRestriction

L130 ↗
AlgebraicGeometry.FiniteEtale.normalizationRestriction
Documentation

The pullback to U of the relative normalization, packaged as a finite etale object over U.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
def normalizationRestriction
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) : FiniteEtale U
def

normalizationRestrictionIso

L139 ↗
AlgebraicGeometry.FiniteEtale.normalizationRestrictionIso
Documentation

The original finite-etale cover is isomorphic, over U, to the restriction of the relative normalization.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X U : Scheme.{u}}
attribute [local instance] compOpenImmersionQuasiCompact
  compOpenImmersionQuasiSeparated
local instance finiteEtaleRespectsIso :
    MorphismProperty.RespectsIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) := by
  apply MorphismProperty.RespectsIso.mk
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
  · intro _ _ _ _ f hf
    let : IsFinite f := hf.toIsFinite
    let : Etale f := hf.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance
Lean source · statement
def normalizationRestrictionIso
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (W : FiniteEtale U) :
    W ≅ normalizationRestriction j W

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