Module

GenericPointSurjective.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointSurjective

3 declarations indexed from sourceView source ↗

Module documentation

The generic absolute Galois map of a normal integral scheme

The geometric generic point determines a continuous map from the absolute Galois group of the function field to the étale fundamental group. For a normal integral scheme this map is surjective, because dominant preimmersions preserve connected finite étale covers.

Imports4

Imported by12

theorem

fundamentalGroupHom_surjective_of_isPreimmersion_of_isDominant

L32 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_isPreimmersion_of_isDominant

Documentation

A dominant quasi-compact preimmersion into a normal integral scheme induces a surjection on fundamental groups at each geometric point.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem fundamentalGroupHom_surjective_of_isPreimmersion_of_isDominant
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [ConnectedSpace U]
    (j : U ⟶ X) [IsPreimmersion j] [IsDominant j] [QuasiCompact j]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ U) :
    Function.Surjective (fundamentalGroupHom j xi)

def

genericAbsoluteGaloisHom

L53 ↗

AlgebraicGeometry.FiniteEtale.genericAbsoluteGaloisHom

Documentation

The canonical absolute Galois map at the geometric generic point. The field fundamental group is identified using the separable closure inside the algebraic closure.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

def genericAbsoluteGaloisHom (X : Scheme.{u}) [IsIntegral X] :
    (SeparableClosure X.functionField ≃ₐ[X.functionField]
      SeparableClosure X.functionField) →ₜ*
        π₁ᵉᵗ(X.genericExtensionMorphism (AlgebraicClosure X.functionField))

theorem

genericAbsoluteGaloisHom_surjective

L65 ↗

AlgebraicGeometry.FiniteEtale.genericAbsoluteGaloisHom_surjective

Documentation

The absolute Galois group of the function field surjects onto the fundamental group of a normal integral scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem genericAbsoluteGaloisHom_surjective
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X] :
    Function.Surjective (genericAbsoluteGaloisHom X)

Module documentation

The generic absolute Galois map of a normal integral scheme

Declarations

fundamentalGroupHom_surjective_of_isPreimmersion_of_isDominant

genericAbsoluteGaloisHom

genericAbsoluteGaloisHom_surjective