Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Dual.Bidual

Functorial duality and biduality of finite locally free sheaves #

Internal Hom into the structure sheaf gives a contravariant endofunctor on finite locally free sheaves. Its action on morphisms is precomposition, not an arbitrary choice of categorical dual. The canonical map to the double dual is a natural isomorphism. It is the existing TauCeti.doubleDualMap, whose evaluation equation pairs a local functional with the original section. Thus dualization loses no information about the sheaf or its morphisms.

The functor and natural isomorphism follow the finite-projective module formalization in TauCeti.Algebra.Category.ModuleCat.FiniteProjective.Monoidal as their template.

The construction lifts Mathlib's MonoidalClosed.internalHom, evaluated at the structure sheaf, using ObjectProperty.lift. Biduality uses TauCeti.doubleDualMap; invertibility follows from the exact pairing with the internal-Hom dual.

source
noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualFunctor {X : AlgebraicGeometry.Scheme} :
CategoryTheory.Functor (FiniteLocallyFreeSheaf X)ᵒᵖ (FiniteLocallyFreeSheaf X)

Internal-Hom dualization of finite locally free sheaves, acting on morphisms by precomposition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualFunctor_obj {X : AlgebraicGeometry.Scheme} (E : (FiniteLocallyFreeSheaf X)ᵒᵖ) :
    dualFunctor.obj E = (Opposite.unop E).dual

    The object assigned by dualization is the internal-Hom dual.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualFunctor_map_hom {X : AlgebraicGeometry.Scheme} {E F : (FiniteLocallyFreeSheaf X)ᵒᵖ} (f : E ⟶ F) :
    (dualFunctor.map f).hom = (CategoryTheory.MonoidalClosed.pre f.unop.hom).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

    Dualization acts on the underlying module morphism by precomposition.

    source
    noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalIso {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
    E ≅ E.dual.dual

    A finite locally free sheaf is canonically isomorphic to its internal-Hom double dual. The forward map is the transpose of evaluation, with the functional on the left.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalIso_hom_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
      E.evalIso.hom.hom = doubleDualMap E.obj

      The bidual isomorphism uses the canonical double-dual map of the underlying sheaf.

      source
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalIso_naturality {X : AlgebraicGeometry.Scheme} {E F : FiniteLocallyFreeSheaf X} (f : E ⟶ F) :
      CategoryTheory.CategoryStruct.comp f F.evalIso.hom = CategoryTheory.CategoryStruct.comp E.evalIso.hom (dualFunctor.map (dualFunctor.map f.op).op)

      Double-dual evaluation is natural in maps of finite locally free sheaves.

      source
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalIso_naturality_assoc {X : AlgebraicGeometry.Scheme} {E F : FiniteLocallyFreeSheaf X} (f : E ⟶ F) {Z : FiniteLocallyFreeSheaf X} (h : F.dual.dual ⟶ Z) :
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp F.evalIso.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp E.evalIso.hom (dualFunctor.map (dualFunctor.map f.op).op)) h

      Double-dual evaluation is natural in maps of finite locally free sheaves.

      source
      noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso {X : AlgebraicGeometry.Scheme} :
      CategoryTheory.Functor.id (FiniteLocallyFreeSheaf X) ≅ dualFunctor.rightOp.comp dualFunctor

      The identity functor on finite locally free sheaves is naturally isomorphic to internal-Hom dualization applied twice.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso_hom_app {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
        evalNatIso.hom.app E = E.evalIso.hom

        The forward component of the bidual natural isomorphism is canonical evaluation.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso_inv_app {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) :
        evalNatIso.inv.app E = E.evalIso.inv

        The inverse component of the bidual natural isomorphism is inverse evaluation.