Duals of invertible sheaves

The internal-Hom dual of an invertible sheaf is again invertible. Evaluation identifies its tensor product with the original sheaf with the tensor unit, so the two sheaves are mutually inverse under tensor product. This supplies inverses for the Picard group.

Main declarations

• SheafOfModules.IsInvertible.dual says that the dual of an invertible sheaf is invertible;
• SheafOfModules.isIso_evaluation_dual_of_isInvertible says that evaluation of an invertible sheaf against its dual is an isomorphism.

References

• R. Hartshorne, Algebraic Geometry, Chapter II, Section 6.
• The Stacks Project, Section Invertible modules, Tag 01CR.

@[instance_reducible]

noncomputable def TauCeti.SheafOfModules.invertibleDualMonoidalCategory {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (X : C) : CategoryTheory.MonoidalCategory (SheafOfModules ((ringCatSheaf R).over X))

The monoidal structure on sheaves of modules over the restriction of R to X.

Equations

• TauCeti.SheafOfModules.invertibleDualMonoidalCategory X = TauCeti.SheafOfModules.monoidalCategory (R.over X)

@[instance_reducible]

noncomputable def TauCeti.SheafOfModules.invertibleDualMonoidalClosed {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (X : C) : CategoryTheory.MonoidalClosed (SheafOfModules ((ringCatSheaf R).over X))

The closed monoidal structure on sheaves of modules over the restriction of R to X.

Equations

• TauCeti.SheafOfModules.invertibleDualMonoidalClosed X = TauCeti.SheafOfModules.monoidalClosed (R.over X)

instance SheafOfModules.IsInvertible.dual {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [TauCeti.SheafOfModules.IsInvertible M] : TauCeti.SheafOfModules.IsInvertible M.dual

The dual of an invertible sheaf of modules is invertible.

instance SheafOfModules.isIso_evaluation_dual_of_isInvertible {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [TauCeti.SheafOfModules.IsInvertible M] : CategoryTheory.IsIso ((CategoryTheory.ihom.ev M).app (unit (TauCeti.SheafOfModules.ringCatSheaf R)))

Evaluation of an invertible sheaf against its internal-Hom dual is an isomorphism.