definition · Étale Fundamental Groups and Cohomology

Étale schemes over a field as continuous Galois sets

The geometric fiber over a separable closure gives an equivalence for all étale schemes over a field, including those with infinitely many components.

Finite Galois orbits correspond to finite separable extensions, while arbitrary disjoint unions account for schemes with infinitely many components. This makes the étale geometry of a point accessible through field Galois theory and provides the basic model for fundamental groups of schemes. Grothendieck's SGA 1 seminar of 1960–61 developed that passage from field extensions to finite covers of schemes.

EtaleFundamentalGroupsAndCohomology on GitHub ↗

Mathematical statement

Let $k$ be a field, let $K$ be a separable closure of $k$, and equip $G=\operatorname{Aut}_k(K)$ with its Krull topology. There is an equivalence $$\operatorname{Et}/k \simeq G\text{-}\mathbf{Set}_{\mathrm{disc,cont}}.$$ On the right are discrete sets with continuous $G$-action; on the left are schemes étale over $\operatorname{Spec}k$.

The forward functor takes the geometric fiber over $\operatorname{Spec}K$. No finiteness condition is imposed on the entire scheme or the entire Galois set. Continuity nevertheless forces every individual orbit to be finite.

Lean code

`AlgebraicGeometry.Scheme.Etale.equivDiscreteContAction`

Published library source ↗Same source in NYLL ↗

opaque equivDiscreteContAction :
    (Spec (.of k)).Etale ≌
      DiscreteContAction TopCat (K ≃ₐ[k] K)

In-scope Lean context

@[expose] public section

universe u

noncomputable section

open CategoryTheory Limits MorphismProperty PreGaloisCategory

open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete

namespace AlgebraicGeometry.Scheme.Etale

variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]

attribute [local instance] IsSepClosure.sep_closed

Full declaration and proof

/-- **Stacks Project, Tag 03QR.**  Étale schemes over a field are
equivalent to discrete continuous sets with an action of its absolute Galois
group.  The forward functor is the geometric fiber at `Spec K`. -/
@[stacks 03QR "The category of schemes étale over a field is equivalent to \
the category of discrete sets with continuous action by its absolute Galois group."]
noncomputable opaque equivDiscreteContAction :
    (Spec (.of k)).Etale ≌
      DiscreteContAction TopCat (K ≃ₐ[k] K) :=
  assembledEquivalence k K

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.2.2: Schemes étale over a point. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.

Published source: 470c51fc.

← All selected results in Étale Fundamental Groups and Cohomology