Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Dual.Basic

Duals of finite locally free sheaves #

A finite locally free sheaf E on a scheme X is dualizable, with left dual its internal Hom 𝓗om(E, 𝒪_X) into the structure sheaf. The evaluation E ⊗ 𝓗om(E, 𝒪_X) ⟶ 𝒪_X is the evaluation of the internal Hom, and the coevaluation is the preimage of the identity of E under the dual-tensor comparison 𝓗om(E, 𝒪_X) ⊗ E ⟶ 𝓗om(E, E), which is invertible because E is finite locally free (AlgebraicGeometry.Scheme.Modules.isIso_dualTensorIhom_of_isLocallyFree).

Consequently the symmetric monoidal category FiniteLocallyFreeSheaf X is rigid, and a quasicoherent sheaf whose underlying module is finite locally free has the left dual 𝓗om(E, 𝒪_X) in the symmetric monoidal category QuasicoherentSheaf X.

Main declarations #

source
@[reducible, inline]
noncomputable abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dual {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
FiniteLocallyFreeSheaf X

The dual 𝓗om(E, 𝒪_X) of a finite locally free sheaf E: the internal Hom from E into the structure sheaf, which is again finite locally free.

This is an abbreviation so that instance search sees its underlying internal Hom, and hence the exact pairing of that sheaf with E.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dual_obj {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    E.dual.obj = (E.obj ⟹ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

    The underlying sheaf of the dual of E is the internal Hom from E into 𝒪_X.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exactPairingDual {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    CategoryTheory.ExactPairing E.dual E

    A finite locally free sheaf E has left dual 𝓗om(E, 𝒪_X). The evaluation is the evaluation of the internal Hom, and the coevaluation is the preimage of the identity of E under the invertible dual-tensor comparison.

    Equations
    source
    @[instance_reducible]
    noncomputable instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rigidCategory {X : AlgebraicGeometry.Scheme} :
    CategoryTheory.RigidCategory (FiniteLocallyFreeSheaf X)

    Finite locally free sheaves form a rigid category: the left and right duals of E are both 𝓗om(E, 𝒪_X), the right duality obtained from the left one through the symmetry.

    Equations
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.leftDual_eq_dual {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    ᘁE = E.dual

    The chosen left dual of a finite locally free sheaf is its dual 𝓗om(E, 𝒪_X).

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rightDual_eq_dual {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    Eᘁ = E.dual

    The chosen right dual of a finite locally free sheaf is its dual 𝓗om(E, 𝒪_X).

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evaluation_leftDual_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    (ε_ (ᘁE) E).hom = (CategoryTheory.ihom.ev E.obj).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

    The evaluation E ⊗ ᘁE ⟶ 𝒪_X of the rigid structure is the evaluation of the internal Hom 𝓗om(E, 𝒪_X).

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.coevaluation_leftDual_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    (η_ (ᘁE) E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.id E.obj) (CategoryTheory.inv ((dualTensorIhom E.obj).app E.obj))

    The coevaluation 𝒪_X ⟶ ᘁE ⊗ E of the rigid structure is the preimage of the identity of E under the dual-tensor comparison 𝓗om(E, 𝒪_X) ⊗ E ⟶ 𝓗om(E, E).

    source
    theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_of_isFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : QuasicoherentSheaf X) (hE : AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X E.obj) :
    Nonempty (CategoryTheory.HasLeftDual E)

    A quasicoherent sheaf whose underlying module is finite locally free has a left dual in the symmetric monoidal category QuasicoherentSheaf X, namely 𝓗om(E, 𝒪_X) with the exact pairing of TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exactPairingDual.