Nyll.AnabelianGeometry.GeometricFundamentalGroup.TwoPuncturesProcyclic

Module documentation

Procyclicity for a genus-zero curve with two punctures

The genus is the dimension of actual coherent H¹. The proved Laurent-chart isomorphism and the actual pullback equivalence of finite etale covers transport a topological generator to the original curve. Procyclicity does not by itself assert that the group is the full profinite completion of the integers; the latter also requires finite quotients of all orders.

theorem

exists_topological_generator_of_finrank_H1_eq_zero_complement_pair

L30 ↗

AnabelianGeometry.GeometricFundamentalGroup.exists_topological_generator_of_finrank_H1_eq_zero_complement_pair

Documentation

The actual etale fundamental group of a smooth proper genus-zero curve minus two distinct closed points is topologically generated by one element in characteristic zero.

Source context 3 commands

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

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

Lean source · statement

theorem exists_topological_generator_of_finrank_H1_eq_zero_complement_pair
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    (X : Scheme.{0}) [IsIntegral X] (c : X ⟶ Spec (.of K))
    [IsProper c] [SmoothOfRelativeDimension 1 c] (𝒱 : X.TwoAffineOpenCover)
    (hg : Module.finrank K (𝒱.structureSheafSections c).H1 = 0)
    (x y : closedPoints X) (hne : x ≠ y)
    (U : X.Opens) (hU : (U : Set X) = {x.1, y.1}ᶜ)
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    ∃ g : π₁ᵉᵗ(ξ), ProCGroups.Generation.TopologicallyGenerates ({g} : Set π₁ᵉᵗ(ξ))

Module documentation

Procyclicity for a genus-zero curve with two punctures

Declarations

exists_topological_generator_of_finrank_H1_eq_zero_complement_pair