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.

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.

Equations

• E.internalHom = (SheafOfModules.isQuasicoherent X.ringCatSheaf).lift ((SheafOfModules.isQuasicoherent X.ringCatSheaf).ι.comp (CategoryTheory.ihom E.obj)) ⋯

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.