Isomorphic divisor sheaves come from linearly equivalent divisors

TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean attaches to a Weil divisor D on an integral scheme the subsheaf 𝒪_X(D) of the sheaf 𝒦_X of rational functions, and shows in SchemeWeilDivisor.nonempty_iso_sheaf_of_linearlyEquivalent that linearly equivalent divisors have isomorphic sheaves. This file proves the converse for locally principal divisors: the isomorphism class of 𝒪_X(D) determines the class of D in the divisor class group.

The mechanism is that an 𝒪_X-linear map from 𝒪_X(D) to 𝒦_X is multiplication by a rational function. A local equation for D near the generic point exhibits 𝒪_X(D) as generated there by one rational function, and 𝒦_X is the constant sheaf with value K(X), so the multiplier read off near the generic point already computes the map over every open subset. An isomorphism 𝒪_X(D) ≅ 𝒪_X(E) is therefore multiplication by a unit g of K(X), and comparing the local equations of D - div g and of E at each codimension-one point gives E = D - div g.

Main declarations

• SchemeWeilDivisor.inv_localEquation_mem_sections: the inverse of a local equation for D on U is a section of 𝒪_X(D) over U;
• SchemeWeilDivisor.IsLocallyPrincipal.exists_rationalFunctionsMul_eq: every 𝒪_X-linear map 𝒪_X(D) ⟶ 𝒦_X is the inclusion followed by multiplication by a rational function;
• SchemeWeilDivisor.IsLocallyPrincipal.exists_sheafι_app_ne_zero: 𝒪_X(D) has a section which is a nonzero rational function;
• SchemeWeilDivisor.linearlyEquivalent_of_nonempty_iso_sheaf and SchemeWeilDivisor.nonempty_iso_sheaf_iff_linearlyEquivalent: locally principal divisors with isomorphic sheaves are linearly equivalent, and conversely.

On a curve every Weil divisor is locally principal, so this makes the comparison map SchemeWeilDivisor.classGroupToLineBundleClass of TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/LineBundle.lean injective: that is the injectivity half of Cl(X) ≅ Pic X.

The statement is Hartshorne, Algebraic Geometry, II, Proposition 6.13; the argument given here is the standard one, run through the constant sheaf 𝒦_X rather than through stalks at the generic point. The proofs reuse the divisor sheaf and its multiplication isomorphisms from TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, the local equations of TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/LocallyPrincipal.lean, and Mathlib's TopCat.Presheaf.exists_le_germ_eq and AlgebraicGeometry.Scheme.ord.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.inv_localEquation_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsLocallyNoetherian X] {D : SchemeWeilDivisor X} {U : X.Opens} [Nonempty ↥↑U] {f : Additive (↑X.functionField)ˣ} (hf : ∀ (y : CodimensionOnePoint X), ↑y ∈ U → WeilDivisor.coeff D y = (orderAt y) f) : (Scheme.rationalFunctionsEquiv U).symm (↑(Additive.toMul f))⁻¹ ∈ D.sections U

The inverse of a local equation for D on U is a section of 𝒪_X(D) over U: its order at a codimension-one point of U is exactly -D.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.IsLocallyPrincipal.exists_rationalFunctionsMul_eq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsNoetherian X] {D : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (ψ : D.sheaf ⟶ Scheme.rationalFunctions X) : ∃ (g : ↑X.functionField), ψ = CategoryTheory.CategoryStruct.comp D.sheafι (Scheme.rationalFunctionsMul X g)

An 𝒪_X-linear map from 𝒪_X(D) to the rational functions is multiplication by a rational function. A local equation for D near the generic point trivializes 𝒪_X(D) there, and the resulting multiplier is independent of the open subset because 𝒦_X is the constant sheaf.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.IsLocallyPrincipal.exists_sheafι_app_ne_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsNoetherian X] {D : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) : ∃ (U : X.Opens) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app D.sheafι U)) s ≠ 0

A local equation near the generic point exhibits a section of 𝒪_X(D) which is a nonzero rational function.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.linearlyEquivalent_of_nonempty_iso_sheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsNoetherian X] {D E : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (hE : E.IsLocallyPrincipal) (h : Nonempty (D.sheaf ≅ E.sheaf)) : (WeilDivisor.OrderSystem.ofScheme X).LinearlyEquivalent D E

Isomorphic divisor sheaves come from linearly equivalent divisors. This is the converse of SchemeWeilDivisor.nonempty_iso_sheaf_of_linearlyEquivalent.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.nonempty_iso_sheaf_iff_linearlyEquivalent {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsNoetherian X] {D E : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (hE : E.IsLocallyPrincipal) : Nonempty (D.sheaf ≅ E.sheaf) ↔ (WeilDivisor.OrderSystem.ofScheme X).LinearlyEquivalent D E

Two divisor sheaves are isomorphic exactly when the divisors are linearly equivalent.