Module

RegularStrictHenselian.lean

Nyll.EtaleFundamentalGroups.Purity.RegularStrictHenselian

1 declaration indexed from sourceView source ↗

Module documentation

Simple connectedness of regular strictly Henselian punctures

The punctured spectrum of a regular strictly Henselian local ring of dimension at least two has trivial étale fundamental group at every geometric point. Local purity extends its finite étale covers over the full local spectrum; strict Henselianity makes the fundamental group of that spectrum trivial.

The regular-local purity input is Stacks Project, Lemma 58.21.3 (tag 0BMA). The dimension bound is essential: punctured strictly Henselian discrete valuation rings can have nontrivial ramified covers.

Imports5

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

subsingleton_fundamentalGroup_puncturedSpectrum_of_regular_strictHenselian

L34 ↗

EtaleFundamentalGroups.subsingleton_fundamentalGroup_puncturedSpectrum_of_regular_strictHenselian

Documentation

Every geometric étale fundamental group of the punctured spectrum of a regular strictly Henselian local ring of dimension at least two is trivial.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open AlgebraicGeometry CategoryTheory
universe u

Lean source · statement

theorem subsingleton_fundamentalGroup_puncturedSpectrum_of_regular_strictHenselian
    (R : Type u) [CommRing R] [IsRegularLocalRing R] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim R)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (.of Ω) ⟶ Scheme.puncturedSpectrum R) : Subsingleton π₁ᵉᵗ(s)

Module documentation

Simple connectedness of regular strictly Henselian punctures

Declarations

subsingleton_fundamentalGroup_puncturedSpectrum_of_regular_strictHenselian