Module

Theorem1Dot4FundamentalGroupIntegers.lean

Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot4FundamentalGroupIntegers

1 declaration indexed from sourceView source ↗

Module documentation

Example 1.4 (1): the fundamental group of the integers

The etale fundamental group of Spec ℤ is trivial for every geometric base point. The proof uses Minkowski's discriminant bound to show that every connected finite etale cover of Spec ℤ is trivial, then tests automorphisms on Galois objects.

Only the assertion about Spec ℤ is in scope. The projective-space and affine-space assertions in the same item, items (2) and (3), and Corollary 2.7 are not formalized.

Source: Yamaguchi, arXiv:2610.02948v1, Example 1.4(1).

Imports4

Nyll.EtaleFundamentalGroups.FiniteEtale.Integers
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Mathlib.CategoryTheory.Galois.Decomposition

Imported by1

Nyll.Yamaguchi26SolvableCoverings.All

theorem

fundamental_group_integers_1_4

L34 ↗

Yamaguchi26SolvableCoverings.fundamental_group_integers_1_4

Documentation

Example 1.4 (1)：任意の幾何点を基点として、整数環のスペクトルの étale 基本群は自明である。

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
namespace Yamaguchi26SolvableCoverings

Lean source · statement

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

Module documentation

Example 1.4 (1): the fundamental group of the integers

Declarations

fundamental_group_integers_1_4