Functorial pullback of line bundles

Pulling back an invertible sheaf along an identity morphism leaves it unchanged, and pullback along a composite agrees with successive pullback. These comparisons make the pullback operation on isomorphism classes of line bundles contravariantly functorial. Pullback also preserves the class of the trivial line bundle (LineBundleClass.pullback_one), through the comparison Scheme.Modules.pullbackObjUnitIso : f^* 𝒪_Y ≅ 𝒪_X, and tensor products of line bundles (LineBundleClass.pullback_mul), through the tensor comparison f^*(L ⊗ K) ≅ f^*L ⊗ f^*K, which is invertible because line bundles are quasicoherent (Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent). So pullback is a homomorphism of Picard groups (LineBundleClass.pullbackHom), as needed for the Picard functor T ↦ Pic(X_T).

The comparisons are restrictions of Mathlib's Scheme.Modules.pullbackId and Scheme.Modules.pullbackComp.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.pullbackId (X : AlgebraicGeometry.Scheme) : pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (InvertibleSheaf X)

Pullback of a line bundle along the identity morphism is naturally isomorphic to the original line bundle.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.pullbackComp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

Pullback along a composite is naturally isomorphic to successive pullback of line bundles.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (a : LineBundleClass Y) : LineBundleClass X

Pullback of an isomorphism class of line bundles along a scheme morphism. It is a group homomorphism by LineBundleClass.pullback_mul, bundled as LineBundleClass.pullbackHom.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullback_mk {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (L : InvertibleSheaf Y) : pullback f (mk L) = mk ((InvertibleSheaf.pullback f).obj L)

Pulling back the class of L gives the class of its pulled-back line bundle.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullback_id {X : AlgebraicGeometry.Scheme} (a : LineBundleClass X) : pullback (CategoryTheory.CategoryStruct.id X) a = a

Pullback by the identity acts identically on line-bundle classes.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullback_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (a : LineBundleClass Z) : pullback f (pullback g a) = pullback (CategoryTheory.CategoryStruct.comp f g) a

Pullback of line-bundle classes is contravariantly functorial under composition.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullback_one {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : pullback f 1 = 1

Pullback preserves the class of the trivial line bundle.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullback_mul {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (a b : LineBundleClass Y) : pullback f (a * b) = pullback f a * pullback f b

Pullback of line-bundle classes is compatible with tensor product: [f^*(L ⊗ K)] = [f^*L] [f^*K].

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.pullbackHom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : LineBundleClass Y →* LineBundleClass X

Pullback of line-bundle classes along a scheme morphism, as a homomorphism of Picard groups.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.pullbackHom f = MonoidHom.mk' (TauCeti.AlgebraicGeometry.LineBundleClass.pullback f) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullbackHom_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (a : LineBundleClass Y) : (pullbackHom f) a = pullback f a

The Picard group homomorphism pullbackHom f is pullback of line-bundle classes.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullbackHom_id (X : AlgebraicGeometry.Scheme) : pullbackHom (CategoryTheory.CategoryStruct.id X) = MonoidHom.id (LineBundleClass X)

Pullback of Picard groups along the identity is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.pullbackHom_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (pullbackHom f).comp (pullbackHom g) = pullbackHom (CategoryTheory.CategoryStruct.comp f g)

Pullback of Picard groups is contravariantly functorial under composition.