Documentation

DerivedAlgGeo.AlgebraicGeometry.Divisors.CartierLineBundle

Cartier divisors as line-bundle data #

The associated sheaf of a Cartier divisor is intrinsically invertible. CartierDivisor.lineBundleData upgrades it to the repository's explicit LineBundleData interface, choosing the sheafified dual as tensor inverse. The resulting Picard class agrees with the direct Cartier-divisor construction.

This bridge is deliberately a leaf: it needs both the associated-sheaf API and the determinant/dual line-bundle API. Keeping it out of the narrower Divisors.AssociatedSheaf umbrella avoids imposing the expensive determinant dependency on consumers such as effective-divisor exact sequences.

source
noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.lineBundleData {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
Modules.LineBundleData X

The line-bundle package canonically associated to a Cartier divisor. Its underlying sheaf is O_X(D) and its chosen inverse is the sheafified dual.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.CartierDivisor.lineBundleData_line {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
    (lineBundleData D).line = associatedSheaf D
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.CartierDivisor.lineBundleData_inverse {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
    (lineBundleData D).inverse = (associatedSheaf D).dualLine
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.CartierDivisor.lineBundleData_toPic {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
    (lineBundleData D).toPic = toPic D

    The Picard class obtained through explicit line-bundle data is the same class as the direct Cartier-divisor construction. The chosen inverse objects may differ, but Pic remembers only their invertible classes.

    source
    theorem AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf_isCoherent {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
    X.coherent (associatedSheaf D)

    A Cartier divisor's associated sheaf is coherent, exposed through the canonical line-bundle adapter rather than reproved from local equations.