Sections of line bundles on integral schemes

A section of a line bundle on an integral scheme is determined by its restriction to any nonempty open subset, and even by its germ at any point of its domain. In particular, the map to the generic stalk is injective. A rational section is regular on an open subset exactly when it comes from the stalk at every point of that subset (mem_range_genericPoint_germ_iff). These are the uniqueness and gluing inputs for realizing a line bundle as a subsheaf of rational sections in the divisor--line-bundle correspondence.

The statements require only integrality; no Noetherian, dimension, or properness hypotheses are needed.

See Hartshorne, Algebraic Geometry, II.6, for the rational-section construction of the divisor associated with a line bundle. The local regularity argument extends the gluing argument of TauCeti.AlgebraicGeometry.Scheme.exists_germToFunctionField_eq_of_forall_mem_range from regular functions to line-bundle sections.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.map_injective_of_isIntegral {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (L : InvertibleSheaf X) {U V : X.Opens} (i : V ⟶ U) [Nonempty ↥↑V] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (L.obj.presheaf.map i.op))

Restricting sections of a line bundle on an integral scheme to a nonempty open subset is injective.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.germ_injective_of_isIntegral {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (L : InvertibleSheaf X) {U : X.Opens} (x : ↥X) (hx : x ∈ U) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (L.obj.presheaf.germ U x hx))

A section of a line bundle on an integral scheme is determined by its germ at any point of its domain. At the generic point this embeds sections into rational sections.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.mem_range_genericPoint_germ_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (L : InvertibleSheaf X) {U : X.Opens} [Nonempty ↥↑U] (q : ↑(L.obj.presheaf.stalk (genericPoint ↥X))) : q ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (L.obj.presheaf.germ U (genericPoint ↥X) ⋯)) ↔ ∀ x ∈ U, q ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (L.obj.presheaf.stalkSpecializes ⋯))

A rational section of a line bundle is regular on a nonempty open subset if and only if it lies in the image of the stalk at every point of that open subset. The local images are taken under specialization to the generic stalk.