Extending rational-function maps from valuation-ring stalks

The properness of ℙ¹_K extends the function-field point [g : 1] over any point whose local ring is a valuation ring. Mathlib's spreading-out theorem then produces a representative of the rational map on an open neighbourhood of that point. Consequently, if every stalk of an integral scheme is a valuation ring, the rational map attached to g is defined everywhere.

This is the extension step in the geometric proof of the product formula from TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve". For a smooth curve, the remaining input to this theorem is the local regularity/DVR result for its stalks.

theorem TauCeti.AlgebraicGeometry.SchemePartialMap.specMap_stalkSpecializes_fromSpecStalkOfMem {X Y : AlgebraicGeometry.Scheme} (p : X.PartialMap Y) {x y : ↥X} (hxy : x ⤳ y) (hy : y ∈ p.domain) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes hxy)) (p.fromSpecStalkOfMem hy) = p.fromSpecStalkOfMem ⋯

Restriction of a partial map to stalks is compatible with specialization inside its domain.

theorem TauCeti.AlgebraicGeometry.SchemePartialMap.fromFunctionField_eq_specMap_fromSpecStalkOfMem {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥X] (p : X.PartialMap Y) (x : ↥X) (hx : x ∈ p.domain) : p.fromFunctionField = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes ⋯)) (p.fromSpecStalkOfMem hx)

The function-field restriction of a partial map factors through its restriction to the stalk at any point of its domain.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.instNonemptyCarrierCarrierCommRingCatToSchemeTopOpens_2 {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.mem_rationalFunctionMap_domain_of_valuationRing {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) (x : ↥X) [IsDomain ↑(X.presheaf.stalk x)] [ValuationRing ↑(X.presheaf.stalk x)] : x ∈ (rationalFunctionMap K f g).domain

If the local ring at x is a valuation ring, the rational-function map to ℙ¹_K is defined at x.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap_domain_eq_top_of_valuationRings {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) (hValuation : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) : (rationalFunctionMap K f g).domain = ⊤

If every local ring of an integral scheme is a valuation ring, every rational-function map X ⤏ ℙ¹_K is defined on all of X.