definition · Étale Fundamental Groups and Cohomology

Finite étale schemes and finite locally constant sheaves

The sheaf of sections identifies finite étale schemes with finite locally constant sheaves of sets on the small étale site.

A finite cover can be viewed as a locally varying finite set whose gluing determines both the scheme and its morphisms. On a connected base with a geometric point, this also connects it to continuous finite fundamental-group actions. The correspondence is the algebraic analogue of the relation between covering spaces and locally constant sheaves in topology, expressed through étale representability.

EtaleFundamentalGroupsAndCohomology on GitHub ↗

Mathematical statement

For every scheme $X$, there is an equivalence $$\operatorname{FinEt}(X)\simeq\mathbf{Sh}_{\mathrm{flc}}(X_{\mathrm{et}},\mathbf{Set}).$$ The right-hand category is the full subcategory of sheaves that are étale locally isomorphic to constant sheaves associated with finite sets.

The forward functor sends $Y\to X$ to its sheaf of sections, $U\mapsto\operatorname{Hom}_X(U,Y)$. No connectedness, noetherianity, quasi-compactness, or assumption that $X$ lies over a field is included.

Lean code

`EtaleCohomology.finiteEtaleEquivFiniteLocallyConstantSetSheaf`

Published library source ↗Same source in NYLL ↗

def finiteEtaleEquivFiniteLocallyConstantSetSheaf (X : Scheme.{u}) :
    FiniteEtale X ≌ EtaleFiniteLocallyConstantSetSheaf X

In-scope Lean context

noncomputable section

open AlgebraicGeometry CategoryTheory

universe u

namespace EtaleCohomology

Full declaration and proof

/-- Finite étale schemes are equivalent to finite locally constant étale set sheaves. -/
def finiteEtaleEquivFiniteLocallyConstantSetSheaf (X : Scheme.{u}) :
    FiniteEtale X ≌ EtaleFiniteLocallyConstantSetSheaf X := by
  let F := finiteEtaleToFiniteLocallyConstantSetSheaf X
  let hF : F.FullyFaithful :=
    { preimage := fun f => (finiteEtaleSheafFullyFaithful X).preimage f.hom
      map_preimage := fun f => ObjectProperty.hom_ext _
        ((finiteEtaleSheafFullyFaithful X).map_preimage f.hom)
      preimage_map := fun f => (finiteEtaleSheafFullyFaithful X).preimage_map f }
  letI : F.IsEquivalence :=
    { faithful := hF.faithful
      full := hF.full
      essSurj := ⟨fun G => by
        obtain ⟨Z, ⟨e⟩⟩ := G.property.exists_finiteEtaleSheaf_iso
        exact ⟨Z, ⟨ObjectProperty.isoMk (IsEtaleFiniteLocallyConstantSet (X := X)) e⟩⟩⟩ }
  exact F.asEquivalence

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

The Stacks Project Authors. Section 59.64: Locally constant sheaves. 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