theorem · Research papers

The étale fundamental group of Spec Z

Every geometric base point gives the trivial étale fundamental group of the integers.

In number-field terms, every nontrivial finite extension of $\mathbb Q$ ramifies at some finite prime. This rigidity gives a base case for arguments over the integers: extending a covering across all possible boundary can force it to be trivial. The classical proof uses Minkowski's discriminant theorem; Yamaguchi records it as Example 1.4(1), with SGA 1 providing the language of finite étale covers and fundamental groups.

YamaguchiPapersFormalization on GitHub ↗

Mathematical statement

For a separably closed field $\Omega$ and any geometric point $\xi:\operatorname{Spec}\Omega\to\operatorname{Spec}\mathbb Z$,

$$\pi_1^{\mathrm{\acute et}}(\operatorname{Spec}\mathbb Z,\xi)=1.$$

The Lean conclusion is that the automorphism group of the geometric fiber functor is a subsingleton.

Lean code

`Yamaguchi26SolvableCoverings.fundamental_group_integers_1_4`

Published library source ↗Same source in NYLL ↗

theorem fundamental_group_integers_1_4
    (Ω : Type) [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ℤ)) :
    Subsingleton π₁ᵉᵗ(ξ)

In-scope Lean context

noncomputable section

open AlgebraicGeometry CategoryTheory

open AlgebraicGeometry.FiniteEtale

namespace Yamaguchi26SolvableCoverings

Full declaration and proof

/-- Example 1.4 (1)：任意の幾何点を基点として、
整数環のスペクトルの étale 基本群は自明である。 -/
theorem fundamental_group_integers_1_4
    (Ω : Type) [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ℤ)) :
    Subsingleton π₁ᵉᵗ(ξ) := by
  constructor
  intro a b
  apply Iso.ext
  apply PreGaloisCategory.natTrans_ext_of_isGalois (fiber ξ)
  intro Y _
  let _ : ConnectedSpace Y.left := connectedSpace_left_of_isConnected Y
  let _ : Subsingleton ((fiber ξ).obj Y) :=
    subsingleton_fiber_of_connected_over_integers Ω ξ Y
  ext x
  exact Subsingleton.elim _ _

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

Naganori Yamaguchi. Extension of solvable coverings across horizontal divisors over the integers. 2026. arXiv:2610.02948v1, submitted October 2, 2026.
Alexander Grothendieck et al.. Revêtements étales et groupe fondamental (SGA 1). Springer, Lecture Notes in Mathematics 224, 1971. Link to the updated edition with remarks by Michel Raynaud.

Published source: a1a5a03f.

← All selected results in Research papers