Module

HenselianSpecialization.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.HenselianSpecialization

9 declarations indexed from sourceView source ↗

Module documentation

The actual specialization comparison of geometric fibers

Finite étale points in the fraction field of a normal henselian local ring specialize bijectively to residue-field points. The canonical section correspondence turns this same specialization into a natural isomorphism of geometric fiber functors. Its pointwise action is compatible with the actual normal-local-ring and fraction-field automorphisms.

Imports4

Imported by3

instance

finiteSections

L35 ↗

AlgebraicGeometry.FiniteEtale.finiteSections

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]

Lean source · statement

instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤)

def

henselianSpecializationOverEquiv

L39 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationOverEquiv

Documentation

Specialization of actual over-points, through their canonical section maps.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X

Lean source · statement

def henselianSpecializationOverEquiv (X : FiniteEtale (Spec (.of H))) :
    (Over.mk (Spec.algebraMap H L) ⟶ X.toComma) ≃
      (Over.mk (Spec.algebraMap H (IsLocalRing.ResidueField R)) ⟶ X.toComma)

theorem

pointHomAlgEquiv_henselianSpecializationOverEquiv

L47 ↗

AlgebraicGeometry.FiniteEtale.pointHomAlgEquiv_henselianSpecializationOverEquiv

Documentation

The over-point comparison is exactly the previously constructed ring specialization.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X

Lean source · statement

theorem pointHomAlgEquiv_henselianSpecializationOverEquiv
    (X : FiniteEtale (Spec (.of H)))
    (x : Over.mk (Spec.algebraMap H L) ⟶ X.toComma) :
    pointHomAlgEquiv H (IsLocalRing.ResidueField R) X
        (henselianSpecializationOverEquiv H R L X x) =
      SchemeTheory.finiteEtalePointSpecialization H R L Γ(X.left, ⊤)
        (pointHomAlgEquiv H L X x)

theorem

henselianSpecializationOverEquiv_naturality

L57 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationOverEquiv_naturality

Documentation

Specialization is natural for the original finite étale-cover morphisms.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X

Lean source · statement

theorem henselianSpecializationOverEquiv_naturality
    {X Y : FiniteEtale (Spec (.of H))} (f : X ⟶ Y)
    (x : Over.mk (Spec.algebraMap H L) ⟶ X.toComma) :
    henselianSpecializationOverEquiv H R L Y (x ≫ f.hom) =
      henselianSpecializationOverEquiv H R L X x ≫ f.hom

theorem

henselianSpecializationOverEquiv_equivariant

L82 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationOverEquiv_equivariant

Documentation

The actual over-point specialization commutes with compatible automorphisms.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X

Lean source · statement

theorem henselianSpecializationOverEquiv_equivariant
    (τ : R ≃ₐ[H] R) (σ : L ≃ₐ[H] L)
    (hσ : ∀ r : R, σ (algebraMap R L r) = algebraMap R L (τ r))
    (X : FiniteEtale (Spec (.of H)))
    (x : Over.mk (Spec.algebraMap H L) ⟶ X.toComma) :
    henselianSpecializationOverEquiv H R L X (mapPointHom H L σ X x) =
      mapPointHom H (IsLocalRing.ResidueField R) (SchemeTheory.residueAlgEquiv H R τ) X
        (henselianSpecializationOverEquiv H R L X x)

def

henselianSpecializationFiberEquiv

L115 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationFiberEquiv

Documentation

The actual generic and residue fibers have the canonical specialization bijection.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X
variable [IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

def henselianSpecializationFiberEquiv (X : FiniteEtale (Spec (.of H))) :
    (fiber (Spec.algebraMap H L)).obj X ≃
      (fiber (Spec.algebraMap H (IsLocalRing.ResidueField R))).obj X

theorem

fiberObjEquivHom_henselianSpecializationFiberEquiv

L123 ↗

AlgebraicGeometry.FiniteEtale.fiberObjEquivHom_henselianSpecializationFiberEquiv

Documentation

The fiber comparison retains the actual over-point specialization.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X
variable [IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

theorem fiberObjEquivHom_henselianSpecializationFiberEquiv
    (X : FiniteEtale (Spec (.of H))) (x : (fiber (Spec.algebraMap H L)).obj X) :
    fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X
        (henselianSpecializationFiberEquiv H R L X x) =
      henselianSpecializationOverEquiv H R L X
        (fiberObjEquivHom (Spec.algebraMap H L) X x)

def

henselianSpecializationFiberIso

L132 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationFiberIso

Documentation

The canonical specialization identifies the two actual geometric fiber functors.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X
variable [IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

def henselianSpecializationFiberIso :
    fiber (Spec.algebraMap H L) ≅
      fiber (Spec.algebraMap H (IsLocalRing.ResidueField R))

def

henselianSpecializationFundamentalGroupEquiv

L152 ↗

AlgebraicGeometry.FiniteEtale.henselianSpecializationFundamentalGroupEquiv

Documentation

This base-point comparison on fundamental groups comes from actual specialization.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
local instance finiteSections (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤) := sections_moduleFinite H X
variable [IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

def henselianSpecializationFundamentalGroupEquiv :
    π₁ᵉᵗ(Spec.algebraMap H L) ≃ₜ*
      π₁ᵉᵗ(Spec.algebraMap H (IsLocalRing.ResidueField R))

Module documentation

The actual specialization comparison of geometric fibers

Declarations