Line-bundle data from an intrinsically invertible sheaf

LineBundleData (in Divisors.Determinant) packages an invertible sheaf together with an explicit tensor inverse. dualLine (in Divisors.Dual) produces such an inverse. This file is the one place where the two meet.

Why this is its own file

It is the only thing in Divisors.Dual that ever needed Divisors.Determinant: three names out of the thirty-seven that file declares, in eleven lines out of seven hundred and forty. That one edge put Dual downstream of Determinant, and so downstream of ExteriorPower, which is the single most expensive module in the repository. Lifting the edge into a leaf costs one file and buys two things:

• the cold-build critical path drops from 1219s to 1041s, because Dual no longer waits on ExteriorPower and the two elaborate in parallel;
• a change to ExteriorPower rebuilds 271s of downstream work instead of 507s, and a change to Determinant 187s instead of 423s.

Keep this file a leaf. Anything added here that does not genuinely need both Determinant and Dual belongs in whichever of them it actually depends on, or the edge comes back.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.ofIsInvertible {X : Scheme} (L : X.Modules) [hL : (have this := L; this).IsInvertible] : LineBundleData X

Upgrade an intrinsically invertible sheaf to line-bundle data with an explicit sheafified-dual tensor inverse.

Equations

• AlgebraicGeometry.Scheme.Modules.LineBundleData.ofIsInvertible L = { line := L, inverse := L.dualLine, lineIsInvertible := hL, inverseIsInvertible := ⋯, tensorInverseIso := L.tensorDualIso }