Module

GeometricStalkHenselian.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselian

5 declarations indexed from sourceView source ↗

Module documentation

Henselianity of the constructed geometric étale stalk

The ring in GeometricStalk is the actual filtered colimit over pointed étale neighborhoods. A monic polynomial descends to one neighborhood because it has only finitely many coefficients. A simple root at the geometric point then defines a further neighborhood using the concrete standard étale algebra R[X,Y]/(f, Y f' - 1). Its universal root gives the required root in the colimit.

The resulting Henselian property is proved, not added as a field of a putative strict henselization. Identification of its residue field and comparison with the inertia group in the manuscript still require separate arguments.

Imports11

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.Derivative
Mathlib.Algebra.Polynomial.Eval.Coeff
Mathlib.Algebra.Polynomial.Monic
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.RingTheory.Etale.StandardEtale
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.RingHom.Etale

Imported by11

theorem

geometricStalk_monic_exists_representative

L47 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_monic_exists_representative

Documentation

A monic polynomial over the geometric stalk comes from a monic polynomial over the sections of one actual pointed étale neighborhood.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalk_monic_exists_representative
    (p : (geometricStalk s)[X]) (hp : p.Monic) :
    ∃ (W : S.Etale) (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W)
      (q : Γ(W.left, ⊤)[X]), q.Monic ∧ q.map (geometricStalkGerm s W t).hom = p

theorem

geometricStalk_lift_simpleRoot

L67 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_lift_simpleRoot

Documentation

A simple root at the geometric point lifts by the actual standard étale neighborhood obtained by adjoining a root and inverting its derivative.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalk_lift_simpleRoot (W : S.Etale)
    (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W)
    (q : Γ(W.left, ⊤)[X]) (hq : q.Monic) (α : Ω)
    (hroot : (q.map (t.left.appTop ≫
      (Scheme.ΓSpecIso (CommRingCat.of Ω)).hom).hom).eval α = 0)
    (hderivative : (q.derivative.map (t.left.appTop ≫
      (Scheme.ΓSpecIso (CommRingCat.of Ω)).hom).hom).eval α ≠ 0) :
    ∃ a : geometricStalk s,
      (q.map (geometricStalkGerm s W t).hom).IsRoot a ∧
      geometricStalkEvaluation s a = α

theorem

geometricStalk_exists_root_of_evaluation_simpleRoot

L168 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_root_of_evaluation_simpleRoot

Documentation

A simple root in the geometric field of a monic polynomial over the stalk is the value of an actual root in the stalk.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalk_exists_root_of_evaluation_simpleRoot
    (p : (geometricStalk s)[X]) (hp : p.Monic) (α : Ω)
    (hroot : (p.map (geometricStalkEvaluation s).hom).eval α = 0)
    (hderivative : (p.derivative.map (geometricStalkEvaluation s).hom).eval α ≠ 0) :
    ∃ a : geometricStalk s, p.IsRoot a ∧ geometricStalkEvaluation s a = α

theorem

geometricStalk_mem_maximalIdeal_iff

L194 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_mem_maximalIdeal_iff

Documentation

The maximal ideal of the constructed stalk is exactly the kernel of its evaluation at the geometric point.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalk_mem_maximalIdeal_iff (a : geometricStalk s) :
    a ∈ IsLocalRing.maximalIdeal (geometricStalk s) ↔
      geometricStalkEvaluation s a = 0

instance

geometricStalk_henselianLocalRing

L203 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_henselianLocalRing

Documentation

The étale stalk constructed from genuine pointed neighborhoods is Henselian. The root is supplied by a concrete standard étale polynomial algebra.

Source context 5 commands

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

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

Lean source · full declaration

instance geometricStalk_henselianLocalRing : HenselianLocalRing (geometricStalk s) where
  is_henselian p hp a₀ hroot hderivative := by
    have hroot' : (p.map (geometricStalkEvaluation s).hom).eval
        (geometricStalkEvaluation s a₀) = 0 := by
      rw [eval_map_apply]
      exact (geometricStalk_mem_maximalIdeal_iff s (p.eval a₀)).mp hroot
    have hderivative' : (p.derivative.map (geometricStalkEvaluation s).hom).eval
        (geometricStalkEvaluation s a₀) ≠ 0 := by
      rw [eval_map_apply]
      exact (geometricStalk_isUnit_iff s (p.derivative.eval a₀)).mp hderivative
    obtain ⟨a, ha, heval⟩ := geometricStalk_exists_root_of_evaluation_simpleRoot s p hp
      (geometricStalkEvaluation s a₀) hroot' hderivative'
    refine ⟨a, ha, ?_⟩
    rw [geometricStalk_mem_maximalIdeal_iff, map_sub, heval, sub_self]

Module documentation

Henselianity of the constructed geometric étale stalk

Declarations

geometricStalk_monic_exists_representative

geometricStalk_lift_simpleRoot

geometricStalk_exists_root_of_evaluation_simpleRoot

geometricStalk_mem_maximalIdeal_iff

geometricStalk_henselianLocalRing