Slimness for proper hyperbolic curves

Mathematical statement

Let $K$ be algebraically closed of characteristic $0$, let $C$ be a smooth proper curve model of a one-variable function field $F/K$, and assume $g(F/K)\ge2$. For a geometric point $\xi$, put $G=\pi_1^{\mathrm{\acute et}}(C,\xi)$. Then

$$\forall\,H\le G\text{ open},\qquad C_G(H)=\{1\}.$$

This is the library's predicate $\mathrm{IsSlim}(G)$. It quantifies over all open subgroups, including nonnormal ones.

Lean code

`AnabelianGeometry.isSlim_fundamentalGroup_proper_hyperbolic`

Published library source ↗Same source in NYLL ↗

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

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 é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. -/
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)) := 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 : Smooth M.toBase := SmoothOfRelativeDimension.smooth 1 M.toBase
  have : IsIntegrallyClosed Γ(Spec (.of K), ⊤) :=
    IsIntegrallyClosed.of_equiv (Scheme.ΓSpecIso (.of K)).symm.commRingCatIsoToRingEquiv
  have : IsNormalIntegral M.C := IsNormalIntegral.of_stalks M.C
    (fun x => (Smooth.isDomain_and_isIntegrallyClosed_stalk M.toBase x).2)
  have : IsIntegral A.left := isIntegral_left_of_isConnected_finiteEtale A
  let : Algebra K A.left.functionField :=
    (baseToFunctionField (show A.left ⟶ Spec (.of K) from A.hom ≫ M.toBase)).toAlgebra
  obtain ⟨hC, hFT, N, i, _, hgenus⟩ :=
    exists_curveModel_of_connected_finiteEtale M A
  let E : FiniteEtale N.C ≌ FiniteEtale A.left :=
    MorphismProperty.Over.pullbackIso
      (@IsFiniteEtale : MorphismProperty Scheme) ⊤ i
  have : (FiniteEtale.pullback i.inv).IsEquivalence := E.isEquivalence_functor
  let e : H ≃ₜ* Aut (FiniteEtale.fiber (geomA ≫ i.inv)) :=
    eA.symm.trans (FiniteEtale.fundamentalGroupEquivOfPullbackEquivalence i.inv geomA)
  have he : e z = 1 :=
    Cohomology.fundamentalGroup_eq_one_of_finiteH1_deck_faithful (geomA ≫ i.inv)
      (fun B _ xi σ hσ => deck_eq_one_of_all_finiteH1_trivial N (hgenus hg) B xi σ hσ)
      (e z) (by
      intro a
      have hcomm : z * e.symm a = e.symm a * z :=
        (Subgroup.mem_center_iff.mp hz (e.symm a)).symm
      have hmap := congrArg e hcomm
      change e z * a = a * e z
      simpa only [map_mul, e.apply_symm_apply] using hmap)
  exact e.injective (he.trans (map_one e).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.