Duals of line bundles #

The internal-Hom dual of an invertible sheaf is again invertible. Evaluation identifies the tensor product of a line bundle with its dual with the trivial line bundle.

Main declarations #

InvertibleSheaf.dual is the dual line bundle;
InvertibleSheaf.dualCongr transports an isomorphism through duality;
InvertibleSheaf.evaluationDualIsoSheaf packages internal-Hom evaluation as an isomorphism;
InvertibleSheaf.tensorDualIso identifies L ⊗ L.dual with the trivial line bundle.

These constructions supply inverses for the Picard group of a scheme.

source

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.dual {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :

InvertibleSheaf X

The dual line bundle, defined as the internal Hom into the structure sheaf.

Equations

L.dual = { obj := SheafOfModules.dual L.obj, property := ⋯ }

Instances For

source

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.dual_obj {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :

L.dual.obj = SheafOfModules.dual L.obj

The underlying sheaf of the dual line bundle is the internal-Hom dual.

source

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongrIso {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

L.dual.obj ≅ K.dual.obj

The sheaf isomorphism underlying transport through duality.

Equations

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

Instances For

source

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongrIso_hom {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

(dualCongrIso e).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToIso ⋯).hom (CategoryTheory.CategoryStruct.comp (SheafOfModules.dualIso ((SheafOfModules.isInvertible X).ι.mapIso e)).hom (CategoryTheory.eqToIso ⋯).inv)

The forward map of dualCongrIso is the internal-Hom map induced by precomposition with the inverse isomorphism, transported to the underlying sheaves of the dual line bundles.

source

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongrIso_inv {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

(dualCongrIso e).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToIso ⋯).hom (CategoryTheory.CategoryStruct.comp (SheafOfModules.dualIso ((SheafOfModules.isInvertible X).ι.mapIso e)).inv (CategoryTheory.eqToIso ⋯).inv)

The inverse map of dualCongrIso is the internal-Hom map induced by precomposition with the forward isomorphism, transported to the underlying sheaves of the dual line bundles.

source

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongr {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

L.dual ≅ K.dual

An isomorphism of line bundles induces an isomorphism of their duals.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongr_hom_val {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

(dualCongr e).hom.hom.val = (dualCongrIso e).hom.val

source

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.dualCongr_inv_val {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} (e : L ≅ K) :

(dualCongr e).inv.hom.val = (dualCongrIso e).inv.val

source

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.evaluationDualIsoSheaf {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :

CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (SheafOfModules.dual L.obj) ≅ SheafOfModules.unit X.ringCatSheaf

Evaluation of a line bundle against its internal-Hom dual, as an isomorphism of sheaves.

Equations

L.evaluationDualIsoSheaf = CategoryTheory.asIso ((CategoryTheory.ihom.ev L.obj).app (SheafOfModules.unit X.ringCatSheaf))

Instances For

source

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.evaluationDualIsoSheaf_hom {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :

L.evaluationDualIsoSheaf.hom = (CategoryTheory.ihom.ev L.obj).app (SheafOfModules.unit X.ringCatSheaf)

The forward map of evaluationDualIsoSheaf is internal-Hom evaluation.

source

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorDualIsoSheaf {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :

(L.tensorProduct L.dual).obj ≅ (trivial X).obj

The sheaf isomorphism underlying evaluation of a line bundle against its dual.

Equations

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

Instances For

source

The forward map of tensorDualIsoSheaf is the tensor comparison followed by internal-Hom evaluation and the identification of the tensor unit with the trivial line bundle.

source