NYLL
Module

RationalPuncturedChart.lean

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

Module documentation

The affine chart obtained by removing infinity

Affineness is obtained from the proved finite-coordinate construction for pointed proper curves. The actual image of the section ring in the function field is then identified with the intersection of the finite valuation rings, hence with the polynomial ring. Both steps are proved for the given open subset, rather than supplied as comparison assumptions.

Imports7
Imported by3

Declarations

theorem

isAffineOpen_complement_of_degree_one

L34 ↗
AnabelianGeometry.GeometricFundamentalGroup.isAffineOpen_complement_of_degree_one
Documentation

The complement of a degree-one closed point on a smooth proper curve model is affine.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve NeronModelInfra
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
Lean source · statement
theorem isAffineOpen_complement_of_degree_one
    {K F : Type u} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
    (M : CurveModel K F) (x : closedPoints M.C) (hx : (M.placeOfPoint x).deg = 1)
    (U : M.C.Opens) (hU : (U : Set M.C) = {x.1}ᶜ) : IsAffineOpen U
theorem

nonempty_affineLine_iso_of_complement_infinity

L65 ↗
AnabelianGeometry.GeometricFundamentalGroup.nonempty_affineLine_iso_of_complement_infinity
Documentation

Removing the point at infinity from any proper rational curve model gives the actual affine line as a scheme. No affine-chart or coordinate-ring isomorphism is assumed.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve NeronModelInfra
open scoped Polynomial
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_affineLine_iso_of_complement_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}ᶜ) :
    Nonempty (U.toScheme ≅ Spec (.of K[X]))

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