Separation of rational places in positive genus

In a function field of positive genus with exact constants, a rational place P has ℓ(P) = 1: there is no nonconstant function with just a simple pole at P, since 1 is its first Weierstrass gap. Consequently the complete linear system of P consists of P alone. Distinct rational places therefore give distinct divisor classes, also after translation by any fixed base divisor P₀.

This is the divisor-class point-separation input to the Abel–Jacobi embedding of a curve of positive genus. It does not assert the existence of a Picard scheme or an immersion.

References

• R. Hartshorne, Algebraic Geometry, Chapter IV, Section 1 and Theorem 4.17.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 1.6.8.

theorem TauCeti.Divisor.dim_ofPoint_eq_one_of_genus_pos {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 0 < genus k F) {P : Place k F} (hP : P.degree = 1) : dim (AlgebraicGeometry.WeilDivisor.ofPoint P) = 1

At a rational place of a positive-genus function field with exact constants, the Riemann–Roch space allowing a simple pole has dimension one.

theorem TauCeti.Place.eq_of_linearlyEquivalent_ofPoint_of_genus_pos {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 0 < genus k F) {P Q : Place k F} (hP : P.degree = 1) (h : (orderSystem hF).LinearlyEquivalent (AlgebraicGeometry.WeilDivisor.ofPoint P) (AlgebraicGeometry.WeilDivisor.ofPoint Q)) : P = Q

Linearly equivalent places coincide if one is rational and the function field has positive genus and exact constants. The second place need not be assumed rational.

theorem TauCeti.Place.eq_of_divisorClass_pointDifference_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P₀ : Place k F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 0 < genus k F) {P Q : Place k F} (hP : P.degree = 1) (h : (orderSystem hF).divisorClass (AlgebraicGeometry.WeilDivisor.pointDifference P P₀) = (orderSystem hF).divisorClass (AlgebraicGeometry.WeilDivisor.pointDifference Q P₀)) : P = Q

Distinct places of degree one of a positive-genus function field have distinct classes relative to a base place.