Module

AffineLineFundamentalGroup.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.AffineLineFundamentalGroup

3 declarations indexed from sourceView source ↗

Module documentation

The etale fundamental group of the affine line in characteristic zero

A connected finite etale cover of Spec K[T] is affine and integral. Its actual section algebra is a finite etale domain over K[T], hence trivial by the normalization and Riemann--Hurwitz argument. The original scheme morphism is therefore an isomorphism. The actual geometric fibre functor and Galois reconstruction then give triviality of the etale fundamental group.

Imports7

Nyll.AnabelianGeometry.GeometricFundamentalGroup.AffineLineEtaleAlgebra
Nyll.SchemeTheory.LocalGeometry.ConnectedDomainStalks
Nyll.SchemeTheory.LocalGeometry.SmoothStalkNormality
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Mathlib.CategoryTheory.Galois.Prorepresentability
Mathlib.AlgebraicGeometry.Noetherian

Imported by3

theorem

isIso_of_connected_finite_etale_affineLine

L37 ↗

AnabelianGeometry.GeometricFundamentalGroup.isIso_of_connected_finite_etale_affineLine

Documentation

Every connected finite etale cover of the affine line over an algebraically closed characteristic-zero field is an isomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem isIso_of_connected_finite_etale_affineLine
    {K : Type u} [Field K] [IsAlgClosed K] [CharZero K]
    {Y : Scheme.{u}} [ConnectedSpace Y]
    (π : Y ⟶ Spec (CommRingCat.of K[X])) [IsFinite π] [Etale π] : IsIso π

theorem

subsingleton_fiber_of_connected_affineLine

L84 ↗

AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fiber_of_connected_affineLine

Documentation

The actual geometric fibre of a connected finite etale affine-line cover is a singleton in characteristic zero.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem subsingleton_fiber_of_connected_affineLine
    {K : Type u} [Field K] [IsAlgClosed K] [CharZero K]
    {Ω : Type u} [Field Ω] (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K[X]))
    (Y : FiniteEtale (Spec (CommRingCat.of K[X]))) [ConnectedSpace Y.left] :
    Subsingleton ((fiber ξ).obj Y)

theorem

subsingleton_fundamentalGroup_affineLine

L103 ↗

AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fundamentalGroup_affineLine

Documentation

The actual etale fundamental group of the affine line over an algebraically closed characteristic-zero field is trivial at every separably closed geometric point.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem subsingleton_fundamentalGroup_affineLine
    {K : Type u} [Field K] [IsAlgClosed K] [CharZero K]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K[X])) :
    Subsingleton π₁ᵉᵗ(ξ)

Module documentation

The etale fundamental group of the affine line in characteristic zero

Declarations

isIso_of_connected_finite_etale_affineLine

subsingleton_fiber_of_connected_affineLine

subsingleton_fundamentalGroup_affineLine