The degree-zero relative Picard fppf sheaf

For a smooth proper geometrically connected family of curves f : X ⟶ S, the degree-zero relative Picard presheaf consists of the line-bundle classes having degree zero on every geometric fibre. This file defines its fppf sheafification and embeds it into the relative Picard fppf sheaf.

The inclusion is a monomorphism: the degree-zero presheaf is a subgroup presheaf of the relative Picard presheaf, and sheafification of additive commutative groups preserves finite limits and hence monomorphisms. The resulting subsheaf is the functorial Pic⁰ used before representability. Identifying it with an open-and-closed identity component of a representing Picard scheme needs the geometric representability and local-constancy theorems and is not asserted here.

Main declarations

• TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheaf: the fppf sheafification of the degree-zero relative Picard presheaf;
• TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheaf: its sheafification map;
• TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheafOfMul: the same map on the underlying multiplicatively written degree-zero Picard functor;
• TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafι: the monomorphism from the degree-zero sheaf to the relative Picard fppf sheaf, compatible with the sheafification maps;
• TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafHomEquiv: the universal property of the degree-zero sheafification.

References

• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Sections 9.4--9.5.
• The Stacks Project, Tag 0B9R.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroAddPresheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ AddCommGrpCat

The degree-zero relative Picard presheaf, transported from multiplicative to additive notation before fppf sheafification.

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroAddPresheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroAddPresheaf f = (relativePicardDegreeZeroFunctor f).comp CommGrpCat.toAddCommGrp

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

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroAddPresheafAddEquiv {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] (T : (CategoryTheory.Over S)ᵒᵖ) : Additive ↑((relativePicardDegreeZeroFunctor f).obj T) ≃+ ↑((relativePicardDegreeZeroAddPresheaf f).obj T)

The sections of the additive degree-zero Picard presheaf are the additive presentation of the sections of the multiplicatively written degree-zero Picard functor.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroAddPresheaf_map_addEquiv_ofMul {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (c : ↑((relativePicardDegreeZeroFunctor f).obj T)) : (CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroAddPresheaf f).map φ)) ((relativePicardDegreeZeroAddPresheafAddEquiv f T) (Additive.ofMul c)) = (relativePicardDegreeZeroAddPresheafAddEquiv f T') (Additive.ofMul ((CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroFunctor f).map φ)) c))

Pullback of a section commutes with changing the degree-zero Picard functor from multiplicative to additive notation.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroAddPresheafι {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroAddPresheaf f ⟶ relativePicardAddPresheaf f

The inclusion of the additive degree-zero relative Picard presheaf into the additive relative Picard presheaf.

instance TauCeti.AlgebraicGeometry.instMonoFunctorOppositeOverSchemeAddCommGrpCatRelativePicardDegreeZeroAddPresheafι {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : CategoryTheory.Mono (relativePicardDegreeZeroAddPresheafι f)

The inclusion of the additive degree-zero relative Picard presheaf is a monomorphism.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat

The degree-zero relative Picard fppf sheaf of a smooth proper geometrically connected family of curves, obtained by sheafifying the presheaf of classes having degree zero on every geometric fibre.

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroFppfSheaf f = (CategoryTheory.presheafToSheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat).obj (relativePicardDegreeZeroAddPresheaf f)

The degree-zero relative Picard fppf sheaf is the fppf sheafification of the additive degree-zero presheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheaf_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : (relativePicardDegreeZeroFppfSheaf f).obj = CategoryTheory.sheafify (AlgebraicGeometry.Scheme.fppfTopology.over S) (relativePicardDegreeZeroAddPresheaf f)

The underlying presheaf of the degree-zero relative Picard fppf sheaf is the sheafification of the additive degree-zero presheaf.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheaf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroAddPresheaf f ⟶ (relativePicardDegreeZeroFppfSheaf f).obj

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

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheaf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroToFppfSheaf f = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify (AlgebraicGeometry.Scheme.fppfTopology.over S) (relativePicardDegreeZeroAddPresheaf f)) (CategoryTheory.eqToHom ⋯)

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

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheafOfMul {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : (relativePicardDegreeZeroFunctor f).comp (CategoryTheory.forget CommGrpCat) ⟶ (relativePicardDegreeZeroFppfSheaf f).obj.comp (CategoryTheory.forget AddCommGrpCat)

The canonical map from the multiplicatively written degree-zero Picard presheaf to the underlying presheaf of sets of its additive fppf sheafification. It sends a section c to the sheafification image of Additive.ofMul c.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheafOfMul_app_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {T : (CategoryTheory.Over S)ᵒᵖ} (c : ↑((relativePicardDegreeZeroFunctor f).obj T)) : (CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroToFppfSheafOfMul f).app T)) c = (CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroToFppfSheaf f).app T)) ((relativePicardDegreeZeroAddPresheafAddEquiv f T) (Additive.ofMul c))

The canonical map from the multiplicative degree-zero Picard presheaf sends a section to the sheafification image of the corresponding additive section.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafι {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroFppfSheaf f ⟶ relativePicardFppfSheaf f

The inclusion of the degree-zero relative Picard fppf sheaf into the full relative Picard fppf sheaf, obtained by sheafifying the inclusion of presheaves.

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafι_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : relativePicardDegreeZeroFppfSheafι f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat).map (relativePicardDegreeZeroAddPresheafι f)) (CategoryTheory.eqToHom ⋯))

The inclusion of degree-zero fppf sheaves is obtained by applying sheafification to the inclusion of additive Picard presheaves and transporting along the defining equalities.

instance TauCeti.AlgebraicGeometry.instMonoSheafOverSchemeOverFppfTopologyAddCommGrpCatRelativePicardDegreeZeroFppfSheafι {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : CategoryTheory.Mono (relativePicardDegreeZeroFppfSheafι f)

The inclusion of the degree-zero relative Picard fppf sheaf is a monomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheaf_comp_relativePicardDegreeZeroFppfSheafι_hom {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroToFppfSheaf f) (relativePicardDegreeZeroFppfSheafι f).hom = CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroAddPresheafι f) (relativePicardToFppfSheaf f)

The inclusion of degree-zero fppf sheaves is compatible with the canonical maps from the degree-zero and full relative Picard presheaves to their fppf sheafifications.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroToFppfSheaf_comp_relativePicardDegreeZeroFppfSheafι_hom_assoc {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {Z : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ AddCommGrpCat} (h : (relativePicardFppfSheaf f).obj ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroToFppfSheaf f) (CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroFppfSheafι f).hom h) = CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroAddPresheafι f) (CategoryTheory.CategoryStruct.comp (relativePicardToFppfSheaf f) h)

The inclusion of degree-zero fppf sheaves is compatible with the canonical maps from the degree-zero and full relative Picard presheaves to their fppf sheafifications.

noncomputable def TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafHomEquiv {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] (F : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat) : (relativePicardDegreeZeroFppfSheaf f ⟶ F) ≃ (relativePicardDegreeZeroAddPresheaf f ⟶ F.obj)

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

@[simp]

theorem TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheafHomEquiv_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] (F : CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat) (g : relativePicardDegreeZeroFppfSheaf f ⟶ F) : (relativePicardDegreeZeroFppfSheafHomEquiv f F) g = CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroToFppfSheaf f) g.hom

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