Nyll.EtaleFundamentalGroups.Purity.ClosedComplementStalkSection

Module documentation

Extending an open section across a closed complement point

When all missing points are closed, at each missing point the open pulls back to the actual stalk puncture. Connectedness of its actual strict-stalk puncture therefore extends a finite etale section to the full stalk. The resulting section agrees on the native pullback of the original open, as required for compatible neighborhood spreading.

theorem

exists_stalk_section_of_closed_complement

L32 ↗

AlgebraicGeometry.FiniteEtale.exists_stalk_section_of_closed_complement

Documentation

The local section required in 0BSA, constructed on the actual stalk with its original overlap equation.

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_stalk_section_of_closed_complement
    {X Y : Scheme.{u}} (U : X.Opens)
    (hclosed : ∀ y : X, y ∉ U → IsClosed ({y} : Set X))
    (x : X) (hx : x ∉ U)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ]
    [ConnectedSpace (Scheme.puncturedSpectrum
      (geometricStalk (Spec.map (CommRingCat.ofHom φ))))]
    (f : Y ⟶ X) [IsFinite f] [Etale f]
    (s : U.toScheme ⟶ Y) (hs : s ≫ f = U.ι) :
    ∃ a : Spec (X.presheaf.stalk x) ⟶ Y,
      a ≫ f = X.fromSpecStalk x ∧
      pullback.snd (X.fromSpecStalk x) U.ι ≫ s =
        pullback.fst (X.fromSpecStalk x) U.ι ≫ a

Module documentation

Extending an open section across a closed complement point

Declarations

exists_stalk_section_of_closed_complement