Vanishing of derived étale H¹ of the multiplicative group over a field

Mathematical statement

Let $K$ be a field of characteristic zero. For the multiplicative group sheaf on the small étale site of $\operatorname{Spec}K$, the theorem proves $$H^1_{\mathrm{et}}(\operatorname{Spec}K,\mathbf G_m)=0.$$ Here $H^1$ denotes derived sheaf cohomology.

The current Lean theorem assumes characteristic zero; the classical vanishing statement holds over every field.

Lean code

`EtaleCohomology.etaleMultiplicativeGroup_H1_eq_zero_of_field`

Published library source ↗Same source in NYLL ↗

theorem etaleMultiplicativeGroup_H1_eq_zero_of_field
    (K : Type u) [Field K] [CharZero K]
    (a : Sheaf.H.{u} (etaleMultiplicativeGroupSheaf (Spec (.of K))) 1) : a = 0

In-scope Lean context

noncomputable section

universe u

open AlgebraicGeometry CategoryTheory Limits Opposite

open AlgebraicGeometry.FiniteEtale

namespace EtaleCohomology

Full declaration and proof

/-- The actual derived etale H1 of Gm over a characteristic-zero field
vanishes. Its extension representative is split using the proved geometric
Galois descent and Hilbert 90, not an assumed comparison with Galois H1. -/
theorem etaleMultiplicativeGroup_H1_eq_zero_of_field
    (K : Type u) [Field K] [CharZero K]
    (a : Sheaf.H.{u} (etaleMultiplicativeGroupSheaf (Spec (.of K))) 1) : a = 0 := by
  let X : Scheme.{u} := Spec (.of K)
  obtain ⟨B, i, p, hz, hS, hclass⟩ :=
    EtaleFundamentalGroups.Cohomology.exists_h1_extension X
      (etaleMultiplicativeGroupSheaf X) a
  let T : X.Etale := Scheme.Etale.mk (𝟙 X)
  let hT : IsTerminal T := MorphismProperty.Over.mkIdTerminal
    (show MorphismProperty Scheme.{u} from @Etale) X
  let Z : Sheaf X.smallEtaleTopology AddCommGrpCat.{u} :=
    (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (AddCommGrpCat.of (ULift.{u} ℤ))
  let eT : (freeAbelianSheafYoneda X.smallEtaleTopology).obj T ≅ Z :=
    freeAbelianSheafYonedaTerminalIso X.smallEtaleTopology hT
  let one : Z.obj.obj (op T) :=
    freeAbelianSheafYonedaHomEquiv X.smallEtaleTopology T Z eT.hom
  obtain ⟨b, hb⟩ := exists_section_lift_of_units_kernel_of_field K i p hz hS one
  let d : (freeAbelianSheafYoneda X.smallEtaleTopology).obj T ⟶ B :=
    (freeAbelianSheafYonedaHomEquiv X.smallEtaleTopology T B).symm b
  have hd : d ≫ p = eT.hom := by
    apply (freeAbelianSheafYonedaHomEquiv X.smallEtaleTopology T Z).injective
    rw [freeAbelianSheafYonedaHomEquiv_postcomp]
    change p.hom.app (op T)
      (freeAbelianSheafYonedaHomEquiv X.smallEtaleTopology T B
        ((freeAbelianSheafYonedaHomEquiv X.smallEtaleTopology T B).symm b)) = one
    rw [Equiv.apply_symm_apply]
    exact hb
  have hsplit : (eT.inv ≫ d) ≫ p = 𝟙 Z := by
    rw [Category.assoc, hd, eT.inv_hom_id]
  rw [← hclass]
  exact (EtaleFundamentalGroups.Cohomology.extClass_eq_zero_iff_exists_section hS).mpr
    ⟨eT.inv ≫ d, hsplit⟩

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.24: Picard groups. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.