theorem · Étale Fundamental Groups and Cohomology

The Kummer sequence on the small étale site

When a positive integer is invertible on the scheme, taking its power on the multiplicative group is locally surjective in the étale topology.

An étale-local root need not descend to a global root. The long exact sequence relates this obstruction to roots-of-unity torsors and torsion in the Picard group, connecting equations for roots with line bundles. Classical Kummer theory studies field extensions obtained by extracting roots; the sheaf sequence carries that viewpoint to schemes, as developed in the Stacks Project.

EtaleFundamentalGroupsAndCohomology on GitHub ↗

Mathematical statement

Let $X$ be a scheme and $n>0$ an integer whose image in $\Gamma(X,\mathcal O_X)$ is a unit. The sheaves on the small étale site form an exact sequence $$1\longrightarrow\mu_n\longrightarrow\mathbf G_m\xrightarrow{(\cdot)^n}\mathbf G_m\longrightarrow1.$$ Here $\mu_n$ is the kernel of the $n$th-power map.

More concretely, every unit $a\in\Gamma(X,\mathcal O_X)^\times$ admits a root after a finite étale surjective morphism $f:Y\to X$: there is $b\in\Gamma(Y,\mathcal O_Y)^\times$ with $b^n=f^*a$. The cover can be chosen to have degree $n$ at every point.

Lean code

`EtaleCohomology.etaleKummerComplex_shortExact`

Published library source ↗Same source in NYLL ↗

theorem etaleKummerComplex_shortExact (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) :
    (etaleKummerComplex X n).ShortExact

In-scope Lean context

noncomputable section

universe u

open AlgebraicGeometry CategoryTheory Limits Opposite

open CategoryTheory.Abelian

namespace EtaleCohomology

Full declaration and proof

/-- The actual Kummer sequence is short exact when n is invertible. -/
theorem etaleKummerComplex_shortExact (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) :
    (etaleKummerComplex X n).ShortExact := by
  have : Epi (etaleMultiplicativeGroupPower X n) :=
    etaleMultiplicativeGroupPower_epi X hn hnX
  unfold etaleKummerComplex
  exact { exact := ShortComplex.exact_kernel (etaleMultiplicativeGroupPower X n) }

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729).
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.28: Kummer theory. 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