Dual compatibility of the affine vector-bundle equivalence

The equivalence between finite projective R-modules and finite locally free sheaves on Spec R identifies the linear dual of a module with the internal-Hom dual of its associated sheaf. The comparison is the canonical internal-Hom comparison of the strong monoidal associated-sheaf functor, after identifying linear duals with module internal Homs.

Its component formula is exposed, and the comparison is contravariantly natural in the finite projective module. Together with the tensor compatibility of FiniteLocallyFreeSheaf.finiteProjectiveEquiv, this completes the affine comparison of tensor products and duals.

The construction uses Mathlib's ModuleCat.homLinearEquiv and the internal-Hom comparison for strong monoidal functors.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 (b).

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivDualIso (R : CommRingCat) (M : (finiteProjectiveModules ↑R).FullSubcategory) : (finiteProjectiveEquiv R).functor.obj (FiniteProjectiveModules.dual (↑R) M) ≅ ((finiteProjectiveEquiv R).functor.obj M).dual

The associated sheaf of the linear dual of a finite projective module is canonically isomorphic to the internal-Hom dual of its associated finite locally free sheaf.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivDualIso_hom_hom (R : CommRingCat) (M : (finiteProjectiveModules ↑R).FullSubcategory) : (finiteProjectiveEquivDualIso R M).hom.hom = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.tilde.functor R).map ModuleCat.homLinearEquiv.toModuleIso.inv) (CategoryTheory.CategoryStruct.comp (((AlgebraicGeometry.tilde.functor R).ihomComparison M.obj).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat ↑R))) ((CategoryTheory.ihom ((AlgebraicGeometry.tilde.functor R).obj M.obj)).map (CategoryTheory.Functor.OplaxMonoidal.η (AlgebraicGeometry.tilde.functor R))))

The underlying sheaf isomorphism comparing affine linear duals is the internal-Hom comparison, preceded by the standard identification of a linear dual with a module internal Hom and followed by the tensor-unit comparison.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivDualIso_naturality (R : CommRingCat) {M N : (finiteProjectiveModules ↑R).FullSubcategory} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.tilde.functor R).map (ModuleCat.ofHom (ModuleCat.Hom.hom f.hom).dualMap)) (finiteProjectiveEquivDualIso R M).hom.hom = CategoryTheory.CategoryStruct.comp (finiteProjectiveEquivDualIso R N).hom.hom ((CategoryTheory.MonoidalClosed.pre ((AlgebraicGeometry.tilde.functor R).map f.hom)).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgebraicGeometry.Spec R).Modules))

The affine dual comparison is contravariantly natural in the finite projective module.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivDualIso_naturality_assoc (R : CommRingCat) {M N : (finiteProjectiveModules ↑R).FullSubcategory} (f : M ⟶ N) {Z : (AlgebraicGeometry.Spec R).Modules} (h : ((finiteProjectiveEquiv R).functor.obj M).obj ⟹ CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgebraicGeometry.Spec R).Modules ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.tilde.functor R).map (ModuleCat.ofHom (ModuleCat.Hom.hom f.hom).dualMap)) (finiteProjectiveEquivDualIso R M).hom.hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (finiteProjectiveEquivDualIso R N).hom.hom ((CategoryTheory.MonoidalClosed.pre ((AlgebraicGeometry.tilde.functor R).map f.hom)).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgebraicGeometry.Spec R).Modules))) h

The affine dual comparison is contravariantly natural in the finite projective module.