Nyll.EtaleFundamentalGroups.Purity.GenericComplementStalkSection

Module documentation

+# Extending an open section to a generic complement stalk

At a generic point of an irreducible component of the missing closed set, 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_generic_complement

L31 ↗

AlgebraicGeometry.FiniteEtale.exists_stalk_section_of_generic_complement

Documentation

The local section required at a generic complement point in 0BQF and 0BQG, 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_generic_complement
    {X Y : Scheme.{u}} (U : X.Opens)
    (x : genericPoints {z : X // z ∉ U})
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (φ : X.presheaf.stalk x.1.1 →+* Ω) [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.1.1) ⟶ Y,
      a ≫ f = X.fromSpecStalk x.1.1 ∧
      pullback.snd (X.fromSpecStalk x.1.1) U.ι ≫ s =
        pullback.fst (X.fromSpecStalk x.1.1) U.ι ≫ a

Module documentation

Declarations

exists_stalk_section_of_generic_complement