Module

GenericKernelStrictNormalGeneration.lean

Nyll.EtaleFundamentalGroups.Inertia.GenericKernelStrictNormalGeneration

4 declarations indexed from sourceView source ↗

Module documentation

The generic-point kernel and actual strict-local fraction fields

Every normalization prime on an affine chart localizes to a maximal prime over its actual scheme point. Conversely every maximal prime over an actual scheme stalk contracts to a prime on each affine neighborhood, and localization recovers that same prime. Both directions preserve the literal original inertia subgroup. The proved strict-stalk fraction-field image theorem therefore identifies the closed normal generators with the actual generic-point kernel.

Reference: https://stacks.math.columbia.edu/tag/0BTD

Imports6

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

theorem

affineNormalizationInertiaGenerators_eq_stalk

L41 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationInertiaGenerators_eq_stalk

Documentation

The original affine-normalization inertia generators and the original actual-stalk inertia generators are the same subset of the absolute Galois group. Both directions use the literal contraction/extension of primes.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
attribute [local instance] normalizationInertiaImageAction

Lean source · statement

theorem affineNormalizationInertiaGenerators_eq_stalk
    (X : Scheme.{u}) [IsIntegral X] :
    affineNormalizationInertiaGenerators X = stalkNormalizationInertiaGenerators X

theorem

genericAbsoluteGaloisHom_ker_eq_normalClosure_geometricStalkFraction

L135 ↗

EtaleFundamentalGroups.Inertia.genericAbsoluteGaloisHom_ker_eq_normalClosure_geometricStalkFraction

Documentation

For every normal integral scheme, the actual generic absolute Galois kernel is normally generated by the automorphisms fixing the literal strict-henselization fraction fields at its points.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
attribute [local instance] normalizationInertiaImageAction

Lean source · statement

theorem genericAbsoluteGaloisHom_ker_eq_normalClosure_geometricStalkFraction
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X] :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker =
      (Subgroup.normalClosure (geometricStalkFractionInertiaGenerators X)).topologicalClosure

theorem

genericAbsoluteGaloisHom_ker_eq_normalClosure_chosenStrictGalois

L146 ↗

EtaleFundamentalGroups.Inertia.genericAbsoluteGaloisHom_ker_eq_normalClosure_chosenStrictGalois

Documentation

The original chosen-point formulation: for any selection of a strict residue point over each x, the actual generic-point kernel is the smallest closed normal subgroup containing every Gal(Ksep/K_x^sh).

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
attribute [local instance] normalizationInertiaImageAction

Lean source · full declaration

theorem genericAbsoluteGaloisHom_ker_eq_normalClosure_chosenStrictGalois
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (choice : ∀ x : X,
      let : Algebra (X.presheaf.stalk x) (SeparableClosure X.functionField) :=
        X.stalkExtensionAlgebra x (SeparableClosure X.functionField)
      MaximalSpectrum (integralClosure (X.presheaf.stalk x)
        (SeparableClosure X.functionField))) :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker =
      (Subgroup.normalClosure (chosenStrictGaloisGenerators X choice)).topologicalClosure := by
  rw [genericAbsoluteGaloisHom_ker_eq_normalClosure_affineNormalizationInertia,
    affineNormalizationInertiaGenerators_eq_stalk,
    normalClosure_stalkNormalizationInertia_eq_chosen X choice,
    chosenStalkNormalizationInertiaGenerators_eq_strictGalois]

theorem

genericAbsoluteGaloisHom_ker_eq_pointInertia_and_chosenStrictGalois

L165 ↗

EtaleFundamentalGroups.Inertia.genericAbsoluteGaloisHom_ker_eq_pointInertia_and_chosenStrictGalois

Documentation

The three subgroups of the original normal-generation theorem agree: the generic-point kernel, the closed normal subgroup generated by literal point-and-residue inertia, and the closed normal subgroup generated by Gal(Ksep/K_x^sh) for any chosen strict residue point over each x. This collects the two proved original comparisons in one public statement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
attribute [local instance] normalizationInertiaImageAction

Lean source · full declaration

theorem genericAbsoluteGaloisHom_ker_eq_pointInertia_and_chosenStrictGalois
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (choice : ∀ x : X,
      let : Algebra (X.presheaf.stalk x) (SeparableClosure X.functionField) :=
        X.stalkExtensionAlgebra x (SeparableClosure X.functionField)
      MaximalSpectrum (integralClosure (X.presheaf.stalk x)
        (SeparableClosure X.functionField))) :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker =
        (Subgroup.normalClosure (pointNormalizationInertiaGenerators X)).topologicalClosure ∧
      (genericAbsoluteGaloisHom X).toMonoidHom.ker =
        (Subgroup.normalClosure (chosenStrictGaloisGenerators X choice)).topologicalClosure :=
  ⟨genericAbsoluteGaloisHom_ker_eq_normalClosure_pointNormalizationInertia X,
    genericAbsoluteGaloisHom_ker_eq_normalClosure_chosenStrictGalois X choice⟩

Module documentation

The generic-point kernel and actual strict-local fraction fields

Declarations

affineNormalizationInertiaGenerators_eq_stalk

genericAbsoluteGaloisHom_ker_eq_normalClosure_geometricStalkFraction

genericAbsoluteGaloisHom_ker_eq_normalClosure_chosenStrictGalois

genericAbsoluteGaloisHom_ker_eq_pointInertia_and_chosenStrictGalois