Duals of invertible module sheaves

This file constructs the dual of an invertible module sheaf without assuming an internal-Hom API for sheaves. On an open U, the dual presheaf consists of morphisms from the restriction of the line sheaf to U into the restricted structure sheaf. Evaluation is locally the ordinary rank-one evaluation isomorphism, so sheafification supplies an explicit tensor inverse.

The main public declarations are dualPresheaf, dualLine, tensorDualIso, and dualLine_isInvertible. LineBundleData.ofIsInvertible, which bridges these to the LineBundleData of Divisors.Determinant, lives in Divisors.LineBundleDual.

@[implicit_reducible]

def AlgebraicGeometry.Scheme.Modules.dualCategory {X : Scheme} : CategoryTheory.Category.{u, u + 1} X.Modules

Equations

• AlgebraicGeometry.Scheme.Modules.dualCategory = { toCategoryStruct := AlgebraicGeometry.Scheme.Modules.instCategory.toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.dualMonoidalCategory {X : Scheme} : CategoryTheory.MonoidalCategory X.PresheafOfModules

Equations

• AlgebraicGeometry.Scheme.Modules.dualMonoidalCategory = PresheafOfModules.monoidalCategory

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.dualSymmetricCategory {X : Scheme} : CategoryTheory.SymmetricCategory X.PresheafOfModules

Equations

• AlgebraicGeometry.Scheme.Modules.dualSymmetricCategory = PresheafOfModules.symmetricCategory

noncomputable def AlgebraicGeometry.Scheme.Modules.dualPresheaf {X : Scheme} (L : X.Modules) : X.PresheafOfModules

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.evaluation {X : Scheme} (L : X.Modules) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toPresheafOfModules X).obj L) L.dualPresheaf ⟶ PresheafOfModules.unit X.ringCatSheaf.obj

Equations

• L.evaluation = { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) => AlgebraicGeometry.Scheme.Modules.evaluationApp✝ L U, naturality := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.dualLine {X : Scheme} (L : X.Modules) : X.Modules

The dual line sheaf, obtained by sheafifying local morphisms into the structure sheaf.

Equations

• L.dualLine = (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).obj L.dualPresheaf

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorDualIso {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] : L.tensorObj L.dualLine ≅ SheafOfModules.unit X.ringCatSheaf

Evaluation identifies a line sheaf tensored with its sheafified local dual with the structure sheaf.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.dualLine_isInvertible {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] : (have this := L.dualLine; this).IsInvertible

The sheafified local dual of an invertible sheaf is invertible.