Graphs of points as relative effective Cartier divisors

Let f : X ⟶ S be a separated morphism of schemes. A T-point x : T ⟶ X of X over S has a graph Γₓ : T ⟶ X_T = T ×_S X (TauCeti.AlgebraicGeometry.graphSection), a section of the projection X_T ⟶ T and hence a closed immersion. Its ideal sheaf commutes with base change along morphisms T' ⟶ T over S. When f is moreover smooth of relative dimension one, the graph is a relative effective Cartier divisor on X_T over T (Scheme.Hom.isRelativeEffectiveCartier_ker_of_smoothOfRelativeDimension).

Together these make the graph a natural transformation graphDivisor from the functor of points T ↦ Hom_S(T, X) of X to the functor Div_{X/S} of relative effective Cartier divisors. It is injective at every T, since a point is determined by its graph, and a section of a separated morphism by its ideal sheaf. Composed with the Abel map D ↦ 𝒪(D) it gives the degree-one Abel map x ↦ 𝒪(Γₓ) into the relative Picard presheaf, from which TauCeti.AlgebraicGeometry.abelJacobiMap is built.

Main declarations

• TauCeti.AlgebraicGeometry.ker_graphSection_comp: the ideal sheaf of the graph commutes with base change;
• TauCeti.AlgebraicGeometry.ker_graphSection_inj: a point is determined by the ideal sheaf of its graph;
• TauCeti.AlgebraicGeometry.graphDivisor: the natural transformation Hom_S(-, X) ⟶ Div_{X/S} sending a point to its graph;
• TauCeti.AlgebraicGeometry.graphDivisor_app_injective: distinct points have distinct graph divisors.

References

• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.3.
• The Stacks Project, Picard Schemes of Curves, section Moduli of divisors on smooth curves.

instance TauCeti.AlgebraicGeometry.instIsClosedImmersionGraphSectionOfIsSeparated {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] {T : CategoryTheory.Over S} (x : T ⟶ CategoryTheory.Over.mk f) : AlgebraicGeometry.IsClosedImmersion (graphSection x)

The graph of a T-point of a separated morphism is a closed immersion.

theorem TauCeti.AlgebraicGeometry.ker_graphSection_comp {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] {T' T : CategoryTheory.Over S} (φ : T' ⟶ T) (x : T ⟶ CategoryTheory.Over.mk f) : AlgebraicGeometry.Scheme.Hom.ker (graphSection (CategoryTheory.CategoryStruct.comp φ x)) = (AlgebraicGeometry.Scheme.Hom.ker (graphSection x)).comap (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ))

The ideal sheaf of a graph commutes with base change. For a separated morphism f, the ideal sheaf of the graph of the base change φ ≫ x of a T-point x along φ : T' ⟶ T is the inverse image of the ideal sheaf of the graph of x along T' ×_S X ⟶ T ×_S X.

@[simp]

theorem TauCeti.AlgebraicGeometry.ker_graphSection_inj {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] {T : CategoryTheory.Over S} {x y : T ⟶ CategoryTheory.Over.mk f} : AlgebraicGeometry.Scheme.Hom.ker (graphSection x) = AlgebraicGeometry.Scheme.Hom.ker (graphSection y) ↔ x = y

A point is determined by the ideal sheaf of its graph: for a separated f, two T-points of X over S are equal exactly when their graphs have the same ideal sheaf.

theorem TauCeti.AlgebraicGeometry.ker_graphSection_mem_relativeEffectiveCartierSubfunctor_obj {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {T : CategoryTheory.Over S} (x : T ⟶ CategoryTheory.Over.mk f) : AlgebraicGeometry.Scheme.Hom.ker (graphSection x) ∈ (relativeEffectiveCartierSubfunctor f).obj (Opposite.op T)

The graph of a T-point of a separated morphism which is smooth of relative dimension one is a relative effective Cartier divisor on X_T over T.

noncomputable def TauCeti.AlgebraicGeometry.graphDivisor {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] : CategoryTheory.yoneda.obj (CategoryTheory.Over.mk f) ⟶ (relativeEffectiveCartierSubfunctor f).toFunctor

The graph divisor: for a separated morphism f : X ⟶ S which is smooth of relative dimension one, the natural transformation from the functor of points T ↦ Hom_S(T, X) of X to the functor Div_{X/S} of relative effective Cartier divisors, sending a T-point x to its graph Γₓ ⊆ X_T.

@[simp]

theorem TauCeti.AlgebraicGeometry.graphDivisor_app_apply_val {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {T : (CategoryTheory.Over S)ᵒᵖ} (x : Opposite.unop T ⟶ CategoryTheory.Over.mk f) : ↑((CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T)) x) = AlgebraicGeometry.Scheme.Hom.ker (graphSection x)

The ideal sheaf of the graph divisor of x is the ideal sheaf of the graph of x.

theorem TauCeti.AlgebraicGeometry.graphDivisor_app_comp {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (x : Opposite.unop T ⟶ CategoryTheory.Over.mk f) : (CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T')) (CategoryTheory.CategoryStruct.comp φ.unop x) = (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierSubfunctor f).toFunctor.map φ)) ((CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T)) x)

The graph divisor of the base change φ ≫ x of a T-point x along φ : T' ⟶ T is the pullback of the graph divisor of x.

theorem TauCeti.AlgebraicGeometry.graphDivisor_app_injective {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (T : (CategoryTheory.Over S)ᵒᵖ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((graphDivisor f).app T))

Distinct points have distinct graph divisors: for every scheme T over S, the graph divisor is injective on T-points.