Rational functions without poles are regular

On a locally Noetherian integral scheme a regular function has nonnegative order at every point where it is defined (TauCeti.AlgebraicGeometry.Scheme.ord_germToFunctionField_nonneg). This file proves the converse for a scheme of dimension at most one whose codimension-one local rings on an open subset U are discrete valuation rings: a rational function with no poles on U is the germ of a regular function on U.

Main declarations

• TauCeti.AlgebraicGeometry.Scheme.exists_algebraMap_stalk_eq_of_ord_nonneg: at a codimension-one point whose local ring is a discrete valuation ring, a rational function of nonnegative order lies in that local ring;
• TauCeti.AlgebraicGeometry.Scheme.exists_algebraMap_stalk_eq_of_coheight_eq_zero: at a point with no proper generization the local ring is already the whole function field;
• TauCeti.AlgebraicGeometry.Scheme.exists_germToFunctionField_eq_of_ord_nonneg: a rational function with nonnegative order at every codimension-one point of U is the germ at the generic point of a section of 𝒪_X over U;
• TauCeti.AlgebraicGeometry.Scheme.exists_unit_germToFunctionField_eq_of_ord_eq_zero: a nonzero rational function with zero order at every codimension-one point of U is the germ of a unit of Γ(X, U).

The third statement is the one-dimensional case of algebraic Hartogs' principle, and it is the input that identifies the sheaf 𝒪_X(0) of the zero divisor with the structure sheaf. The last one applies it to a function and to its inverse; it is the local comparison used to glue the local equations of a locally principal Weil divisor into a Cartier divisor.

The argument follows Hartshorne, Algebraic Geometry, II.6.3A and Proposition II.6.11, in the dimension-one case where the intersection of the local rings can be taken over the points of U themselves. The local step is Mathlib's IsDiscreteValuationRing.exists_lift_of_le_one together with Ring.ordFrac_eq_valuation_inv, and the global step, that a rational function lying in every local ring of U is regular on U, is TauCeti.AlgebraicGeometry.Scheme.exists_germToFunctionField_eq_of_forall_mem_range.

theorem TauCeti.AlgebraicGeometry.Scheme.exists_algebraMap_stalk_eq_of_ord_nonneg {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] (hx : Order.coheight x = 1) {f : ↑X.functionField} (hf : 0 ≤ AlgebraicGeometry.Scheme.ord f x) : ∃ (g : ↑(X.presheaf.stalk x)), (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) g = f

At a codimension-one point whose local ring is a discrete valuation ring, a rational function of nonnegative order is a section of that local ring. This is the local half of the statement that a rational function without poles is regular.

theorem TauCeti.AlgebraicGeometry.Scheme.exists_algebraMap_stalk_eq_of_coheight_eq_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {x : ↥X} (hx : Order.coheight x = 0) (f : ↑X.functionField) : ∃ (g : ↑(X.presheaf.stalk x)), (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) g = f

At a point with no proper generization the local ring is the whole function field: it is a zero-dimensional local domain, hence a field, and it has the function field as its field of fractions.

theorem TauCeti.AlgebraicGeometry.Scheme.exists_germToFunctionField_eq_of_ord_nonneg {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (hDVR : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)) (hU : ∀ y ∈ U, Order.coheight y ≤ 1) {f : ↑X.functionField} (hf : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → 0 ≤ AlgebraicGeometry.Scheme.ord f ↑y) : ∃ (a : ↑(X.presheaf.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) a = f

A rational function without poles is regular. On a locally Noetherian integral scheme, let U be a nonempty open subset of dimension at most one whose codimension-one local rings are discrete valuation rings. A rational function whose order is nonnegative at every codimension-one point of U is the image of a section of 𝒪_X over U.

This is the one-dimensional case of algebraic Hartogs' principle. The hypothesis on the dimension enters only through the points of U: at a codimension-one point the discrete valuation gives the bound, and at a point with no proper generization the local ring is already the function field.

theorem TauCeti.AlgebraicGeometry.Scheme.exists_unit_germToFunctionField_eq_of_ord_eq_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (hDVR : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)) (hU : ∀ y ∈ U, Order.coheight y ≤ 1) {f : (↑X.functionField)ˣ} (hf : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → AlgebraicGeometry.Scheme.ord ↑f ↑y = 0) : ∃ (a : (↑(X.presheaf.obj (Opposite.op U)))ˣ), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) ↑a = ↑f

A rational function without zeros or poles is a regular unit. On a locally Noetherian integral scheme, let U be a nonempty open subset of dimension at most one whose codimension-one local rings are discrete valuation rings. A nonzero rational function whose order vanishes at every codimension-one point of U is the germ of a unit of Γ(X, U).

Simultaneous regularity of the function and its inverse makes the resulting section a unit.