Module

ArithmeticSurjective.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSurjective

3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Surjective

A geometrically connected scheme over a field induces a surjection on the fundamental group of that field.

Imports8

Imported by4

theorem

fundamentalGroupHom_surjective_of_geometricallyConnected

L34 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_geometricallyConnected

Documentation

A geometrically connected scheme over a field induces a surjection on the fundamental group of that field.

Source context 5 commands

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

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

Lean source · statement

theorem fundamentalGroupHom_surjective_of_geometricallyConnected
    {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [GeometricallyConnected f]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (fundamentalGroupHom f xi)

def

arithmeticFundamentalGroupHom

L70 ↗

AlgebraicGeometry.FiniteEtale.arithmeticFundamentalGroupHom

Documentation

The arithmetic map to the absolute Galois group of k, with the comparison of geometric points supplied by the fiber-functor comparison theorem.

Source context 5 commands

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

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

Lean source · statement

def arithmeticFundamentalGroupHom
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X) : π₁ᵉᵗ(xi) →ₜ* (K ≃ₐ[k] K)

theorem

arithmeticFundamentalGroupHom_surjective

L87 ↗

AlgebraicGeometry.FiniteEtale.arithmeticFundamentalGroupHom_surjective

Documentation

The arithmetic fundamental-group map of a geometrically connected scheme over k is surjective.

Source context 5 commands

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

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

Lean source · statement

theorem arithmeticFundamentalGroupHom_surjective
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [GeometricallyConnected f]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (arithmeticFundamentalGroupHom k K f xi)

Module documentation

Arithmetic Surjective

Declarations

fundamentalGroupHom_surjective_of_geometricallyConnected

arithmeticFundamentalGroupHom

arithmeticFundamentalGroupHom_surjective