Abel–Jacobi maps into the degree-zero Picard fppf sheaf

For a smooth proper geometrically connected family of curves f : X ⟶ S with a section x₀, the normalized Abel map sends a relative effective Cartier divisor D of degree d to the degree-zero class 𝒪(D - d • x₀). Composing this map with fppf sheafification gives the canonical map from the divisor functor to the degree-zero relative Picard fppf sheaf.

In degree one, the graph construction gives the Abel–Jacobi map from the functor of points of X. It sends the base-changed section x₀ to zero. These maps are stated before representability; when the degree-zero Picard sheaf is represented, they are the functor-of-points maps induced by the corresponding morphisms of schemes.

Main declarations

• TauCeti.AlgebraicGeometry.abelJacobiMapOfDegreeToPicZeroFppf: the normalized degree-d Abel map into the degree-zero Picard fppf sheaf;
• TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf: the Abel–Jacobi map from the functor of points of X into that sheaf;
• TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf_app_basePoint: the base point maps to zero.

References

• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Sections 9.3 and 9.5.
• J. S. Milne, Jacobian varieties, in Arithmetic Geometry (G. Cornell, J. H. Silverman, eds.), Springer, 1986, Sections 2 and 5.

noncomputable def TauCeti.AlgebraicGeometry.abelJacobiMapOfDegreeToPicZeroFppf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (d : ℕ) : (relativeEffectiveCartierDegreeSubfunctor f d).toFunctor.comp CategoryTheory.uliftFunctor.{u + 1, u} ⟶ (relativePicardDegreeZeroFppfSheaf f).obj.comp (CategoryTheory.forget AddCommGrpCat)

The normalized Abel map into the degree-zero Picard fppf sheaf. A relative effective Cartier divisor D of degree d is sent to the fppf-local class of 𝒪(D - d • x₀).

@[simp]

theorem TauCeti.AlgebraicGeometry.abelJacobiMapOfDegreeToPicZeroFppf_app_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (d : ℕ) {T : (CategoryTheory.Over S)ᵒᵖ} (D : ((relativeEffectiveCartierDegreeSubfunctor f d).toFunctor.comp CategoryTheory.uliftFunctor.{u + 1, u}).obj T) : (CategoryTheory.ConcreteCategory.hom ((abelJacobiMapOfDegreeToPicZeroFppf f hx₀ d).app T)) D = (CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroToFppfSheaf f).app T)) ((relativePicardDegreeZeroAddPresheafAddEquiv f T) (Additive.ofMul (relativePicardDegreeZeroFunctor.mk f ↑((CategoryTheory.ConcreteCategory.hom ((abelJacobiMapOfDegreeToPicZero f hx₀ d).app T)) D) ⋯)))

The degree-d Abel map into the degree-zero Picard fppf sheaf is the sheafification image of its degree-zero Picard class.

noncomputable def TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) : (CategoryTheory.yoneda.obj (CategoryTheory.Over.mk f)).comp CategoryTheory.uliftFunctor.{u + 1, u} ⟶ (relativePicardDegreeZeroFppfSheaf f).obj.comp (CategoryTheory.forget AddCommGrpCat)

The Abel–Jacobi map into the degree-zero Picard fppf sheaf. It sends an S-point x : T ⟶ X to the fppf-local class of 𝒪(Γₓ - x₀,T).

theorem TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) : abelJacobiMapToPicZeroFppf f hx₀ = CategoryTheory.CategoryStruct.comp (abelJacobiMapToPicZero f hx₀) (CategoryTheory.CategoryStruct.comp (relativePicardDegreeZeroSubfunctorIsoFunctor f).hom (relativePicardDegreeZeroToFppfSheafOfMul f))

The Abel–Jacobi map into the degree-zero Picard fppf sheaf is the existing degree-zero Abel–Jacobi class followed by the comparison with the group-valued functor and sheafification.

@[simp]

theorem TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf_app_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T : (CategoryTheory.Over S)ᵒᵖ} (x : ((CategoryTheory.yoneda.obj (CategoryTheory.Over.mk f)).comp CategoryTheory.uliftFunctor.{u + 1, u}).obj T) : (CategoryTheory.ConcreteCategory.hom ((abelJacobiMapToPicZeroFppf f hx₀).app T)) x = (CategoryTheory.ConcreteCategory.hom ((relativePicardDegreeZeroToFppfSheaf f).app T)) ((relativePicardDegreeZeroAddPresheafAddEquiv f T) (Additive.ofMul (relativePicardDegreeZeroFunctor.mk f ↑((CategoryTheory.ConcreteCategory.hom ((abelJacobiMapToPicZero f hx₀).app T)) x) ⋯)))

The value of the Abel–Jacobi map in the degree-zero Picard fppf sheaf is the sheafification image of its existing degree-zero Picard class.

@[simp]

theorem TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf_app_basePoint {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : (CategoryTheory.ConcreteCategory.hom ((abelJacobiMapToPicZeroFppf f hx₀).app T)) { down := basePoint hx₀ (Opposite.unop T) } = 0

The Abel–Jacobi map into the degree-zero Picard fppf sheaf sends the base point to zero.