NYLL
Module

GeometricStalkPuncturedSections.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkPuncturedSections
1 declaration indexed from sourceView source ↗

Module documentation

Descent of finite étale sections from the actual punctured strict stalk

If the puncture of the actual geometric étale stalk of a local ring is connected, every finite étale section on the original puncture extends uniquely over the original local spectrum. The extension is first built over the actual strictly local stalk. Its two restrictions to the fpqc double overlap agree on a dense open obtained by flat going-down. The unramified separated equalizer makes them equal on the entire overlap, so the native fpqc effective epimorphism descends the actual section.

Imports14
Imported by4

Declarations

theorem

existsUnique_section_of_connected_geometricStalk_puncture

L44 ↗
EtaleFundamentalGroups.StrictHenselian.existsUnique_section_of_connected_geometricStalk_puncture
Documentation

Connectedness of the actual punctured strict stalk gives unique extension of finite étale sections over the punctured local spectrum.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · statement
theorem existsUnique_section_of_connected_geometricStalk_puncture
    {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    (φ : R →+* Ω) [IsLocalHom φ]
    [ConnectedSpace
      (Scheme.puncturedSpectrum (geometricStalk (Spec.map (CommRingCat.ofHom φ))))]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsFinite f] [Etale f]
    (s : Scheme.puncturedSpectrum R ⟶ X)
    (hs : s ≫ f = Scheme.puncturedSpectrumInclusion R) :
    ∃! t : Spec (.of R) ⟶ X,
      t ≫ f = 𝟙 _ ∧ Scheme.puncturedSpectrumInclusion R ≫ t = s

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