Module

TwoPuncturesGenusZero.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.TwoPuncturesGenusZero

1 declaration indexed from sourceView source ↗

Module documentation

The two-puncture chart from coherent genus zero

Starting from the actual structure-sheaf H¹ dimension of a smooth proper integral curve, we construct its curve model and transport both specified punctures. The resulting scheme isomorphism identifies their complement with the spectrum of the Laurent polynomial ring. This geometric theorem alone does not assert the structure of its étale fundamental group.

Imports4

Imported by3

theorem

nonempty_laurent_iso_of_finrank_H1_eq_zero_complement_pair

L30 ↗

AnabelianGeometry.GeometricFundamentalGroup.nonempty_laurent_iso_of_finrank_H1_eq_zero_complement_pair

Documentation

Over an algebraically closed field, a smooth proper integral curve of coherent genus zero minus any two distinct closed points is isomorphic as a scheme to the Laurent polynomial chart. There is no characteristic assumption, and neither coordinates nor a curve model are inputs.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem nonempty_laurent_iso_of_finrank_H1_eq_zero_complement_pair
    {K : Type} [Field K] [IsAlgClosed 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}ᶜ) :
    Nonempty (U.toScheme ≅ Spec (.of (LaurentPolynomial K)))

Module documentation

The two-puncture chart from coherent genus zero

Declarations

nonempty_laurent_iso_of_finrank_H1_eq_zero_complement_pair