Duality for sheaves of modules on a scheme

The self-duality of a finite free sheaf of modules specializes to the symmetric monoidal category X.Modules on a scheme. This is the local model for duality of finite locally free sheaves. Gluing these local dualities, the dual-tensor comparison 𝓗om(M, 𝒪_X) ⊗ N ⟶ 𝓗om(M, N) of a locally free 𝒪_X-module of finite type is an isomorphism, so 𝓗om(M, 𝒪_X) is a left dual of M by TauCeti.exactPairingOfIsIsoDualTensorIhom.

Main declarations

• AlgebraicGeometry.Scheme.Modules.exactPairingFree: a finite free 𝒪_X-module is self-dual;
• AlgebraicGeometry.Scheme.Modules.isIso_dualTensorIhom_of_isLocallyFree: the dual-tensor comparison of a locally free 𝒪_X-module of finite type is an isomorphism.

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.monoidalCategorySheafOfModules (X : AlgebraicGeometry.Scheme) : CategoryTheory.MonoidalCategory (SheafOfModules X.ringCatSheaf)

The monoidal structure of X.Modules, stated for the unfolded type SheafOfModules X.ringCatSheaf, which typeclass search does not see through the definition of Scheme.Modules.

Equations

• TauCeti.AlgebraicGeometry.monoidalCategorySheafOfModules X = AlgebraicGeometry.Scheme.Modules.instMonoidalCategory X

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.exactPairingFree (X : Scheme) (I : Type u) [Finite I] : CategoryTheory.ExactPairing (SheafOfModules.free I) (SheafOfModules.free I)

The free 𝒪_X-module on a finite type is self-dual.

Equations

• AlgebraicGeometry.Scheme.Modules.exactPairingFree X I = TauCeti.SheafOfModules.exactPairingFree I

instance AlgebraicGeometry.Scheme.Modules.isIso_dualTensorIhom_of_isLocallyFree {X : Scheme} (M : X.Modules) [SheafOfModules.IsLocallyFree M] [SheafOfModules.IsFiniteType M] : CategoryTheory.IsIso (TauCeti.dualTensorIhom M)

The dual-tensor comparison 𝓗om(M, 𝒪_X) ⊗ N ⟶ 𝓗om(M, N) of a locally free 𝒪_X-module of finite type is an isomorphism.