Extending rational functions on smooth relative curves

Every stalk of an integral scheme smooth of relative dimension one over a field is a valuation ring, and its non-generic stalks are discrete valuation rings. Consequently every non-generic point has codimension one and is closed, so proper closed subsets of a Noetherian relative curve are finite. Combining this local algebra with properness of the projective line shows that the rational map [g : 1] attached to a nonzero rational function is defined everywhere.

This discharges the local-extension step in the geometric product-formula argument from TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve".

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.valuationRing_stalk_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : ↥X) : ValuationRing ↑(X.presheaf.stalk x)

A stalk of an integral scheme smooth of relative dimension one over a field is a valuation ring.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isDiscreteValuationRing_stalk_of_ne_genericPoint_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : ↥X) (hx : x ≠ genericPoint ↥X) : IsDiscreteValuationRing ↑(X.presheaf.stalk x)

The stalk at any non-generic point of an integral scheme smooth of relative dimension one over a field is a discrete valuation ring.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isDiscreteValuationRing_stalk_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : CodimensionOnePoint X) : IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)

A codimension-one stalk of an integral scheme smooth of relative dimension one over a field is a discrete valuation ring.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coheight_eq_one_of_ne_genericPoint_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : ↥X) (hx : x ≠ genericPoint ↥X) : Order.coheight x = 1

Every non-generic point of an integral smooth relative curve has codimension one.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isClosed_singleton_of_ne_genericPoint_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : ↥X) (hx : x ≠ genericPoint ↥X) : IsClosed {x}

Every non-generic point of an integral smooth relative curve is a closed point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_closed_subset_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (Z : Set ↥X) (hZ : IsClosed Z) (hZne : Z ≠ Set.univ) : Z.Finite

Every proper closed subset of an integral Noetherian smooth relative curve is finite.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_eq_ord_stalk_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x : CodimensionOnePoint X) {a : ↑(X.presheaf.stalk ↑x)} (ha : a ≠ 0) (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (algebraMap ↑(X.presheaf.stalk ↑x) ↑X.functionField) a) : (orderAt x) g = ↑(Ring.ord (↑(X.presheaf.stalk ↑x)) a).toNat

On a smooth relative curve, a rational function represented by a nonzero element of a codimension-one stalk has order equal to the finite order of that stalk element.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap_domain_eq_top_of_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : (rationalFunctionMap K f g).domain = ⊤

The projective-line-valued rational map [g : 1] on an integral smooth relative curve is defined everywhere.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : X ⟶ ProjectiveLine.scheme K

The everywhere-defined morphism X ⟶ ℙ¹_K represented by the rational function [g : 1] on an integral smooth relative curve.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_toRationalMap (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : AlgebraicGeometry.Scheme.Hom.toRationalMap (rationalFunctionMorphism K X f g) = rationalFunctionMap K f g

The global rational-function morphism represents the rational map from which it was constructed.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_fromFunctionField (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : (AlgebraicGeometry.Scheme.Hom.toPartialMap (rationalFunctionMorphism K X f g)).fromFunctionField = rationalFunctionGenericMorphism K f g

Restriction of the global rational-function morphism to the function field is the point [g : 1].

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_comp_structureMap (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : CategoryTheory.CategoryStruct.comp (rationalFunctionMorphism K X f g) (ProjectiveLine.structureMap K) = f

The global rational-function morphism is a morphism over Spec K.