Module

CurveModelGenericPointEvaluation.lean

Nyll.AlgebraicCurves.Models.CurveModelGenericPointEvaluation

2 declarations indexed from sourceView source ↗

Module documentation

Evaluation at the actual geometric generic point

The value of a pulled-back rational function at the geometric generic point is its image in the geometric-point field. The proof compares actual scheme stalk maps and the existing place-evaluation map.

Imports4

Imported by2

theorem

evalAt_geometricGenericPoint

L28 ↗

AlgebraicCurve.CurveModel.evalAt_geometricGenericPoint

Documentation

Actual place evaluation at a lifted generic point agrees with the specified embedding of the original function field.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace AlgebraicCurve.CurveModel

Lean source · statement

theorem evalAt_geometricGenericPoint
    {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
    (M : CurveModel K F) {X : Scheme} [IsIntegral X]
    (p : M.C ⟶ X) (φ : X.functionField →+* F)
    (hφ : ∀ (U : X.Opens) [Nonempty U] [Nonempty (p ⁻¹ᵁ U)] (s : Γ(X, U)),
      φ (X.germToFunctionField U s) =
        M.ffEquiv.symm (M.C.germToFunctionField (p ⁻¹ᵁ U) ((p.app U).hom s)))
    (ι : X.functionField →+* K)
    (x : {q : Spec (.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _})
    (hx : x.1 ≫ p =
      Spec.map (CommRingCat.ofHom ι) ≫ X.fromSpecStalk (genericPoint X))
    (r : X.functionField) :
    (M.pointEquivPlace x).evalAt (φ r) = ι r

theorem

ord_geometricGenericPoint

L89 ↗

AlgebraicCurve.CurveModel.ord_geometricGenericPoint