Pullback of dual vector bundles

For a finite locally free sheaf E, pulling back its dual agrees with taking the dual of its pullback. The comparison uses the canonical base-change map for internal Hom and the canonical identification of the pullback of the structure sheaf with the structure sheaf. The comparison is natural in E, so it assembles into a natural isomorphism between dualizing then pulling back and pulling back then dualizing. It is also coherent: along the identity it is the identity comparison of pullback, and along a composite f ≫ g it is the comparison along g followed by the comparison along f, through the composition comparison of pullback (pullbackDualIso_hom_id and pullbackDualIso_hom_comp).

References

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

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) : (pullback f).obj E.dual ≅ ((pullback f).obj E).dual

Pulling back a finite locally free sheaf's dual is canonically isomorphic to the dual of its pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_hom_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) : (pullbackDualIso f E).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackIhomComparison E.obj f).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit Y.Modules)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom ((AlgebraicGeometry.Scheme.Modules.pullback f).obj E.obj)).map (AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso f).hom) (CategoryTheory.eqToHom ⋯)))

The underlying map is the canonical internal-Hom base-change comparison, followed by the identification f* 𝒪_Y ≅ 𝒪_X.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_naturality {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {E F : FiniteLocallyFreeSheaf Y} (g : E ⟶ F) : CategoryTheory.CategoryStruct.comp ((pullback f).map (dualFunctor.map g.op)) (pullbackDualIso f E).hom = CategoryTheory.CategoryStruct.comp (pullbackDualIso f F).hom (dualFunctor.map ((pullback f).map g).op)

The dual pullback comparison is natural in maps of finite locally free sheaves.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_naturality_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {E F : FiniteLocallyFreeSheaf Y} (g : E ⟶ F) {Z : FiniteLocallyFreeSheaf X} (h : ((pullback f).obj E).dual ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((pullback f).map (dualFunctor.map g.op)) (pullbackDualIso f E).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (pullbackDualIso f F).hom (dualFunctor.map ((pullback f).map g).op)) h

The dual pullback comparison is natural in maps of finite locally free sheaves.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualNatIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : dualFunctor.comp (pullback f) ≅ (pullback f).op.comp dualFunctor

Pulling back duals of finite locally free sheaves is naturally isomorphic to dualizing their pullbacks.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualNatIso_hom_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : (FiniteLocallyFreeSheaf Y)ᵒᵖ) : (pullbackDualNatIso f).hom.app E = (pullbackDualIso f (Opposite.unop E)).hom

The forward component of the natural dual pullback comparison is pullbackDualIso.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualNatIso_inv_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : (FiniteLocallyFreeSheaf Y)ᵒᵖ) : (pullbackDualNatIso f).inv.app E = (pullbackDualIso f (Opposite.unop E)).inv

The inverse component of the natural dual pullback comparison is pullbackDualIso.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_hom_id {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : CategoryTheory.CategoryStruct.comp (pullbackDualIso (CategoryTheory.CategoryStruct.id X) E).hom (dualFunctor.map ((pullbackId X).inv.app E).op) = (pullbackId X).hom.app E.dual

Along the identity, the dual pullback comparison is the identity comparison of pullback: composed with the dual of the inverse identity comparison of E, it is the identity comparison of dual E.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_hom_id_assoc {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) {Z : FiniteLocallyFreeSheaf X} (h : dualFunctor.obj (Opposite.op E) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (pullbackDualIso (CategoryTheory.CategoryStruct.id X) E).hom (dualFunctor.map ((pullbackId X).inv.app E).op)) h = CategoryTheory.CategoryStruct.comp ((pullbackId X).hom.app E.dual) h

Along the identity, the dual pullback comparison is the identity comparison of pullback: composed with the dual of the inverse identity comparison of E, it is the identity comparison of dual E.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_hom_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : FiniteLocallyFreeSheaf Z) : CategoryTheory.CategoryStruct.comp (pullbackDualIso (CategoryTheory.CategoryStruct.comp f g) E).hom (dualFunctor.map ((pullbackComp f g).hom.app E).op) = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app E.dual) (CategoryTheory.CategoryStruct.comp ((pullback f).map (pullbackDualIso g E).hom) (pullbackDualIso f ((pullback g).obj E)).hom)

Along a composite f ≫ g, the dual pullback comparison is the comparison along g followed by the comparison along f: composed with the dual of the composition comparison of E, it is the inverse composition comparison of dual E followed by the pullback along f of the comparison along g and the comparison along f.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso_hom_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : FiniteLocallyFreeSheaf Z) {Z✝ : FiniteLocallyFreeSheaf X} (h : dualFunctor.obj (Opposite.op ((pullback f).obj ((pullback g).obj E))) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (pullbackDualIso (CategoryTheory.CategoryStruct.comp f g) E).hom (dualFunctor.map ((pullbackComp f g).hom.app E).op)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app E.dual) (CategoryTheory.CategoryStruct.comp ((pullback f).map (pullbackDualIso g E).hom) (pullbackDualIso f ((pullback g).obj E)).hom)) h

Along a composite f ≫ g, the dual pullback comparison is the comparison along g followed by the comparison along f: composed with the dual of the composition comparison of E, it is the inverse composition comparison of dual E followed by the pullback along f of the comparison along g and the comparison along f.