Module

GeometricStalkHenselianMap.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselianMap

14 declarations indexed from sourceView source ↗

Module documentation

The actual pointed étale stalk maps to a Henselian target

Every pointed étale neighborhood lifts uniquely to the Henselian target, including non-affine neighborhoods. Their actual section maps form a cocone, so the defining presheaf-fiber colimit constructs the ring homomorphism. Its residue is the original evaluation and it extends the given base map. No comparison morphism or alternate colimit is assumed.

Imports8

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidue
Nyll.SchemeTheory.Etale.HenselianLocalSection
Nyll.SchemeTheory.Affine.SpecSectionMap
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by11

theorem

existsUnique_pointedHenselianLift

L38 ↗

EtaleFundamentalGroups.StrictHenselian.existsUnique_pointedHenselianLift

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem existsUnique_pointedHenselianLift
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    ∃! l : Spec (.of S) ⟶ W.left,
      l ≫ W.hom = Spec.map (CommRingCat.ofHom f) ∧
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue S)) ≫ l = t.left

def

geometricNeighborhoodHenselianLift

L51 ↗

EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodHenselianLift

Documentation

The actual lift of a pointed étale neighborhood into the Henselian target.

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

def geometricNeighborhoodHenselianLift
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    Spec (.of S) ⟶ W.left

theorem

geometricNeighborhoodHenselianLift_comp

L58 ↗

EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodHenselianLift_comp

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricNeighborhoodHenselianLift_comp
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    geometricNeighborhoodHenselianLift f W t ≫ W.hom =
      Spec.map (CommRingCat.ofHom f)

theorem

geometricNeighborhoodHenselianLift_residue

L66 ↗

EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodHenselianLift_residue

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricNeighborhoodHenselianLift_residue
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    Spec.map (CommRingCat.ofHom (IsLocalRing.residue S)) ≫
        geometricNeighborhoodHenselianLift f W t = t.left

theorem

geometricNeighborhoodHenselianLift_naturality

L74 ↗

EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodHenselianLift_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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricNeighborhoodHenselianLift_naturality
    {W V : (Spec (.of R)).Etale} (g : W ⟶ V)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    geometricNeighborhoodHenselianLift f W t ≫ g.left =
      geometricNeighborhoodHenselianLift f V
        ((Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
          ((IsLocalRing.residue S).comp f)))).fiber.map g t)

def

henselianNeighborhoodSectionMap

L100 ↗

EtaleFundamentalGroups.StrictHenselian.henselianNeighborhoodSectionMap

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

def henselianNeighborhoodSectionMap
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    Γ(W.left, ⊤) ⟶ CommRingCat.of S

theorem

henselianNeighborhoodSectionMap_naturality

L108 ↗

EtaleFundamentalGroups.StrictHenselian.henselianNeighborhoodSectionMap_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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem henselianNeighborhoodSectionMap_naturality
    ⦃W V : (Spec (.of R)).Etale⦄ (g : W ⟶ V)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    g.left.appTop ≫ henselianNeighborhoodSectionMap f W t =
      henselianNeighborhoodSectionMap f V
        ((Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
          ((IsLocalRing.residue S).comp f)))).fiber.map g t)

def

geometricStalkToHenselianCat

L126 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselianCat

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

def geometricStalkToHenselianCat :
    geometricStalk (Spec.map (CommRingCat.ofHom ((IsLocalRing.residue S).comp f))) ⟶
      CommRingCat.of S

def

geometricStalkToHenselian

L136 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian

Documentation

The map out of the actual geometric-stalk colimit into the prescribed Henselian target, constructed from its genuine pointed lifts.

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

def geometricStalkToHenselian :
    geometricStalk (Spec.map (CommRingCat.ofHom ((IsLocalRing.residue S).comp f))) →+* S

theorem

geometricStalkGerm_toHenselian

L141 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_toHenselian

Documentation

The colimit map has the literal section-map value on every 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 {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricStalkGerm_toHenselian
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    geometricStalkGerm (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))) W t ≫
        CommRingCat.ofHom (geometricStalkToHenselian f) =
      (geometricNeighborhoodHenselianLift f W t).appTop ≫
        (Scheme.ΓSpecIso (CommRingCat.of S)).hom

theorem

geometricStalkGerm_toSpecLiftSectionMap

L162 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_toSpecLiftSectionMap

Documentation

The actual colimit germ equation through the generic section-map API. The defining naturality proof stays with its original owner.

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricStalkGerm_toSpecLiftSectionMap
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointEtaleNeighborhoods (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    geometricStalkGerm (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))) W t ≫
        CommRingCat.ofHom (geometricStalkToHenselian f) =
      specLiftSectionMap (geometricNeighborhoodHenselianLift f W t)

theorem

geometricStalkToHenselian_comp_structure

L181 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_comp_structure

Documentation

The constructed map extends exactly the prescribed base-ring 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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricStalkToHenselian_comp_structure :
    (geometricStalkToHenselian f).comp
      (geometricStalkStructureMap ((IsLocalRing.residue S).comp f)) = f

theorem

geometricStalkToHenselian_residue

L206 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_residue

Documentation

Reduction of the constructed map is exactly the defining evaluation.

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

theorem geometricStalkToHenselian_residue :
    (IsLocalRing.residue S).comp (geometricStalkToHenselian f) =
      (geometricStalkEvaluation (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f)))).hom

instance

geometricStalkToHenselian_isLocalHom

L256 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_isLocalHom

Documentation

The constructed map is local, as its reduction is the actual evaluation.

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 S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  (f : R →+* S)

Lean source · statement

instance geometricStalkToHenselian_isLocalHom :
    IsLocalHom (geometricStalkToHenselian f)

Module documentation

The actual pointed étale stalk maps to a Henselian target

Declarations