NYLL
Module

ArithmeticMap.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticMap
2 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Map

Identifying the field fundamental group with its absolute Galois group preserves the kernel of the arithmetic map.

Imports2
Imported by4

Declarations

theorem

arithmeticFundamentalGroupHom_ker

L23 ↗
AlgebraicGeometry.FiniteEtale.arithmeticFundamentalGroupHom_ker
Documentation

Identifying the field fundamental group with its absolute Galois group preserves the kernel of the arithmetic map.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem arithmeticFundamentalGroupHom_ker
    (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) :
    (arithmeticFundamentalGroupHom k K f xi).toMonoidHom.ker =
      (fundamentalGroupHom f xi).toMonoidHom.ker
theorem

arithmeticFundamentalGroupHom_surjective_of_connected_constantField

L43 ↗
AlgebraicGeometry.FiniteEtale.arithmeticFundamentalGroupHom_surjective_of_connected_constantField
Documentation

The arithmetic map to an absolute Galois group is surjective when a separably closed constant extension is connected.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
theorem arithmeticFundamentalGroupHom_surjective_of_connected_constantField
    (k K L : Type u) [Field k] [Field K] [Field L]
    [Algebra k K] [IsSepClosure k K] [Algebra k L] [IsSepClosed L]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (arithmeticFundamentalGroupHom k K f xi)

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