NYLL
Module

LocalToGlobalExtension.lean

Nyll.EtaleFundamentalGroups.Purity.LocalToGlobalExtension
2 declarations indexed from sourceView source ↗

Module documentation

Extending finite étale covers by local purity

On a topologically Noetherian scheme, local purity at all points outside an open implies that every finite étale cover of the open extends globally. At a generic missing point, local purity, spreading, and two-open gluing would enlarge a maximal extension. Consequently its domain is the whole scheme. This proves Stacks Project, Lemma 58.21.6 (tag 0EY7).

Imports9
Imported by1

Declarations

theorem

pullback_essSurj_of_hasPuncturedPurity

L41 ↗
AlgebraicGeometry.FiniteEtale.pullback_essSurj_of_hasPuncturedPurity
Documentation

Local purity along the missing points extends all finite étale covers of the open. Only topological Noetherianity of the ambient scheme is needed in addition to the stated local purity.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
Lean source · statement
theorem pullback_essSurj_of_hasPuncturedPurity
    {X : Scheme.{u}} [NoetherianSpace X] (U : X.Opens)
    (hpurity : ∀ x : X, x ∉ U → HasPuncturedPurity (X.presheaf.stalk x)) :
    (pullback U.ι).EssSurj
theorem

pullback_essSurj_of_isOpenImmersion_of_hasPuncturedPurity

L82 ↗
AlgebraicGeometry.FiniteEtale.pullback_essSurj_of_isOpenImmersion_of_hasPuncturedPurity
Documentation

For an arbitrary open immersion, local purity outside its image extends every finite etale cover of its source. This is the open-immersion form of Stacks Project, Lemma 58.21.6 (0EY7).

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
Lean source · statement
theorem pullback_essSurj_of_isOpenImmersion_of_hasPuncturedPurity
    {U X : Scheme.{u}} [NoetherianSpace X]
    (j : U ⟶ X) [IsOpenImmersion j]
    (hpurity : ∀ x : X, x ∉ Set.range j → HasPuncturedPurity (X.presheaf.stalk x)) :
    (pullback j).EssSurj

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