Module

ProperGenusZero.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.ProperGenusZero

1 declaration indexed from sourceView source ↗

Module documentation

The proper genus-zero case from structure-sheaf cohomology

The genus is the dimension of the actual structure-sheaf H¹ on a two-affine cover. Its proved comparison with function-field cohomology, followed by the actual curve-model construction and pullback equivalence, proves triviality of the original étale fundamental group. No presentation theorem, rational coordinate, or comparison assumption is used.

Imports5

Imported by1

Nyll.AnabelianGeometry.GeometricFundamentalGroup.All

theorem

subsingleton_fundamentalGroup_of_finrank_H1_eq_zero

L31 ↗

AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fundamentalGroup_of_finrank_H1_eq_zero

Documentation

A smooth proper integral genus-zero curve over an algebraically closed field of characteristic zero has trivial étale fundamental group. The genus is computed from the actual structure sheaf on a two-affine cover, and the geometric point is arbitrary.

Source context 3 commands

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

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

Lean source · statement

theorem subsingleton_fundamentalGroup_of_finrank_H1_eq_zero
    {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)
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X) :
    Subsingleton π₁ᵉᵗ(ξ)

Module documentation

The proper genus-zero case from structure-sheaf cohomology

Declarations

subsingleton_fundamentalGroup_of_finrank_H1_eq_zero