Nyll.AnabelianGeometry.GeometricFundamentalGroup.OpenCurveSlim

Module documentation

Slimness of actual hyperbolic open-curve fundamental groups

Arbitrary open subgroups, including nonnormal ones, are realized by actual connected finite étale covers. Their actual compactifications and boundary Riemann--Hurwitz prove hyperbolicity. The geometric H¹ argument then kills their centers, giving the existing full IsSlim predicate.

theorem

isSlim_fundamentalGroup_open_hyperbolic

L29 ↗

AnabelianGeometry.isSlim_fundamentalGroup_open_hyperbolic

Documentation

The actual fundamental group of a hyperbolic open curve is slim.

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_open_hyperbolic
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F]
    (M : CurveModel K F) {X : Scheme}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] [CompactSpace X]
    (j : X ⟶ M.C) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
    (hboundary : (M.openBoundaryPlaces j).Nonempty)
    (hhyperbolic : 0 <
      2 * (genusFF K F : ℤ) + (M.openBoundaryPlaces_finite j).toFinset.card - 2)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X) :
    IsSlim (Aut (FiniteEtale.fiber geom))

Module documentation

Slimness of actual hyperbolic open-curve fundamental groups

Declarations

isSlim_fundamentalGroup_open_hyperbolic