Module

FundamentalGroup.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.FundamentalGroup

2 declarations indexed from sourceView source ↗

Module documentation

The fundamental group of an actual strictly Henselian spectrum

Henselian reduction identifies finite etale covers with those of the residue field. When this field is separably closed its Galois group is trivial. Base-point comparison gives the result at every geometric point, including points over the fraction field. The geometric etale stalk constructed as a colimit satisfies all these hypotheses internally.

Imports6

Imported by5

theorem

subsingleton_fundamentalGroup_of_strictHenselian

L34 ↗

EtaleFundamentalGroups.StrictHenselian.subsingleton_fundamentalGroup_of_strictHenselian

Documentation

Every geometric fundamental group of a strictly Henselian local ring is trivial. No finiteness or Noetherian hypothesis on the ring is needed.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem subsingleton_fundamentalGroup_of_strictHenselian
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (.of Ω) ⟶ Spec (.of R)) : Subsingleton π₁ᵉᵗ(s)

theorem

subsingleton_fundamentalGroup_geometricStalk

L73 ↗

EtaleFundamentalGroups.StrictHenselian.subsingleton_fundamentalGroup_geometricStalk