Module

GeometricStalkStructure.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure

5 declarations indexed from sourceView source ↗

Module documentation

The actual structure map into the geometric étale stalk

For a geometric point of Spec R given by a ring map φ : R →+* Ω, use the identity étale neighborhood of Spec R. Its germ map, composed with the canonical identification of the sections of Spec R with R, constructs the structure homomorphism into the geometric stalk. Evaluation composed with this structure homomorphism is exactly φ.

If φ is local, so is the constructed structure homomorphism. In particular this applies when R is local and φ is its residue map followed by an embedding of its residue field into the chosen separably closed field. Neither flatness of this structure map nor a comparison with a separately chosen strict henselization is assumed here.

Imports3

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidue
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by18

def

geometricStalkStructureMap

L41 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap

Documentation

The structure map is the actual germ map of the identity étale neighborhood, precomposed with the sections--ring identification for Spec R.

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 {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkStructureMap :
    R →+* geometricStalk (Spec.map (CommRingCat.ofHom φ))

theorem

geometricStalkStructureMap_evaluation

L49 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_evaluation

Documentation

The structure map has the specified value at 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 {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkStructureMap_evaluation :
    (geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ))).hom.comp
      (geometricStalkStructureMap φ) = φ

theorem

geometricStalkStructureMap_evaluation_apply

L82 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_evaluation_apply

Documentation

Pointwise form of the compatibility with 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 {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkStructureMap_evaluation_apply (r : R) :
    geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ))
      (geometricStalkStructureMap φ r) = φ r

theorem

geometricStalkGerm_comp_structure

L89 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_comp_structure

Documentation

The structure map factors through the sections of every actual pointed étale neighborhood, compatibly with its 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 {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkGerm_comp_structure
    (W : (Spec (CommRingCat.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom φ))).fiber.obj W) :
    (geometricStalkGerm (Spec.map (CommRingCat.ofHom φ)) W t).hom.comp
      (((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ W.hom.appTop).hom) =
      geometricStalkStructureMap φ

instance

geometricStalkStructureMap_isLocalHom

L116 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_isLocalHom

Documentation

A closed geometric point of a local ring gives a local structure map into the constructed geometric stalk.

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 {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · full declaration

instance geometricStalkStructureMap_isLocalHom [IsLocalHom φ] :
    IsLocalHom (geometricStalkStructureMap φ) where
  map_nonunit r hr := by
    have hunit := hr.map (geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ))).hom
    rw [geometricStalkStructureMap_evaluation_apply] at hunit
    exact (inferInstance : IsLocalHom φ).map_nonunit r hunit

Module documentation

The actual structure map into the geometric étale stalk

Declarations

geometricStalkStructureMap

geometricStalkStructureMap_evaluation

geometricStalkStructureMap_evaluation_apply

geometricStalkGerm_comp_structure

geometricStalkStructureMap_isLocalHom