NYLL
Module

GenericPointEssentialImage.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointEssentialImage
3 declarations indexed from sourceView source ↗

Module documentation

Generic fibers and the kernel of the generic absolute Galois map

The absolute Galois action on a generic fiber is restriction of the action of the fundamental group. A finite continuous absolute Galois action comes from a finite étale cover precisely when the generic kernel acts trivially.

Imports4
Imported by2

Declarations

def

genericPullbackContActionIso

L31 ↗
AlgebraicGeometry.FiniteEtale.genericPullbackContActionIso
Documentation

Generic pullback and the finite Galois-set equivalence identify the absolute Galois action with restriction along the generic Galois map.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
def genericPullbackContActionIso (X : Scheme.{u}) [IsIntegral X] :
    pullback (X.fromSpecStalk (genericPoint X)) ⋙
        (equivContAction X.functionField (SeparableClosure X.functionField)).functor ≅
      functorToContAction
          (fiber (X.genericExtensionMorphism (AlgebraicClosure X.functionField))) ⋙
        ContAction.res FintypeCat (genericAbsoluteGaloisHom X)
theorem

genericPullback_essImage_iff_ker_le_ker_ρAut

L55 ↗
AlgebraicGeometry.FiniteEtale.genericPullback_essImage_iff_ker_le_ker_ρAut
Documentation

A finite continuous absolute Galois action occurs as the generic fiber of a finite étale cover exactly when the generic Galois kernel acts trivially.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem genericPullback_essImage_iff_ker_le_ker_ρAut
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (Y : ContAction FintypeCat.{u}
      (SeparableClosure X.functionField ≃ₐ[X.functionField]
        SeparableClosure X.functionField)) :
    (pullback (X.fromSpecStalk (genericPoint X)) ⋙
      (equivContAction X.functionField (SeparableClosure X.functionField)).functor).essImage Y ↔
        (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤ (Action.ρAut Y.obj).ker
theorem

genericPullback_obj_essImage_iff_ker_le_ker_ρAut

L70 ↗
AlgebraicGeometry.FiniteEtale.genericPullback_obj_essImage_iff_ker_le_ker_ρAut
Documentation

A finite étale scheme over the function field extends to the base exactly when the generic kernel acts trivially on its finite Galois set.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem genericPullback_obj_essImage_iff_ker_le_ker_ρAut
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (W : FiniteEtale (Spec (.of X.functionField))) :
    (pullback (X.fromSpecStalk (genericPoint X))).essImage W ↔
      (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤
        (Action.ρAut
          (((equivContAction X.functionField (SeparableClosure X.functionField)).functor.obj
            W).obj)).ker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.