Module

ProperCurveSlim.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.ProperCurveSlim

1 declaration indexed from sourceView source ↗

Module documentation

Slimness of actual fundamental groups of proper hyperbolic curves

Every actual open subgroup is realized by an actual connected finite étale cover. Its smooth proper model remains hyperbolic by Riemann--Hurwitz. Geometric deck H¹ faithfulness proves its center trivial, and the existing open-subgroup criterion gives the full centralizer quantification of IsSlim.

Imports6

Imported by1

Nyll.AnabelianGeometry.GeometricFundamentalGroup.All

theorem

isSlim_fundamentalGroup_proper_hyperbolic

L33 ↗

AnabelianGeometry.isSlim_fundamentalGroup_proper_hyperbolic

Documentation

The actual étale fundamental group of a proper hyperbolic curve over an algebraically closed field of characteristic zero is slim, with the actual open-subgroup quantification of the library's IsSlim definition.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
open ProCGroups.FiniteStepSolvableQuotients
namespace AnabelianGeometry

Lean source · statement

theorem isSlim_fundamentalGroup_proper_hyperbolic
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F) (hg : 2 ≤ genusFF K F)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ M.C) :
    IsSlim (Aut (FiniteEtale.fiber geom))

Module documentation

Slimness of actual fundamental groups of proper hyperbolic curves

Declarations

isSlim_fundamentalGroup_proper_hyperbolic