Module

GeometricStalkLocalizedGerm.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkLocalizedGerm

6 declarations indexed from sourceView source ↗

Module documentation

Localized neighborhood rings mapping to the geometric étale stalk

On an actual pointed étale neighborhood, take the prime ideal given by the kernel of evaluation in the geometric field. Every section outside this ideal has an invertible germ. The universal property of localization therefore constructs a map from the actual local ring of sections at this prime to the geometric stalk. This map is local, as follows from the criterion for a fraction to be a unit in a localization at a prime.

This supplies the local-stage maps needed to transfer local algebra from affine étale neighborhoods. No local-stage map or comparison is postulated.

Imports4

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by8

def

geometricNeighborhoodPrime

EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodPrime

Documentation

The actual prime of the neighborhood's ring of sections selected by its given geometric point.

Source context 5 commands

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

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

Lean source · statement

def geometricNeighborhoodPrime : PrimeSpectrum Γ(W.left, ⊤)

theorem

geometricStalkGerm_isUnit_of_mem_primeCompl

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_isUnit_of_mem_primeCompl

Documentation

A denominator outside the selected prime has an invertible germ.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalkGerm_isUnit_of_mem_primeCompl
    (a : (geometricNeighborhoodPrime s W t).asIdeal.primeCompl) :
    IsUnit (geometricStalkGerm s W t a)

def

geometricStalkLocalizedGerm

EtaleFundamentalGroups.StrictHenselian.geometricStalkLocalizedGerm

Documentation

The actual local ring of sections at the chosen point maps to the geometric stalk by localization of the germ map.

Source context 5 commands

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

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

Lean source · statement

def geometricStalkLocalizedGerm :
    Localization.AtPrime (geometricNeighborhoodPrime s W t).asIdeal →+* geometricStalk s

theorem

geometricStalkLocalizedGerm_comp

EtaleFundamentalGroups.StrictHenselian.geometricStalkLocalizedGerm_comp

Documentation

The map from the local ring extends the original section germ map.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalkLocalizedGerm_comp :
    (geometricStalkLocalizedGerm s W t).comp
      (algebraMap Γ(W.left, ⊤)
        (Localization.AtPrime (geometricNeighborhoodPrime s W t).asIdeal)) =
      (geometricStalkGerm s W t).hom

theorem

geometricStalkLocalizedGerm_apply

EtaleFundamentalGroups.StrictHenselian.geometricStalkLocalizedGerm_apply

Documentation

On an ordinary section the localized germ is its original germ.

Source context 5 commands

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

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

Lean source · statement

theorem geometricStalkLocalizedGerm_apply (a : Γ(W.left, ⊤)) :
    geometricStalkLocalizedGerm s W t
      (algebraMap Γ(W.left, ⊤)
        (Localization.AtPrime (geometricNeighborhoodPrime s W t).asIdeal) a) =
      geometricStalkGerm s W t a

instance

geometricStalkLocalizedGerm_isLocalHom

EtaleFundamentalGroups.StrictHenselian.geometricStalkLocalizedGerm_isLocalHom

Documentation

The localized germ map is local: a fraction with unit germ has a numerator outside the prime selected by the geometric point.

Source context 5 commands

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

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

Lean source · full declaration

instance geometricStalkLocalizedGerm_isLocalHom :
    IsLocalHom (geometricStalkLocalizedGerm s W t) where
  map_nonunit z hz := by
    obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq
      (geometricNeighborhoodPrime s W t).asIdeal.primeCompl z
    rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul,
      geometricStalkLocalizedGerm_apply] at hz
    have haunit : IsUnit (geometricStalkGerm s W t a) := isUnit_of_mul_isUnit_left hz
    apply (IsLocalization.AtPrime.isUnit_mk'_iff
      (Localization.AtPrime (geometricNeighborhoodPrime s W t).asIdeal)
      (geometricNeighborhoodPrime s W t).asIdeal a b).mpr
    change (t.left.appTop ≫ (Scheme.ΓSpecIso (CommRingCat.of Ω)).hom).hom a ≠ 0
    intro ha
    apply (haunit.map (geometricStalkEvaluation s).hom).ne_zero
    exact (ConcreteCategory.congr_hom (geometricStalkGerm_evaluation s W t) a).trans ha