Line-bundle classes attached to Weil divisors

On a Noetherian integral scheme of dimension at most one whose codimension-one local rings are discrete valuation rings, every Weil divisor D is locally principal. Its sheaf 𝓞_X(D) is therefore a line bundle. Linearly equivalent divisors have isomorphic sheaves, so this construction descends from Weil divisors to the divisor class group.

Main declarations

• SchemeWeilDivisor.toInvertibleSheaf packages 𝓞_X(D) as an invertible sheaf;
• SchemeWeilDivisor.toLineBundleClass is its isomorphism class;
• SchemeWeilDivisor.classGroupToLineBundleClass is the induced map from the divisor class group to line-bundle classes, and SchemeWeilDivisor.classGroupToLineBundleClass_injective says that it is injective: a divisor is determined up to linear equivalence by the isomorphism class of its sheaf.

This is the set-level divisor-to-line-bundle comparison. Its compatibility with addition, 𝓞_X(D + E) ≅ 𝓞_X(D) ⊗ 𝓞_X(E), needs the tensor product of module sheaves and is proved in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/TensorProduct.lean, and its surjectivity in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Picard.lean.

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

The invertible sheaf 𝓞_X(D) associated to a Weil divisor on a Noetherian integral scheme of dimension at most one whose codimension-one local rings are DVRs.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toInvertibleSheaf hX D = ⋯.toInvertibleSheaf hX

@[simp]

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

The underlying sheaf of SchemeWeilDivisor.toInvertibleSheaf is 𝓞_X(D).

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) (D : SchemeWeilDivisor X) : LineBundleClass X

The isomorphism class of the line bundle 𝓞_X(D) associated to a Weil divisor.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass hX D = TauCeti.AlgebraicGeometry.LineBundleClass.mk (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toInvertibleSheaf hX D)

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_eq_mk_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {D : SchemeWeilDivisor X} {L : InvertibleSheaf X} : toLineBundleClass hX D = LineBundleClass.mk L ↔ Nonempty ((toInvertibleSheaf hX D).obj ≅ L.obj)

The line-bundle class of D equals the class of L exactly when their underlying sheaves are isomorphic.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_eq_of_linearlyEquivalent {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {D E : SchemeWeilDivisor X} (hDE : (WeilDivisor.OrderSystem.ofScheme X).LinearlyEquivalent D E) : toLineBundleClass hX D = toLineBundleClass hX E

Linearly equivalent Weil divisors determine the same line-bundle class.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : toLineBundleClass hX 0 = 1

The zero divisor determines the trivial line-bundle class.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_principalDivisor {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) (g : Additive (↑X.functionField)ˣ) : toLineBundleClass hX ((WeilDivisor.OrderSystem.ofScheme X).principalDivisor g) = 1

A principal divisor determines the trivial line-bundle class.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : (WeilDivisor.OrderSystem.ofScheme X).ClassGroup → LineBundleClass X

The map from the divisor class group to isomorphism classes of line bundles which sends the class of D to the class of 𝓞_X(D).

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass hX = Quotient.lift (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass hX) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass_divisorClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) (D : SchemeWeilDivisor X) : classGroupToLineBundleClass hX ((WeilDivisor.OrderSystem.ofScheme X).divisorClass D) = toLineBundleClass hX D

The map from divisor classes to line-bundle classes sends the class of D to the class of 𝓞_X(D).

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_eq_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {D E : SchemeWeilDivisor X} : toLineBundleClass hX D = toLineBundleClass hX E ↔ (WeilDivisor.OrderSystem.ofScheme X).LinearlyEquivalent D E

Two Weil divisors have the same line-bundle class exactly when they are linearly equivalent. Every divisor on such a curve is locally principal, so SchemeWeilDivisor.nonempty_iso_sheaf_iff_linearlyEquivalent applies to all of them.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass_injective {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : Function.Injective (classGroupToLineBundleClass hX)

The map from divisor classes to line-bundle classes is injective.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) : classGroupToLineBundleClass hX 0 = 1

The zero divisor class maps to the trivial line-bundle class.