The Abel–Jacobi map on functors of points

Let f : X ⟶ S be a separated morphism of schemes which is smooth of relative dimension one, with a section x₀. A T-point x : T ⟶ X of X over S has a graph Γₓ ⊆ X_T = T ×_S X, a relative effective Cartier divisor on X_T over T, natural in T (TauCeti.AlgebraicGeometry.graphDivisor). Composing with the Abel map D ↦ 𝒪(D) into the relative Picard presheaf T ↦ Pic(X_T) / Pic(T) (TauCeti.AlgebraicGeometry.abelMap) gives the degree-one Abel map x ↦ 𝒪(Γₓ). Dividing by its value at the base point normalizes it to the Abel–Jacobi map abelJacobiMap, which sends a T-point x to the class of 𝒪(Γₓ) ⊗ 𝒪(x₀_T)⁻¹ = 𝒪(Γₓ - x₀_T), where x₀_T is the base change of x₀, and sends the base point to the identity (abelJacobiMap_app_basePoint).

For a smooth proper geometrically connected curve X over a field with a rational point x₀, this is the map x ↦ 𝒪(x - x₀) from X to its Jacobian, written on functors of points. Representability of the Picard functor and of its degree-zero part is not treated here, so no morphism of schemes is constructed.

Main declarations

• TauCeti.AlgebraicGeometry.abelJacobiMap: the natural transformation from the functor of points T ↦ Hom_S(T, X) to T ↦ Pic(X_T) / Pic(T), sending x to the class of 𝒪(Γₓ - x₀_T) (abelJacobiMap_app_apply);
• TauCeti.AlgebraicGeometry.abelJacobiMap_app_basePoint: it sends x₀ to the identity.

References

• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.3 (the Abel map).
• J. S. Milne, Jacobian varieties, in Arithmetic Geometry (G. Cornell, J. H. Silverman, eds.), Springer, 1986, Section 2 (the canonical map Q ↦ 𝒪(Q - P) from a curve to its Jacobian).

noncomputable def TauCeti.AlgebraicGeometry.abelJacobiMap {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 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} ⟶ (relativePicardPresheaf f).comp (CategoryTheory.forget CommGrpCat)

The Abel–Jacobi map of a separated morphism f : X ⟶ S, smooth of relative dimension one, with a section x₀: the natural transformation from the functor of points T ↦ Hom_S(T, X) of X to the relative Picard presheaf T ↦ Pic(X_T) / Pic(T), sending a T-point x to the class of 𝒪(Γₓ - x₀_T) = 𝒪(Γₓ) ⊗ 𝒪(x₀_T)⁻¹, where Γₓ is the graph of x and x₀_T the base change of x₀ (abelJacobiMap_app_apply).

theorem TauCeti.AlgebraicGeometry.abelJacobiMap_app_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {x₀ : S ⟶ X} (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T : (CategoryTheory.Over S)ᵒᵖ} (x : Opposite.unop T ⟶ CategoryTheory.Over.mk f) : (CategoryTheory.ConcreteCategory.hom ((abelJacobiMap f hx₀).app T)) { down := x } = (CategoryTheory.ConcreteCategory.hom ((abelMap f).app T)) { down := (CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T)) x } / (CategoryTheory.ConcreteCategory.hom ((abelMap f).app T)) { down := (CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T)) (basePoint hx₀ (Opposite.unop T)) }

The Abel–Jacobi map sends a T-point x to the quotient of the Abel map at its graph by the Abel map at the graph of the base point, that is, to the class of 𝒪(Γₓ - x₀_T).

@[simp]

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

The Abel–Jacobi map sends the base point to the identity: 𝒪(x₀_T - x₀_T) = 𝒪.