Module

HenselianResidueFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.HenselianResidueFundamentalGroup

5 declarations indexed from sourceView source ↗

Module documentation

The actual closed-point fundamental group of a henselian local ring

The existing henselian finite étale equivalence and the canonical extension of a separably closed geometric-point field identify the residue Galois group with the fundamental group at the actual closed geometric point. An explicit residue-field isomorphism permits the original residue field to be retained.

Imports4

Imported by2

theorem

henselianResiduePullback_isEquivalence

L32 ↗

AlgebraicGeometry.FiniteEtale.henselianResiduePullback_isEquivalence

Documentation

Henselian reduction is an equivalence for the native finite étale category.

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 : Type u) [CommRing H] [HenselianLocalRing H]

Lean source · statement

theorem henselianResiduePullback_isEquivalence :
    (pullback (Spec.map (CommRingCat.ofHom (IsLocalRing.residue H)))).IsEquivalence

def

henselianClosedPoint

L50 ↗

AlgebraicGeometry.FiniteEtale.henselianClosedPoint

Documentation

The original closed-point inclusion expressed through its actual residue isomorphism.

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 : Type u) [CommRing H] [HenselianLocalRing H]
variable (k : Type u) [Field k] (e : IsLocalRing.ResidueField H ≃+* k)

Lean source · statement

def henselianClosedPoint : Spec (.of k) ⟶ Spec (.of H)

theorem

henselianClosedPoint_pullback_isEquivalence

L55 ↗

AlgebraicGeometry.FiniteEtale.henselianClosedPoint_pullback_isEquivalence

Documentation

The actual residue isomorphism preserves the henselian pullback equivalence.

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 : Type u) [CommRing H] [HenselianLocalRing H]
variable (k : Type u) [Field k] (e : IsLocalRing.ResidueField H ≃+* k)

Lean source · statement

theorem henselianClosedPoint_pullback_isEquivalence :
    (pullback (henselianClosedPoint H k e)).IsEquivalence

def

henselianResidueGaloisEquivFundamentalGroup

L90 ↗

AlgebraicGeometry.FiniteEtale.henselianResidueGaloisEquivFundamentalGroup

Documentation

The residue Galois group is the fundamental group at the actual extended closed geometric point, using the prescribed residue isomorphism.

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 : Type u) [CommRing H] [HenselianLocalRing H]
variable (k : Type u) [Field k] (e : IsLocalRing.ResidueField H ≃+* k)
variable (C Ω : Type u) [Field C] [Field Ω]
  [Algebra k C] [IsSepClosure k C] [Algebra C Ω] [Algebra k Ω]
  [IsScalarTower k C Ω] [IsSepClosed Ω]

Lean source · statement

def henselianResidueGaloisEquivFundamentalGroup :
    Gal(C/k) ≃ₜ* π₁ᵉᵗ(ξ k Ω ≫ henselianClosedPoint H k e)

theorem

henselianResidueGaloisEquivFundamentalGroup_point

L108 ↗

AlgebraicGeometry.FiniteEtale.henselianResidueGaloisEquivFundamentalGroup_point

Documentation

The closed-point Galois comparison has the literal compatible field action. The computation is retained at abstract ring and field structures.

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 : Type u) [CommRing H] [HenselianLocalRing H]
variable (k : Type u) [Field k] (e : IsLocalRing.ResidueField H ≃+* k)
variable (C Ω : Type u) [Field C] [Field Ω]
  [Algebra k C] [IsSepClosure k C] [Algebra C Ω] [Algebra k Ω]
  [IsScalarTower k C Ω] [IsSepClosed Ω]

Lean source · statement

theorem henselianResidueGaloisEquivFundamentalGroup_point
    (σ : Gal(C/k)) (ρ : Ω →+* Ω)
    (hρ : ρ.comp (algebraMap C Ω) = (algebraMap C Ω).comp σ.toRingHom)
    (X : FiniteEtale (Spec (.of H)))
    (x : (fiber (ξ k Ω ≫ henselianClosedPoint H k e)).obj X) :
    (fiberObjEquivHom (ξ k Ω ≫ henselianClosedPoint H k e) X
      ((henselianResidueGaloisEquivFundamentalGroup H k e C Ω σ).hom.app X x)).left =
      Spec.map (CommRingCat.ofHom ρ) ≫
        (fiberObjEquivHom (ξ k Ω ≫ henselianClosedPoint H k e) X x).left

Module documentation

The actual closed-point fundamental group of a henselian local ring

Declarations

henselianResiduePullback_isEquivalence

henselianClosedPoint

henselianClosedPoint_pullback_isEquivalence

henselianResidueGaloisEquivFundamentalGroup

henselianResidueGaloisEquivFundamentalGroup_point