NYLL
Module

RationalTwoPuncturedChart.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalTwoPuncturedChart
1 declaration indexed from sourceView source ↗

Module documentation

The actual two-puncture chart of a rational curve

The complements of zero and infinity are affine. Their intersection has its actual section ring embedded in the function field, with image equal to the Laurent polynomial image. This constructs the scheme isomorphism with the multiplicative group chart.

Imports8
Imported by2

Declarations

theorem

nonempty_laurent_iso_of_complement_zero_infinity

L37 ↗
AnabelianGeometry.GeometricFundamentalGroup.nonempty_laurent_iso_of_complement_zero_infinity
Documentation

The complement of zero and infinity in a proper rational curve model is the spectrum of the Laurent polynomial ring. The section-ring comparison and affineness are constructed.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
open AlgebraicCurves.Models.Proofs
open CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open AlgebraicCurve.S1c Classical in
Lean source · statement
theorem nonempty_laurent_iso_of_complement_zero_infinity
    {K : Type u} [Field K] [IsAlgClosed K] (M : CurveModel K (RatFunc K))
    (U : M.C.Opens)
    (hU : (U : Set M.C) =
      {(M.placeEquiv.symm (RationalFunctionField.placeInfty K)).1,
        (M.placeEquiv.symm (RationalFunctionField.placeOfPoint K 0)).1}ᶜ) :
    Nonempty (U.toScheme ≅ Spec (.of (LaurentPolynomial K)))

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