Module

LocallyConnectedSectionExtension.lean

Nyll.EtaleFundamentalGroups.Purity.LocallyConnectedSectionExtension

1 declaration indexed from sourceView source ↗

Module documentation

+# Finite etale section extension from punctured strict-stalk connectedness

For a scheme whose quasi-compact opens have finitely many irreducible components, a finite etale section on a dense open extends globally when the punctured strict stalk at each missing point is connected. A maximum extension is constructed by gluing, and a generic complement point would produce a larger compatible neighborhood, a contradiction.

The strict stalks are the existing geometric stalks for arbitrary chosen separably closed residue geometric points. No reducedness, normality, Noetherianity of rings, or retrocompactness of the dense open is imposed.

Imports5

Nyll.EtaleFundamentalGroups.Purity.GenericComplementStalkSection
Nyll.SchemeTheory.Descent.AffineChartCompatibleStalkSpreading
Nyll.SchemeTheory.Etale.MaximalSectionExtension
Mathlib.AlgebraicGeometry.Properties
Mathlib.Topology.Sober

Imported by2

theorem

exists_section_of_connected_punctured_strict_stalks

L36 ↗

AlgebraicGeometry.FiniteEtale.exists_section_of_connected_punctured_strict_stalks

Documentation

The actual global finite etale section extension used for Stacks 0BQG, and hence for the topologically Noetherian statement 0BQF.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace EtaleFundamentalGroups.StrictHenselian
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem exists_section_of_connected_punctured_strict_stalks
    {X Y : Scheme.{u}}
    (hfin : ∀ A : X.Opens, IsCompact (A : Set X) →
      (irreducibleComponents A.toScheme).Finite)
    (U : X.Opens) (hU : Dense (U : Set X))
    (Ω : X → Type u) [∀ x : X, Field (Ω x)] [∀ x : X, IsSepClosed (Ω x)]
    (φ : ∀ x : X, X.presheaf.stalk x →+* Ω x) [∀ x : X, IsLocalHom (φ x)]
    (hconn : ∀ x : X, x ∉ U → ConnectedSpace (Scheme.puncturedSpectrum
      (geometricStalk (Spec.map (CommRingCat.ofHom (φ x))))))
    (f : Y ⟶ X) [IsFinite f] [Etale f]
    (s : U.toScheme ⟶ Y) (hs : s ≫ f = U.ι) :
    ∃ t : X ⟶ Y, t ≫ f = 𝟙 X ∧ U.ι ≫ t = s

Module documentation

Declarations

exists_section_of_connected_punctured_strict_stalks