The relative Picard presheaf and the rigidified Picard functor

Let f : X ⟶ S be a morphism of schemes. The relative Picard presheaf of f sends a scheme T over S to the quotient Pic(X_T) / Pic(T) of the Picard group of the base change X_T = T ×_S X by the line-bundle classes pulled back from T, and a morphism T' ⟶ T over S to pullback along the induced morphism X_{T'} ⟶ X_T. The relative Picard functor Pic_{X/S} is its sheafification for the fppf (or étale) topology.

When f has a section x₀, the presheaf T ↦ Pic(X_T) / Pic(T) is already the rigidified Picard functor: forgetting the rigidification is a natural bijection from the classes of line bundles on X_T rigidified along the base-changed section x₀_T onto Pic(X_T) / Pic(T). Pointwise this is a statement about any section s of a morphism p : Y ⟶ T: forgetting the rigidification is injective on classes rigidified along s, with image the kernel of s^* : Pic(Y) → Pic(T), and p^* splits s^*, so that this kernel maps isomorphically onto Pic(Y) / p^* Pic(T) (TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk_toLineBundleClass_bijective). No hypothesis on f beyond the existence of the section is needed.

Main declarations

• TauCeti.AlgebraicGeometry.relativePicardPresheaf: the presheaf of commutative groups T ↦ Pic(X_T) / Pic(T) on schemes over S;
• TauCeti.AlgebraicGeometry.rigidifiedPicardFunctorIso: the rigidified Picard functor of (X, x₀) is naturally isomorphic to the underlying presheaf of sets of the relative Picard presheaf.

References

• S. Bosch, W. Lütkebohmert, M. Raynaud, Néron Models, Section 8.1.
• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.2.

theorem TauCeti.AlgebraicGeometry.range_pullbackHom_fst_le_comap {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T' T : CategoryTheory.Over S} (φ : T' ⟶ T) : (LineBundleClass.pullbackHom (CategoryTheory.Limits.pullback.fst T.hom f)).range ≤ Subgroup.comap (LineBundleClass.pullbackHom (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ))) (LineBundleClass.pullbackHom (CategoryTheory.Limits.pullback.fst T'.hom f)).range

Pullback along the morphism X_{T'} ⟶ X_T induced by φ : T' ⟶ T over S carries the line-bundle classes pulled back from T to line-bundle classes pulled back from T'.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardPresheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ CommGrpCat

The relative Picard presheaf of a morphism f : X ⟶ S: it sends a scheme T over S to the quotient Pic(X_T) / Pic(T) of the Picard group of X_T = T ×_S X by the classes pulled back along the projection X_T ⟶ T, and a morphism over S to pullback along the induced morphism of base changes.

Equations

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

theorem TauCeti.AlgebraicGeometry.relativePicardPresheaf_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (T : (CategoryTheory.Over S)ᵒᵖ) : (relativePicardPresheaf f).obj T = ↧(LineBundleClass (CategoryTheory.Limits.pullback (Opposite.unop T).hom f) ⧸ (LineBundleClass.pullbackHom (CategoryTheory.Limits.pullback.fst (Opposite.unop T).hom f)).range)

The value of the relative Picard presheaf at T is Pic(X_T) / Pic(T).

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardPresheaf_map_mk {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (a : LineBundleClass (CategoryTheory.Limits.pullback (Opposite.unop T).hom f)) : (CategoryTheory.ConcreteCategory.hom ((relativePicardPresheaf f).map φ)) ↑a = ↑(LineBundleClass.pullback (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ.unop)) a)

The relative Picard presheaf acts on the image of a line-bundle class on X_T by pulling it back along the induced morphism of base changes.

noncomputable def TauCeti.AlgebraicGeometry.rigidifiedPicardFunctorIso {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) : rigidifiedPicardFunctor f x₀ hx₀ ≅ (relativePicardPresheaf f).comp (CategoryTheory.forget CommGrpCat)

The rigidified Picard functor is the relative Picard presheaf. For a morphism f : X ⟶ S with a section x₀, forgetting the rigidification identifies the classes of line bundles on X_T rigidified along x₀_T with Pic(X_T) / Pic(T), naturally in the scheme T over S.

Equations

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

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardFunctorIso_hom_app {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) (a : (rigidifiedPicardFunctor f x₀ hx₀).obj T) : (CategoryTheory.ConcreteCategory.hom ((rigidifiedPicardFunctorIso f x₀ hx₀).hom.app T)) a = ↑(RigidifiedLineBundleClass.toLineBundleClass a)

The comparison rigidifiedPicardFunctorIso sends the class of a rigidified line bundle to the image of its underlying line-bundle class.