NYLL
Module

OnePunctureGenusZero.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.OnePunctureGenusZero
2 declarations indexed from sourceView source ↗

Module documentation

The genus-zero one-puncture case from coherent cohomology

The input genus is the dimension of the actual structure-sheaf H¹. We construct the curve model, transport the specified closed point and its open complement, and obtain an actual affine-line isomorphism. This proves the fundamental-group structure for the general case (g,r) = (0,1).

Imports6
Imported by1

Declarations

theorem

nonempty_affineLine_iso_of_finrank_H1_eq_zero_complement

L31 ↗
AnabelianGeometry.GeometricFundamentalGroup.nonempty_affineLine_iso_of_finrank_H1_eq_zero_complement
Documentation

A smooth proper integral curve of coherent genus zero, minus any one closed point, is the affine line over an algebraically closed field of characteristic zero.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem nonempty_affineLine_iso_of_finrank_H1_eq_zero_complement
    {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 : closedPoints X) (U : X.Opens) (hU : (U : Set X) = {x.1}ᶜ) :
    Nonempty (U.toScheme ≅ Spec (.of K[X]))
theorem

subsingleton_fundamentalGroup_of_finrank_H1_eq_zero_complement

L67 ↗
AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fundamentalGroup_of_finrank_H1_eq_zero_complement
Documentation

For (g,r) = (0,1) in characteristic zero, the actual étale fundamental group is trivial. The genus uses coherent H¹; the single puncture is the actual complement of the given open.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem subsingleton_fundamentalGroup_of_finrank_H1_eq_zero_complement
    {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 : closedPoints X) (U : X.Opens) (hU : (U : Set X) = {x.1}ᶜ)
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    Subsingleton π₁ᵉᵗ(ξ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.