Internal Hom from a finite locally free sheaf in quasicoherent sheaves

For a finite locally free sheaf E on a scheme X, the ordinary sheaf internal Hom 𝓗om(E, -) preserves quasicoherence and is right adjoint to tensoring with E inside QuasicoherentSheaf X. It is naturally isomorphic to tensoring with the internal-Hom dual 𝓗om(E, 𝒪_X). Evaluation and coevaluation are those of the ambient tensor--Hom adjunction; the target sheaf is arbitrary quasicoherent, without a finiteness hypothesis.

The adjunction is restricted using Mathlib's Adjunction.restrictFullyFaithful. The dual-tensor isomorphism lifts TauCeti.dualTensorIhom, retaining its canonical evaluation equation.

When the target is also finite locally free, so is 𝓗om(E, F). Hence FiniteLocallyFreeSheaf X is itself closed monoidal, with internal Homs, evaluation and precomposition computed in X.Modules (CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory); its internal Hom into 𝒪_X is the dual FiniteLocallyFreeSheaf.dual E.

instance AlgebraicGeometry.Scheme.Modules.isMonoidalClosed_isFiniteLocallyFree (X : Scheme) : (isFiniteLocallyFree X).IsMonoidalClosed

Finite locally free sheaves are closed under internal Hom in X.Modules. With this instance, FiniteLocallyFreeSheaf X is closed monoidal, with internal Homs computed in X.Modules.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.ihom_obj_unit_eq_dual {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : (E ⟹ CategoryTheory.MonoidalCategoryStruct.tensorUnit (FiniteLocallyFreeSheaf X)) = E.dual

The internal Hom from E into the structure sheaf in FiniteLocallyFreeSheaf X is the dual 𝓗om(E, 𝒪_X).

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.internalHom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.Functor (QuasicoherentSheaf X) (QuasicoherentSheaf X)

Internal Hom from E, restricted to quasicoherent target sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.internalHom_obj_obj {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : (E.internalHom.obj F).obj = (E.obj ⟹ F.obj)

The underlying sheaf of the quasicoherent internal Hom is the ordinary sheaf internal Hom.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.internalHom_map_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) {F G : QuasicoherentSheaf X} (f : F ⟶ G) : (E.internalHom.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom E.obj).map f.hom) (CategoryTheory.eqToHom ⋯))

The internal-Hom functor acts by the ordinary sheaf internal-Hom map.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.tensorInternalHomAdjunction {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.MonoidalCategory.tensorLeft ((toQuasicoherent X).obj E) ⊣ E.internalHom

Tensoring with E is left adjoint to the ordinary internal Hom from E, within quasicoherent sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.tensorInternalHomAdjunction_counit_app_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : (E.tensorInternalHomAdjunction.counit.app F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft E.obj (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ihom.ev E.obj).app F.obj)

Evaluation of the restricted tensor--Hom adjunction is ordinary internal-Hom evaluation.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.tensorInternalHomAdjunction_unit_app_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : (E.tensorInternalHomAdjunction.unit.app F).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev E.obj).app F.obj) (CategoryTheory.eqToHom ⋯)

Coevaluation of the restricted adjunction is ordinary tensor--Hom coevaluation.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.closedToQuasicoherent {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.Closed ((toQuasicoherent X).obj E)

A finite locally free sheaf is closed in the quasicoherent category, with right adjoint its ordinary sheaf internal Hom.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.ihom_toQuasicoherent {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.ihom ((toQuasicoherent X).obj E) = E.internalHom

The chosen internal Hom in the quasicoherent category is ordinary sheaf internal Hom.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.ihom_ev_toQuasicoherent_app_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : ((CategoryTheory.ihom.ev ((toQuasicoherent X).obj E)).app F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft E.obj (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ihom.ev E.obj).app F.obj)

Evaluation in the quasicoherent category is ordinary sheaf evaluation.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsIsoFunctorModulesDualTensorIhomObjIsFiniteLocallyFree {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.IsIso (dualTensorIhom E.obj)

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualTensorInternalHomIso {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.MonoidalCategory.tensorLeft ((toQuasicoherent X).obj E.dual) ≅ E.internalHom

Tensoring with the internal-Hom dual of E is naturally isomorphic to internal Hom from E, on arbitrary quasicoherent target sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualTensorInternalHomIso_hom_app_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : (E.dualTensorInternalHomIso.hom.app F).hom = CategoryTheory.CategoryStruct.comp ((dualTensorIhom E.obj).app F.obj) (CategoryTheory.eqToHom ⋯)

The dual-tensor isomorphism is the canonical comparison on underlying sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualTensorInternalHomIso_inv_app_hom {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (F : QuasicoherentSheaf X) : (E.dualTensorInternalHomIso.inv.app F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((CategoryTheory.asIso (dualTensorIhom E.obj)).inv.app F.obj)

The inverse dual-tensor isomorphism inverts the canonical comparison.