Line bundles from locally principal Weil divisors

Let X be a locally Noetherian integral scheme of dimension at most one whose codimension-one local rings are discrete valuation rings. This file proves that a locally principal Weil divisor D defines a line bundle 𝒪_X(D).

The local-principality API supplies, around every point, a nonzero rational function whose order agrees with D. Multiplication by this local equation identifies the restriction of 𝒪_X(D) with that of 𝒪_X(0). Since 𝒪_X(0) ≅ 𝒪_X, these local isomorphisms form a rank-one trivialization atlas.

Main declarations

• SchemeWeilDivisor.IsLocallyPrincipal.isInvertible_sheaf proves that the sheaf of a locally principal Weil divisor is invertible;
• SchemeWeilDivisor.IsLocallyPrincipal.toInvertibleSheaf packages it as an object of the category of invertible sheaves on X.

The construction follows Hartshorne, Algebraic Geometry, II.6.11 and the Stacks Project, Divisors, Tags 0BE0 and 0BE9.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.IsLocallyPrincipal.isInvertible_sheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsLocallyNoetherian X] {D : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : SheafOfModules.isInvertible X D.sheaf

The sheaf of a locally principal Weil divisor is a line bundle. On a locally Noetherian integral scheme of dimension at most one whose codimension-one local rings are discrete valuation rings, local equations for D trivialize 𝒪_X(D) as a rank-one module sheaf.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.IsLocallyPrincipal.toInvertibleSheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsLocallyNoetherian X] {D : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : InvertibleSheaf X

The invertible sheaf 𝒪_X(D) attached to a locally principal Weil divisor.

Equations

• hD.toInvertibleSheaf hX = { obj := D.sheaf, property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.IsLocallyPrincipal.toInvertibleSheaf_obj {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] [AlgebraicGeometry.IsLocallyNoetherian X] {D : SchemeWeilDivisor X} (hD : D.IsLocallyPrincipal) (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : (hD.toInvertibleSheaf hX).obj = D.sheaf

The underlying sheaf of the line bundle attached to D is 𝒪_X(D).