Module

GenericKernelFiniteGalois.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericKernelFiniteGalois

1 declaration indexed from sourceView source ↗

Module documentation

The generic-point kernel as an intersection of unramified finite kernels

For an arbitrary normal integral scheme, the actual generic absolute Galois kernel is the intersection of the restriction kernels of its finite Galois subextensions with etale normalization. The classifier is the existing finite-etale generic-fiber equivalence, and no local criterion is assumed.

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

Imports2

Imported by2

theorem

genericAbsoluteGaloisHom_ker_eq_iInf_etale_finiteGalois

L29 ↗

EtaleFundamentalGroups.genericAbsoluteGaloisHom_ker_eq_iInf_etale_finiteGalois

Documentation

Finite Galois extensions with etale normalization determine the literal kernel of the canonical generic-point surjection.

Source context 3 commands

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

open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem genericAbsoluteGaloisHom_ker_eq_iInf_etale_finiteGalois
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X] :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker =
      ⨅ (E : FiniteGaloisIntermediateField X.functionField
        (SeparableClosure X.functionField))
        (_ : Etale (X.genericExtensionMorphism E).fromNormalization),
        E.toIntermediateField.fixingSubgroup

Module documentation

The generic-point kernel as an intersection of unramified finite kernels

Declarations

genericAbsoluteGaloisHom_ker_eq_iInf_etale_finiteGalois