Rational points of a curve of positive genus are separated by their ideal sheaves

Let Y be a smooth proper integral curve over a field K with positive genus. Two rational points s and t of Y whose ideal line bundles 𝒪(-s) and 𝒪(-t) are isomorphic coincide.

The ideal sheaf of a rational point s hitting the closed point p is 𝒪(-p) (AlgebraicGeometry.Scheme.Hom.kerSheafIsoNegPoint), so isomorphic ideal sheaves make the two points linearly equivalent as Weil divisors. Linearly equivalent rational points on a curve of positive genus are equal (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.eq_of_linearlyEquivalent_ofPoint_of_genus_pos), and a section of Y ⟶ Spec K is determined by its underlying point.

Main declarations

• AlgebraicGeometry.Scheme.Hom.eq_of_mk_toInvertibleSheaf_eq_of_genus_pos: two rational points of a smooth proper curve of positive genus whose ideal sheaves are isomorphic coincide.

References

• R. Hartshorne, Algebraic Geometry, Chapter IV, Section 1: on a curve of positive genus distinct points are not linearly equivalent.

theorem AlgebraicGeometry.Scheme.Hom.eq_of_mk_toInvertibleSheaf_eq_of_genus_pos {K : Type u} [Field K] {Y : Scheme} [Y.Over (Spec ↧K)] [IsIntegral Y] [IsProper (Y ↘ Spec ↧K)] [SmoothOfRelativeDimension 1 (Y ↘ Spec ↧K)] (hg : 0 < genus K Y) {s t : Spec ↧K ⟶ Y} (hs : CategoryTheory.CategoryStruct.comp s (Y ↘ Spec ↧K) = CategoryTheory.CategoryStruct.id (Spec ↧K)) (ht : CategoryTheory.CategoryStruct.comp t (Y ↘ Spec ↧K) = CategoryTheory.CategoryStruct.id (Spec ↧K)) (h : TauCeti.AlgebraicGeometry.LineBundleClass.mk ⋯.toInvertibleSheaf = TauCeti.AlgebraicGeometry.LineBundleClass.mk ⋯.toInvertibleSheaf) : s = t

Rational points of a curve of positive genus are separated by their ideal sheaves. Let Y be a smooth proper integral curve over a field K with positive genus. If two rational points s and t have isomorphic ideal line bundles 𝒪(-s) ≅ 𝒪(-t), then s = t.