Pullback of internal Hom from a finite locally free sheaf

For a finite locally free sheaf E and an arbitrary sheaf of modules F on Y, the canonical comparison f* 𝓗om(E, F) ⟶ 𝓗om(f* E, f* F) is an isomorphism for every scheme morphism f : X ⟶ Y. No flatness assumption on f or finiteness assumption on F is needed.

The comparison for quasicoherent sources and its evaluation and curry equations are defined in TauCeti.AlgebraicGeometry.Modules.Pullback.InternalHom.Basic. This module specializes its exact-pairing invertibility criterion to the internal-Hom dual of a finite locally free sheaf.

References

• The Stacks Project, Tag 0C6I (base change for sheaf Hom).

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instExactPairingModulesObjIsFiniteLocallyFreeDual {Y : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf Y) : CategoryTheory.ExactPairing E.dual.obj E.obj

The internal-Hom dual of E forms an exact pairing with E in sheaves of modules.

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isIso_pullbackIhomComparison {X Y : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf Y) (f : X ⟶ Y) : CategoryTheory.IsIso (pullbackIhomComparison E.obj f)

The canonical internal-Hom base-change comparison is invertible for a finite locally free source and an arbitrary target sheaf of modules.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackIhomIso {X Y : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf Y) (f : X ⟶ Y) : (CategoryTheory.ihom E.obj).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ≅ (AlgebraicGeometry.Scheme.Modules.pullback f).comp (CategoryTheory.ihom ((AlgebraicGeometry.Scheme.Modules.pullback f).obj E.obj))

Arbitrary pullback commutes with internal Hom from a finite locally free sheaf, naturally in every target sheaf of modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackIhomIso_hom {X Y : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf Y) (f : X ⟶ Y) : (E.pullbackIhomIso f).hom = pullbackIhomComparison E.obj f

The forward map of the base-change isomorphism is the canonical comparison.