Module

GeometricStalkAlgebraColimit.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkAlgebraColimit

9 declarations indexed from sourceView source ↗

Module documentation

The actual geometric stalk as a filtered colimit of base algebras

The structure maps of the pointed étale neighborhoods commute with the actual geometric-stalk germ maps. Thus the defining ring colimit lifts to the category of algebras under the original ring. Restricting along the small filtered final model supplies a small filtered diagram whose colimit is the same actual stalk, with its actual structure homomorphism. This is the input for finite-data algebra descent, rather than an assumed presentation of strict henselization.

Imports4

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Filtered.FinallySmall
Mathlib.CategoryTheory.Limits.Final

Imported by6

def

geometricStalkRingDiagram

L35 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkRingDiagram

Documentation

The rings of all actual pointed étale neighborhoods of the chosen point.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkRingDiagram :
    (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.Elementsᵒᵖ ⥤
      CommRingCat.{u}

def

geometricStalkDiagramStructure

L43 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkDiagramStructure

Documentation

The base-ring maps on the actual pointed-neighborhood diagram.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · full declaration

def geometricStalkDiagramStructure :
    (Functor.const _).obj (CommRingCat.of R) ⟶ geometricStalkRingDiagram φ where
  app j := (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ j.unop.obj.hom.appTop
  naturality j k f := by
    change (𝟙 (CommRingCat.of R)) ≫
        ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ k.unop.obj.hom.appTop) =
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ j.unop.obj.hom.appTop) ≫
        f.unop.hom.left.appTop
    rw [Category.id_comp, Category.assoc, ← Scheme.Hom.comp_appTop]
    exact congrArg (fun g => (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ g.appTop)
      (MorphismProperty.Over.w f.unop.hom).symm

def

geometricStalkAlgebraDiagram

L57 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkAlgebraDiagram

Documentation

The defining pointed-neighborhood diagram, with its actual base-algebra structures retained.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkAlgebraDiagram :
    (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.Elementsᵒᵖ ⥤
      Under (CommRingCat.of R)

def

geometricStalkAlgebraCocone

L63 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkAlgebraCocone

Documentation

The actual germ cocone in base algebras.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkAlgebraCocone : Cocone (geometricStalkAlgebraDiagram φ)

def

geometricStalkAlgebraCoconeIsColimit

L73 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkAlgebraCoconeIsColimit

Documentation

The constructed germ cocone is colimiting as a diagram of base algebras.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkAlgebraCoconeIsColimit :
    IsColimit (geometricStalkAlgebraCocone φ)

abbrev

GeometricStalkAlgebraIndex

L81 ↗

EtaleFundamentalGroups.StrictHenselian.GeometricStalkAlgebraIndex

Documentation

A small filtered index category for the actual algebra presentation.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

abbrev GeometricStalkAlgebraIndex

def

geometricStalkSmallAlgebraDiagram

L86 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkSmallAlgebraDiagram

Documentation

A small filtered diagram of actual pointed-neighborhood algebras.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkSmallAlgebraDiagram :
    GeometricStalkAlgebraIndex φ ⥤ Under (CommRingCat.of R)

def

geometricStalkSmallAlgebraCocone

L91 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkSmallAlgebraCocone

Documentation

The small algebra cocone has the same actual geometric-stalk vertex.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkSmallAlgebraCocone : Cocone (geometricStalkSmallAlgebraDiagram φ)

def

geometricStalkSmallAlgebraCoconeIsColimit

L95 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkSmallAlgebraCoconeIsColimit

Documentation

The actual small filtered algebra cocone is colimiting.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)

Lean source · statement

def geometricStalkSmallAlgebraCoconeIsColimit :
    IsColimit (geometricStalkSmallAlgebraCocone φ)

Module documentation

The actual geometric stalk as a filtered colimit of base algebras

Declarations