Nyll.EtaleFundamentalGroups.Purity.RetrocompactSectionExtension

Module documentation

Global section extension over a retrocompact dense open

Every missing point is closed, so the original open pulls back to its actual local puncture. Connectedness of the punctured strict stalk gives a local section; retrocompact compatible spreading gives a neighborhood section. The already constructed maximum extension therefore covers X.

theorem

exists_section_of_retrocompact_closed_complement

L32 ↗

AlgebraicGeometry.FiniteEtale.exists_section_of_retrocompact_closed_complement

Documentation

Finite etale sections extend globally under the original hypotheses of Stacks 0BSA, without any finite-component or Noetherian hypothesis.

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_retrocompact_closed_complement
    {X Y : Scheme.{u}}
    (U : X.Opens) [QuasiCompact U.ι] (hU : Dense (U : Set X))
    (hclosed : ∀ x : X, x ∉ U → IsClosed ({x} : 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

Global section extension over a retrocompact dense open

Declarations

exists_section_of_retrocompact_closed_complement