Module

GeometricStalkChangeField.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkChangeField

8 declarations indexed from sourceView source ↗

Module documentation

Extending the field of a pointed étale colimit

Compose each actual field-valued neighborhood point with the given field embedding. The existing colimit descent constructs the map on stalks. Its evaluation and structure-map equations are proved on the original germ maps.

Imports5

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by2

def

pointedEtaleChangeField

L33 ↗

EtaleFundamentalGroups.StrictHenselian.pointedEtaleChangeField

Documentation

The same actual étale neighborhood pointed over the larger field.

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

def pointedEtaleChangeField (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom φ))).fiber.obj W) :
    (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom (ι.comp φ)))).fiber.obj W

theorem

pointedEtaleChangeField_naturality

L40 ↗

EtaleFundamentalGroups.StrictHenselian.pointedEtaleChangeField_naturality

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

theorem pointedEtaleChangeField_naturality
    {W V : (Spec (.of R)).Etale} (g : W ⟶ V)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom φ))).fiber.obj W) :
    (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom (ι.comp φ)))).fiber.map g
        (pointedEtaleChangeField φ ι W t) =
      pointedEtaleChangeField φ ι V
        ((Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom φ))).fiber.map g t)

def

geometricStalkChangeField

L52 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkChangeField

Documentation

Field extension induces the actual map between the existing pointed étale colimits; no second colimit construction is introduced.

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

def geometricStalkChangeField :
    geometricStalk (Spec.map (CommRingCat.ofHom φ)) ⟶
      geometricStalk (Spec.map (CommRingCat.ofHom (ι.comp φ)))

theorem

geometricStalkGerm_changeField

L66 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_changeField

Documentation

The induced map sends every germ to the germ with its extended 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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

theorem geometricStalkGerm_changeField (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom φ))).fiber.obj W) :
    geometricStalkGerm (Spec.map (CommRingCat.ofHom φ)) W t ≫
        geometricStalkChangeField φ ι =
      geometricStalkGerm (Spec.map (CommRingCat.ofHom (ι.comp φ))) W
        (pointedEtaleChangeField φ ι W t)

theorem

geometricStalkChangeField_evaluation

L76 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkChangeField_evaluation

Documentation

Evaluation of the colimit map is the prescribed field embedding.

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

theorem geometricStalkChangeField_evaluation :
    geometricStalkChangeField φ ι ≫
        geometricStalkEvaluation (Spec.map (CommRingCat.ofHom (ι.comp φ))) =
      geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ)) ≫
        CommRingCat.ofHom ι

theorem

geometricStalkChangeField_evaluation_apply

L98 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkChangeField_evaluation_apply

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

theorem geometricStalkChangeField_evaluation_apply
    (a : geometricStalk (Spec.map (CommRingCat.ofHom φ))) :
    geometricStalkEvaluation (Spec.map (CommRingCat.ofHom (ι.comp φ)))
        (geometricStalkChangeField φ ι a) =
      ι (geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ)) a)

theorem

geometricStalkChangeField_comp_structure

L106 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkChangeField_comp_structure

Documentation

The field-extension map preserves the original base-ring structure.

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · statement

theorem geometricStalkChangeField_comp_structure :
    (geometricStalkChangeField φ ι).hom.comp (geometricStalkStructureMap φ) =
      geometricStalkStructureMap (ι.comp φ)

instance

geometricStalkChangeField_isLocalHom

L136 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkChangeField_isLocalHom

Documentation

Extending the pointing field gives a local map of the constructed stalks.

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 Ω] [Field Ω']
  (φ : R →+* Ω) (ι : Ω →+* Ω')

Lean source · full declaration

instance geometricStalkChangeField_isLocalHom :
    IsLocalHom (geometricStalkChangeField φ ι).hom where
  map_nonunit a ha := by
    apply geometricStalk_isUnit_of_evaluation_ne_zero
      (Spec.map (CommRingCat.ofHom φ)) a
    intro hzero
    apply (ha.map (geometricStalkEvaluation
      (Spec.map (CommRingCat.ofHom (ι.comp φ)))).hom).ne_zero
    rw [geometricStalkChangeField_evaluation_apply, hzero, map_zero]

Module documentation

Extending the field of a pointed étale colimit

Declarations