Pullback of line bundles

Let f : X ⟶ Y be a morphism of schemes. The inverse image f^* L of a line bundle L on Y is a line bundle on X, giving a pullback functor on line bundles. The generic restriction compatibility used to establish this result is provided by TauCeti.AlgebraicGeometry.Modules.Pullback.Basic.

Main declarations

• TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible_pullback: the pullback of an invertible sheaf is invertible;
• TauCeti.AlgebraicGeometry.InvertibleSheaf.pullback: the pullback functor on line bundles.

References

• R. Hartshorne, Algebraic Geometry, Section II.5 and Section II.6 (the Picard group).
• The Stacks Project, Sheaves of Modules, section Invertible modules.

instance TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible_pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (M : Y.Modules) [hM : isInvertible Y M] : isInvertible X ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)

The pullback of an invertible sheaf along a morphism of schemes is invertible.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Functor (InvertibleSheaf Y) (InvertibleSheaf X)

The pullback of line bundles along a morphism of schemes f : X ⟶ Y, as a functor from line bundles on Y to line bundles on X.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.pullback_obj_obj {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (L : InvertibleSheaf Y) : ((pullback f).obj L).obj = (AlgebraicGeometry.Scheme.Modules.pullback f).obj L.obj

The underlying sheaf of the pullback of a line bundle is its pullback as a sheaf of modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.pullback_map {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {L K : InvertibleSheaf Y} (φ : L ⟶ K) : ((pullback f).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map φ.hom) (CategoryTheory.eqToHom ⋯))

Pullback acts on a morphism of line bundles by the underlying module pullback.