Module

GenericKernelNormalGeneration.lean

Nyll.EtaleFundamentalGroups.Inertia.GenericKernelNormalGeneration

3 declarations indexed from sourceView source ↗

Module documentation

The generic-point kernel is normally generated by original inertia

The generators are the original ideal inertia groups of the literal normalization rings on all nonempty affine charts. The existing actual normalization-chart pullbacks and the finite Galois inertia image theorem identify exactly which finite Galois restrictions annihilate these groups. The actual generic-point kernel has precisely the same finite restrictions.

No Noetherian, finiteness-of-normalization, or kernel-comparison hypothesis is imposed.

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

Imports4

Imported by4

def

affineNormalizationInertiaGenerators

L37 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationInertiaGenerators

Documentation

The original normalization-inertia elements on all nonempty affine charts of an integral scheme, regarded in the same absolute Galois group.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def affineNormalizationInertiaGenerators (X : Scheme.{u}) [IsIntegral X] :
    Set Gal(SeparableClosure X.functionField/X.functionField)

theorem

affineNormalizationInertiaGenerators_subset_fixingSubgroup_iff_etale

L58 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationInertiaGenerators_subset_fixingSubgroup_iff_etale

Documentation

A finite Galois restriction kills every original normalization inertia exactly when its actual global normalization is etale.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem affineNormalizationInertiaGenerators_subset_fixingSubgroup_iff_etale
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (E : FiniteGaloisIntermediateField X.functionField
      (SeparableClosure X.functionField)) :
    affineNormalizationInertiaGenerators X ⊆
        (E.toIntermediateField.fixingSubgroup :
          Set Gal(SeparableClosure X.functionField/X.functionField)) ↔
      Etale (X.genericExtensionMorphism E).fromNormalization

theorem

genericAbsoluteGaloisHom_ker_eq_normalClosure_affineNormalizationInertia

L98 ↗

EtaleFundamentalGroups.Inertia.genericAbsoluteGaloisHom_ker_eq_normalClosure_affineNormalizationInertia

Documentation

On an arbitrary normal integral scheme, the literal generic-point kernel is the smallest closed normal subgroup containing every original normalization inertia group on every affine chart.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

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

Module documentation

The generic-point kernel is normally generated by original inertia

Declarations

affineNormalizationInertiaGenerators

affineNormalizationInertiaGenerators_subset_fixingSubgroup_iff_etale

genericAbsoluteGaloisHom_ker_eq_normalClosure_affineNormalizationInertia