Module

ArithmeticComposite.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticComposite

3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Composite

The fundamental group of a separably closed field at any geometric point is trivial.

Imports2

Imported by7

theorem

subsingleton_fundamentalGroup_of_isSepClosed

L21 ↗

AlgebraicGeometry.FiniteEtale.subsingleton_fundamentalGroup_of_isSepClosed

Documentation

The fundamental group of a separably closed field at any geometric point is trivial.

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 subsingleton_fundamentalGroup_of_isSepClosed
    (L : Type u) [Field L] [IsSepClosed L]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (eta : Spec (.of Ω) ⟶ Spec (.of L)) :
    Subsingleton π₁ᵉᵗ(eta)

theorem

fundamentalGroupHom_constantField_comp_eq_one

L32 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_constantField_comp_eq_one

Documentation

The geometric and arithmetic maps for a separably closed constant field have trivial composite.

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 fundamentalGroupHom_constantField_comp_eq_one
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosed L]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    (fundamentalGroupHom f (xi ≫ Limits.pullback.snd _ f)).comp
      (fundamentalGroupHom (Limits.pullback.snd _ f) xi) = 1

theorem

arithmeticFundamentalGroupHom_constantField_comp_eq_one

L63 ↗

AlgebraicGeometry.FiniteEtale.arithmeticFundamentalGroupHom_constantField_comp_eq_one

Documentation

The same trivial composite after identifying the field fundamental group with an absolute Galois group.

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_constantField_comp_eq_one
    (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))
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    (arithmeticFundamentalGroupHom k K f (xi ≫ Limits.pullback.snd _ f)).comp
      (fundamentalGroupHom (Limits.pullback.snd _ f) xi) = 1

Module documentation

Arithmetic Composite

Declarations

subsingleton_fundamentalGroup_of_isSepClosed

fundamentalGroupHom_constantField_comp_eq_one

arithmeticFundamentalGroupHom_constantField_comp_eq_one