Regular rational differentials and Weil orders on curves

The rational image of a differential stalk at a discrete valuation ring point is the image of the Kähler differentials of its associated place's valuation ring. This comparison holds over an arbitrary field and does not require that the place be rational.

For an invertible differential sheaf on an open subset of dimension at most one, regularity is detected at its codimension-one points. There the stalk of the differential sheaf is free of rank one, so the Kähler differentials of the place's valuation ring are generated by a single differential d z (exists_span_D_eq_top_of_isInvertible). Over an exact constant field, the Kähler–Weil comparison at such a place identifies regularity with nonnegative Weil order. This holds at places of every degree and over an imperfect constant field, so no codimension-one point needs to be rational and no residue field needs to be separable. Thus a nonzero Weil differential corresponds to a regular section on the open subset exactly when it has no poles there. This supplies the local-lattice comparison for identifying the differential line bundle with a canonical divisor sheaf.

References

• R. Hartshorne, Algebraic Geometry, II, Section 8, and IV, Section 1.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section IV.3.

The sheaf regularity criterion is mem_range_rationalDifferential_iff. The valuation-ring comparison uses Scheme.stalkToPlaceIntegersAlgEquiv, the rank-one stalks come from Scheme.Modules.finrank_stalk_of_isInvertible, and the local order criterion uses Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_span_D_eq_top.

theorem TauCeti.AlgebraicGeometry.mem_range_rationalDifferentialStalk_iff_mem_range_map {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] (x : ↥X) [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] (η : Ω[↑X.functionField⁄k]) : η ∈ Set.range ⇑(rationalDifferentialStalk k x) ↔ η ∈ (KaehlerDifferential.map k k ↥(X.toPlace x).integers ↑X.functionField).range

A differential stalk at a discrete valuation ring point has the same rational image as the Kähler differentials of the associated place's valuation ring. This holds for places of arbitrary residue degree.

theorem TauCeti.AlgebraicGeometry.exists_span_D_eq_top_of_isInvertible {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials k X)] (x : ↥X) [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] : ∃ (z : ↥(X.toPlace x).integers), ↥(X.toPlace x).integers ∙ (KaehlerDifferential.D k ↥(X.toPlace x).integers) z = ⊤

If the differential sheaf is invertible, then at a discrete valuation ring point the Kähler differentials of the associated place's valuation ring are generated by a single differential d z. The place may have any residue degree, and the base field need not be perfect.

theorem TauCeti.AlgebraicGeometry.mem_range_rationalDifferential_iff_weilDifferentialOrder_nonneg {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials k X)] (hF : IsFunctionField k ↑X.functionField) (hk : IsIntegrallyClosedIn k ↑X.functionField) {t : ↑X.functionField} (ht : Transcendental k t) [Algebra.IsSeparable ↥k⟮t⟯ ↑X.functionField] (U : X.Opens) [Nonempty ↥↑U] (hU : ∀ y ∈ U, Order.coheight y ≤ 1) (hDVR : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)) (ω : ↥(weilDifferentialSpace k ↑X.functionField)) (hω : ↑ω ≠ 0) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hk ht).symm ω ∈ Set.range ⇑(rationalDifferential k U) ↔ ∀ (y : CodimensionOnePoint X) (hy : ↑y ∈ U), 0 ≤ weilDifferentialOrder hF hk ⋯ hω (X.toPlace ↑y)

Over an exact constant field, when the differential sheaf is invertible, a nonzero Weil differential corresponds to a regular differential on a curve open exactly when its order is nonnegative at every codimension-one point there. The codimension-one points need not be rational, and the constant field need not be perfect.

theorem TauCeti.AlgebraicGeometry.smul_D_mem_range_rationalDifferential_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials k X)] (hF : IsFunctionField k ↑X.functionField) (hk : IsIntegrallyClosedIn k ↑X.functionField) {t : ↑X.functionField} (ht : Transcendental k t) [Algebra.IsSeparable ↥k⟮t⟯ ↑X.functionField] [AlgebraicGeometry.IsLocallyNoetherian X] (U : X.Opens) [Nonempty ↥↑U] (hU : ∀ y ∈ U, Order.coheight y ≤ 1) (hDVR : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)) (f : ↑X.functionField) : f • (KaehlerDifferential.D k ↑X.functionField) t ∈ Set.range ⇑(rationalDifferential k U) ↔ f = 0 ∨ ∀ (y : CodimensionOnePoint X) (hy : ↑y ∈ U), -weilDifferentialOrder hF hk ⋯ ⋯ (X.toPlace ↑y) ≤ AlgebraicGeometry.Scheme.ord f ↑y

The rational differential f dt is regular on U exactly when f satisfies the order bounds of the divisor of the Weil differential dt. Only codimension-one stalks on U are required to be discrete valuation rings, and the constant field is exact but need not be perfect.