The relative Picard fppf sheaf

For a morphism of schemes f : X ⟶ S, the relative Picard presheaf sends an S-scheme T to Pic(X_T) / Pic(T). The relative Picard functor is its associated sheaf for the fppf topology on schemes over S.

This file constructs that sheaf and records its universal property. It makes no representability claim: constructing a scheme that represents the sheaf, and identifying its degree-zero component, require additional geometric input.

Main declarations

• TauCeti.AlgebraicGeometry.relativePicardAddPresheaf: the relative Picard presheaf written as an additive commutative group;
• TauCeti.AlgebraicGeometry.relativePicardAddPresheafMk: the canonical section represented by a line-bundle class;
• TauCeti.AlgebraicGeometry.relativePicardFppfSheaf: its fppf sheafification;
• TauCeti.AlgebraicGeometry.relativePicardToFppfSheaf: the canonical map from T ↦ Pic(X_T) / Pic(T) to the relative Picard fppf sheaf;
• TauCeti.AlgebraicGeometry.relativePicardFppfSheafHomEquiv: the universal property of the sheafification.

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.relativePicardAddPresheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ AddCommGrpCat

The relative Picard presheaf, transported from multiplicative to additive notation. This changes only the presentation of the abelian group law: addition is tensor product of line-bundle classes.

theorem TauCeti.AlgebraicGeometry.relativePicardAddPresheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : relativePicardAddPresheaf f = (relativePicardPresheaf f).comp CommGrpCat.toAddCommGrp

The additive relative Picard presheaf is obtained from the multiplicative one by the equivalence between commutative groups and additive commutative groups.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardAddPresheafMk {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (T : (CategoryTheory.Over S)ᵒᵖ) (a : LineBundleClass (CategoryTheory.Limits.pullback (Opposite.unop T).hom f)) : ↑((relativePicardAddPresheaf f).obj T)

The section of the additive relative Picard presheaf represented by a line-bundle class.

theorem TauCeti.AlgebraicGeometry.relativePicardAddPresheafMk_surjective {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (T : (CategoryTheory.Over S)ᵒᵖ) : Function.Surjective (relativePicardAddPresheafMk f T)

Every section of the additive relative Picard presheaf is represented by a line-bundle class.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardAddPresheaf_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 ((relativePicardAddPresheaf f).map φ)) (relativePicardAddPresheafMk f T a) = relativePicardAddPresheafMk f T' (LineBundleClass.pullback (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ.unop)) a)

Pulling back a represented section of the additive relative Picard presheaf pulls back its line-bundle class.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardFppfSheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat

The relative Picard fppf sheaf of f : X ⟶ S, obtained by sheafifying the presheaf T ↦ Pic(X_T) / Pic(T) on the fppf site of schemes over S.

This definition does not assert that the resulting sheaf is representable.

theorem TauCeti.AlgebraicGeometry.relativePicardFppfSheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : relativePicardFppfSheaf f = (CategoryTheory.presheafToSheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat).obj (relativePicardAddPresheaf f)

The relative Picard fppf sheaf is obtained by applying the fppf sheafification functor to the additive relative Picard presheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardFppfSheaf_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : (relativePicardFppfSheaf f).obj = CategoryTheory.sheafify (AlgebraicGeometry.Scheme.fppfTopology.over S) (relativePicardAddPresheaf f)

The underlying presheaf of the relative Picard fppf sheaf is the sheafification of relativePicardPresheaf f.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardToFppfSheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : relativePicardAddPresheaf f ⟶ (relativePicardFppfSheaf f).obj

The canonical map from the relative Picard presheaf to its fppf sheafification.

theorem TauCeti.AlgebraicGeometry.relativePicardToFppfSheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) : relativePicardToFppfSheaf f = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify (AlgebraicGeometry.Scheme.fppfTopology.over S) (relativePicardAddPresheaf f)) (CategoryTheory.eqToHom ⋯)

The canonical map to the relative Picard fppf sheaf is the unit of fppf sheafification.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardFppfSheafHomEquiv {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (F : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat) : (relativePicardFppfSheaf f ⟶ F) ≃ (relativePicardAddPresheaf f ⟶ F.obj)

Universal property of the relative Picard fppf sheaf. Maps from the sheafification to an fppf sheaf F are naturally equivalent to maps from the relative Picard presheaf to the underlying presheaf of F.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardFppfSheafHomEquiv_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (F : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat) (g : relativePicardFppfSheaf f ⟶ F) : (relativePicardFppfSheafHomEquiv f F) g = CategoryTheory.CategoryStruct.comp (relativePicardToFppfSheaf f) g.hom

The universal-property equivalence restricts a sheaf morphism along the canonical map from the relative Picard presheaf.