The geometric–arithmetic exact sequence

Mathematical statement

Let $k$ be a field, $L$ a separable closure, and $X\to\operatorname{Spec}k$ a quasi-compact, quasi-separated scheme such that $X_L$ is connected. Choose a geometric point $\xi:\operatorname{Spec}\Omega\to X_L$, with $\Omega$ separably closed, and let $x$ be its image in $X$. Then $$1\longrightarrow\pi_1^{\mathrm{et}}(X_L,\xi)\longrightarrow\pi_1^{\mathrm{et}}(X,x)\longrightarrow\operatorname{Gal}(L/k)\longrightarrow1$$ is exact.

The maps are the continuous homomorphisms induced by pullback and the structure morphism. Exactness includes injectivity on the left, surjectivity on the right, and equality of the kernel with the image. No splitting is asserted.

Lean code

`AlgebraicGeometry.FiniteEtale.arithmetic_exactSequence_of_isSepClosure`

Published library source ↗Same source in NYLL ↗

theorem arithmetic_exactSequence_of_isSepClosure
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosure k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    let geometric := fundamentalGroupHom (Limits.pullback.snd _ f) xi
    let arithmetic := arithmeticFundamentalGroupHom k L f (xi ≫ Limits.pullback.snd _ f)
    Function.Injective geometric ∧ Function.Surjective arithmetic ∧
      arithmetic.toMonoidHom.ker = geometric.toMonoidHom.range := by
  let : IsSepClosed L := IsSepClosure.sep_closed k
  let : ConnectedSpace X := connectedSpace_of_connected_constantField k L f
  refine ⟨fundamentalGroupHom_injective_of_separable_constant_extension k L X f xi,
    arithmeticFundamentalGroupHom_surjective_of_connected_constantField k L L f
      (xi ≫ Limits.pullback.snd _ f), ?_⟩
  exact (arithmeticFundamentalGroupHom_ker k L f (xi ≫ Limits.pullback.snd _ f)).trans
    (fundamentalGroupHom_constantField_ker_eq_range k L f xi)

In-scope Lean context

noncomputable section

universe u

open CategoryTheory Limits

namespace AlgebraicGeometry.FiniteEtale

Full declaration and proof

/-- The arithmetic short exact sequence over a separable closure. Both maps
are the actual continuous maps on geometric fiber automorphism groups. -/
theorem arithmetic_exactSequence_of_isSepClosure
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosure k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    let geometric := fundamentalGroupHom (Limits.pullback.snd _ f) xi
    let arithmetic := arithmeticFundamentalGroupHom k L f (xi ≫ Limits.pullback.snd _ f)
    Function.Injective geometric ∧ Function.Surjective arithmetic ∧
      arithmetic.toMonoidHom.ker = geometric.toMonoidHom.range := by
  let : IsSepClosed L := IsSepClosure.sep_closed k
  let : ConnectedSpace X := connectedSpace_of_connected_constantField k L f
  refine ⟨fundamentalGroupHom_injective_of_separable_constant_extension k L X f xi,
    arithmeticFundamentalGroupHom_surjective_of_connected_constantField k L L f
      (xi ≫ Limits.pullback.snd _ f), ?_⟩
  exact (arithmeticFundamentalGroupHom_ker k L f (xi ≫ Limits.pullback.snd _ f)).trans
    (fundamentalGroupHom_constantField_ker_eq_range k L f xi)

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

A. Grothendieck (director), with two exposés by M. Raynaud. Revêtements étales et groupe fondamental (SGA 1). Séminaire de Géométrie Algébrique du Bois Marie 1960–61. Société Mathématique de France, Documents Mathématiques 3, xviii + 327, 2003. Revised and annotated edition of the seminar volume first published in 1971 as Lecture Notes in Mathematics 224.
The Stacks Project Authors. Lemma 58.14.3: Geometric and arithmetic fundamental groups. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.