Module

GeometricStalk.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk

12 declarations indexed from sourceView source ↗

Module documentation

The local ring of a geometric point on the étale site

For an actual geometric point s : Spec Ω ⟶ S, take the filtered colimit of the rings of global sections on all pointed étale neighborhoods of s. The index category and its filteredness come from Scheme.pointEtaleNeighborhoods. The construction also applies to an arbitrary field-valued point; separable closedness is needed only when viewing it as a point of the étale topology. This constructs a commutative ring, its maps from the neighborhoods, and its evaluation homomorphism to Ω; no ring or universal property is postulated.

An element of this ring is a unit exactly when its evaluation is nonzero. For the nontrivial direction, represent the element on an étale neighborhood and replace that neighborhood by the basic open where the section is invertible. The geometric point lifts to this basic open because its value is nonzero. It follows that the constructed ring is local.

This is the actual étale-stalk construction needed for strict henselization. The Henselian property, the identification of its residue field with the separable closure of the original residue field, and the subsequent inertia comparison are separate statements, not fields assumed by this construction.

Imports12

Mathlib.Algebra.Category.Ring.Colimits
Mathlib.Algebra.Category.Ring.FilteredColimits
Nyll.EtaleFundamentalGroups.StrictHenselian.PointedEtaleNeighborhoods
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Filtered.Basic
Mathlib.CategoryTheory.Discrete.Basic
Mathlib.Geometry.RingedSpace.Basic
Mathlib.RingTheory.LocalRing.Basic

Imported by13

def

etaleSections

L53 ↗

EtaleFundamentalGroups.StrictHenselian.etaleSections

Documentation

Sections of the actual schemes in the small étale site.

Source context 4 commands

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

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

Lean source · statement

def etaleSections (S : Scheme.{u}) : S.Etaleᵒᵖ ⥤ CommRingCat.{u}

def

geometricStalk

L60 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk

Documentation

The filtered colimit of rings of sections on pointed étale neighborhoods.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

def geometricStalk : CommRingCat.{u}

theorem

geometricStalk_eq_smallEtale_presheafFiber

L66 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_eq_smallEtale_presheafFiber

Documentation

For a separably closed field, this is literally the existing presheaf fiber of the small étale site. Both constructions use the same functor of points and the same chosen colimit; topology is not used by presheafFiber.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalk_eq_smallEtale_presheafFiber [IsSepClosed Ω] :
    geometricStalk s = (Scheme.pointSmallEtale s).presheafFiber.obj (etaleSections S)

def

geometricStalkGerm

L72 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm

Documentation

The ring homomorphism from an actual pointed étale neighborhood to the geometric stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

def geometricStalkGerm (W : S.Etale)
    (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W) :
    Γ(W.left, ⊤) ⟶ geometricStalk s

def

geometricStalkEvaluation

L79 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkEvaluation

Documentation

Evaluation in Ω, obtained by descending the section maps along the geometric points of the neighborhoods.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

def geometricStalkEvaluation : geometricStalk s ⟶ CommRingCat.of Ω

theorem

geometricStalkGerm_evaluation

L92 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_evaluation

Documentation

Evaluation of a germ is evaluation of its representing section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalkGerm_evaluation (W : S.Etale)
    (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W) :
    geometricStalkGerm s W t ≫ geometricStalkEvaluation s =
      t.left.appTop ≫ (Scheme.ΓSpecIso (CommRingCat.of Ω)).hom

theorem

geometricStalk_exists_representative

L100 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_representative

Documentation

Every element of the constructed colimit is represented on an actual pointed étale neighborhood.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalk_exists_representative (a : geometricStalk s) :
    ∃ (W : S.Etale) (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W)
      (z : Γ(W.left, ⊤)), geometricStalkGerm s W t z = a

theorem

geometricStalk_exists_representatives

L108 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_representatives

Documentation

A finite family of germs has representatives on one actual pointed étale neighborhood. The common neighborhood is supplied by cofilteredness of the category of elements of the geometric-point functor.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalk_exists_representatives {ι : Type*} [Finite ι]
    (a : ι → geometricStalk s) :
    ∃ (W : S.Etale) (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W)
      (z : ι → Γ(W.left, ⊤)), ∀ i, geometricStalkGerm s W t (z i) = a i

instance

geometricStalk_nontrivial

L130 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_nontrivial

Documentation

The constructed ring has distinct zero and one, since it has its actual evaluation homomorphism to a field.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

instance geometricStalk_nontrivial : Nontrivial (geometricStalk s)

theorem

geometricStalk_isUnit_of_evaluation_ne_zero

L135 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_isUnit_of_evaluation_ne_zero

Documentation

A nonzero value at the geometric point makes a germ invertible: restrict its representative to its basic open and use the filtered-colimit relation.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalk_isUnit_of_evaluation_ne_zero
    (a : geometricStalk s) (ha : geometricStalkEvaluation s a ≠ 0) :
    IsUnit a

theorem

geometricStalk_isUnit_iff

L188 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_isUnit_iff

Documentation

Units in the étale geometric stalk are detected by their actual values.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

theorem geometricStalk_isUnit_iff (a : geometricStalk s) :
    IsUnit a ↔ geometricStalkEvaluation s a ≠ 0

instance

geometricStalk_isLocalRing

L196 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_isLocalRing

Documentation

The étale geometric stalk constructed as a filtered colimit is a local ring.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
  (s : Spec (.of Ω) ⟶ S)

Lean source · statement

instance geometricStalk_isLocalRing : IsLocalRing (geometricStalk s)

Module documentation

The local ring of a geometric point on the étale site

Declarations