Slimness for punctured hyperbolic curves

Mathematical statement

Let $K$ be algebraically closed of characteristic $0$. Let $j:U\hookrightarrow C$ be an open immersion into a smooth proper curve model of genus $g$, with nonempty finite boundary of size $r$. In the public statement, $U$ is integral, normal, locally Noetherian and quasi-compact, and $j$ is quasi-compact and quasi-separated. If

$$2g+r-2>0,$$

then for every geometric point $\xi$ of $U$ and every open subgroup $H\le\pi_1^{\mathrm{\acute et}}(U,\xi)$,

$$C_{\pi_1^{\mathrm{\acute et}}(U,\xi)}(H)=\{1\}.$$

Lean code

`AnabelianGeometry.isSlim_fundamentalGroup_open_hyperbolic`

Published library source ↗Same source in NYLL ↗

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))

In-scope Lean context

noncomputable section

open CategoryTheory AlgebraicGeometry AlgebraicCurve

open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups

open ProCGroups.FiniteStepSolvableQuotients

namespace AnabelianGeometry

Full declaration and proof

/-- The actual fundamental group of a hyperbolic open curve is slim. -/
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)) := by
  apply isSlim_iff_openSubgroups_center_eq_bot.mpr
  intro H
  rw [Subgroup.eq_bot_iff_forall]
  intro z hz
  obtain ⟨A, hA, geomA, _, eA, _⟩ :=
    FiniteEtale.exists_connectedCover_lift_fundamentalGroup_equiv_openSubgroup geom H
  have : IsConnected A := FiniteEtale.isConnected_of_connectedSpace_left A
  have : IsIntegral A.left := isIntegral_left_of_isConnected_finiteEtale A
  have : IsNormalIntegral A.left := isNormalIntegral_left_of_isConnected_finiteEtale A
  have : IsLocallyNoetherian A.left := isLocallyNoetherian_left_finiteEtale A
  have : IsIntegral ((Functor.id Scheme).obj A.left) :=
    inferInstanceAs (IsIntegral A.left)
  have : IsIntegral ((Functor.fromPUnit X).obj A.right) :=
    inferInstanceAs (IsIntegral X)
  have : IsFiniteEtale A.hom := A.prop
  have : CompactSpace A.left :=
    QuasiCompact.compactSpace_of_compactSpace (X := A.left) (Y := X) A.hom
  have : Surjective A.hom := IsFiniteEtale.surjective A.hom
  let cA : A.left ⟶ Spec (.of K) := A.hom ≫ j ≫ M.toBase
  let : Algebra K A.left.functionField := (baseToFunctionField cA).toAlgebra
  obtain ⟨N, d, k, hk, hd, hfinite, hsquare, hb, hn⟩ :=
    exists_hyperbolic_open_cover_model M j A hhyperbolic
  have : IsOpenImmersion k := hk
  have : IsFinite d := hfinite
  have : IsProper N.toBase := N.isProper
  have : QuasiSeparatedSpace N.C :=
    quasiSeparatedSpace_of_quasiSeparated N.toBase
  have : QuasiCompact k := inferInstance
  have : QuasiSeparated k := inferInstance
  have hsurj : Function.Surjective d :=
    surjective_finite_extension_of_open_square j A.hom A.hom.surjective k d hsquare
  have hNboundary :=
    openBoundary_nonempty_of_finite_square M N d hd hsurj j k hb hboundary
  have he : eA.symm z = 1 :=
    Cohomology.fundamentalGroup_eq_one_of_finiteH1_deck_faithful geomA
      (fun B _ xi σ hσ =>
        open_deck_eq_one_of_all_finiteH1_trivial N k hNboundary hn B xi σ hσ)
      (eA.symm z) (by
        intro a
        have hcomm : z * eA a = eA a * z :=
          (Subgroup.mem_center_iff.mp hz (eA a)).symm
        have hmap := congrArg eA.symm hcomm
        change eA.symm z * a = a * eA.symm z
        simpa only [map_mul, eA.symm_apply_apply] using hmap)
  exact eA.symm.injective (he.trans (map_one eA.symm).symm)

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729).
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Alexander Grothendieck et al.. Revêtements étales et groupe fondamental (SGA 1). Springer, Lecture Notes in Mathematics 224, 1971. Link to the updated edition with remarks by Michel Raynaud.
Shinichi Mochizuki. The local pro-p anabelian geometry of curves. Inventiones mathematicae, 138, 319–423, 1999. Historical context for the arithmetic reconstruction problem; that reconstruction theorem is not claimed as formalized here.