The rigidified Picard functor

Let f : X ⟶ S be a morphism of schemes with a section x₀ : S ⟶ X. For a scheme T over S, the base change X_T = T ×_S X of X has the section x₀_T : T ⟶ X_T induced by x₀. The rigidified Picard functor of (X, x₀) sends T to the set of isomorphism classes of line bundles on X_T rigidified along x₀_T: line bundles L on X_T together with a trivialization x₀_T^* L ≅ 𝒪_T, up to isomorphisms of line bundles respecting the trivializations. A morphism T' ⟶ T over S acts by pullback along the induced morphism X_{T'} ⟶ X_T.

The rigidification is how the section x₀ enters the construction of the Picard scheme: when f_* 𝒪_X = 𝒪_S holds universally, a rigidified line bundle has no automorphisms other than the identity, and for every section the rigidified functor is the relative Picard presheaf T ↦ Pic(X_T) / Pic(T). The first statement is the rigidity theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_iff of the separate module TauCeti.AlgebraicGeometry.LineBundle.Rigidified.Automorphisms, which this file does not import; it identifies the automorphisms of a rigidified line bundle with the kernel of the pullback of global units along the section. The second statement is TauCeti.AlgebraicGeometry.rigidifiedPicardFunctorIso of the module TauCeti.AlgebraicGeometry.PicardFunctor.Relative; this file constructs the functor.

Main declarations

• TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor: the rigidified Picard functor (Over S)ᵒᵖ ⥤ Type, with rigidifiedPicardFunctor_map computing its action on classes and rigidifiedPicardFunctor_map_mk on representatives.

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.

noncomputable def TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ (Type (u + 1))

The rigidified Picard functor of a morphism f : X ⟶ S with a section x₀: it sends a scheme T over S to the isomorphism classes of line bundles on X_T = T ×_S X rigidified along the base-changed section x₀_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.

@[simp]

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : (rigidifiedPicardFunctor f x₀ hx₀).obj T = RigidifiedLineBundleClass (baseChangeSection f x₀ hx₀ (Opposite.unop T))

The value of the rigidified Picard functor at T is the set of classes of line bundles on X_T rigidified along the base-changed section.

@[simp]

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor_map {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') : (rigidifiedPicardFunctor f x₀ hx₀).map φ = TypeCat.ofHom (RigidifiedLineBundleClass.pullback ⋯)

The rigidified Picard functor acts by pullback along the induced map of base changes.

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor_map_mk {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (P : RigidifiedLineBundle (baseChangeSection f x₀ hx₀ (Opposite.unop T))) : (CategoryTheory.ConcreteCategory.hom ((rigidifiedPicardFunctor f x₀ hx₀).map φ)) (RigidifiedLineBundleClass.mk P) = RigidifiedLineBundleClass.mk (RigidifiedLineBundle.pullback ⋯ P)

The rigidified Picard functor acts on the class of a rigidified line bundle by pulling it back along the induced morphism of base changes.