Module

RationalFundamentalGroup.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalFundamentalGroup

2 declarations indexed from sourceView source ↗

Module documentation

The fundamental group of a proper rational curve

The actual etale fundamental group of a proper rational curve model over an algebraically closed field of characteristic zero is trivial at every geometric point. Connected finite etale covers are isomorphisms by the geometric argument. Their geometric fibres are therefore singletons. The proved reconstruction of fibre-functor endomorphisms from pointed Galois objects then forces every automorphism of the actual fibre functor to agree with every other one.

Imports4

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalConnectedEtale
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Mathlib.CategoryTheory.Galois.Prorepresentability

Imported by2

theorem

subsingleton_fiber_of_connected_rational

L32 ↗

AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fiber_of_connected_rational

Documentation

A connected finite etale cover of a proper rational curve has singleton geometric fibre in characteristic zero.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem subsingleton_fiber_of_connected_rational
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    (M : CurveModel K (RatFunc K)) {Ω : Type} [Field Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ M.C)
    (Y : FiniteEtale M.C) [ConnectedSpace Y.left] :
    Subsingleton ((fiber ξ).obj Y)

theorem

subsingleton_fundamentalGroup_rational

L52 ↗

AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fundamentalGroup_rational