Relative effective Cartier divisors of degree one are sections

Let f : X ⟶ S be locally of finite presentation with fibres of dimension at most one, and let D be a relative effective Cartier divisor on X over S which is proper over S. Then D is finite locally free over S, and it maps isomorphically to S exactly when its degree, the rank of D ⟶ S, is 1 at every point of S. When f is moreover separated, D is then the divisor [s] of a unique section s of f, the section AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso cut out by D. Conversely, the divisor of a section of a separated f has degree one.

Applied to the base changes X_T = T ×_S X ⟶ T of a proper f, this shows that a relative effective Cartier divisor on X_T over T has degree one exactly when it is the graph Γₓ of a T-point x of X over S, and x is then unique (TauCeti.AlgebraicGeometry.exists_ker_graphSection_eq_iff_finrank_eq_one). When f is smooth of relative dimension one, every graph is a relative effective Cartier divisor, and this is the statement that the graph divisor TauCeti.AlgebraicGeometry.graphDivisor is injective, by TauCeti.AlgebraicGeometry.graphDivisor_app_injective, with image the divisors of degree one. Since graphDivisor is a natural transformation, the correspondence between points and divisors of degree one commutes with arbitrary base change T' ⟶ T.

Main results

In the namespace AlgebraicGeometry.Scheme.IdealSheafData:

• IsRelativeEffectiveCartier.isIso_subschemeι_comp_iff_finrank_eq_one: a proper relative effective Cartier divisor on a relative curve maps isomorphically to the base exactly when it has degree one;
• IsRelativeEffectiveCartier.exists_comp_eq_id_and_ker_eq_iff_finrank_eq_one: it is the divisor of a section exactly when it has degree one.

In the namespace TauCeti.AlgebraicGeometry:

• exists_ker_graphSection_eq_iff_finrank_eq_one: a relative effective Cartier divisor on X_T over T is the graph of a T-point of X over S exactly when it has degree one.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.2.
• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.3.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isIso_subschemeι_comp_iff_finrank_eq_one {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [LocallyOfFinitePresentation f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] [IsProper (CategoryTheory.CategoryStruct.comp I.subschemeι f)] (hI : I.IsRelativeEffectiveCartier f) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f) ↔ Hom.finrank (CategoryTheory.CategoryStruct.comp I.subschemeι f) = 1

A relative effective Cartier divisor maps isomorphically to the base exactly when it has degree one. If f : X ⟶ S is locally of finite presentation with fibres of dimension at most one, then the closed subscheme of a relative effective Cartier divisor on X over S which is proper over S maps isomorphically to S if and only if its rank is 1 at every point of S.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.exists_comp_eq_id_and_ker_eq_iff_finrank_eq_one {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [IsSeparated f] [LocallyOfFinitePresentation f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] [IsProper (CategoryTheory.CategoryStruct.comp I.subschemeι f)] (hI : I.IsRelativeEffectiveCartier f) : (∃ (s : S ⟶ X), CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S ∧ Hom.ker s = I) ↔ Hom.finrank (CategoryTheory.CategoryStruct.comp I.subschemeι f) = 1

Relative effective Cartier divisors of degree one are sections. If f : X ⟶ S is separated and locally of finite presentation with fibres of dimension at most one, then a relative effective Cartier divisor on X over S which is proper over S is the divisor of a section of f if and only if it has degree one, that is, rank 1 over every point of S. The section is then unique (AlgebraicGeometry.Scheme.Hom.ker_eq_ker_iff_of_comp_eq_id); it is AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso.

theorem TauCeti.AlgebraicGeometry.exists_ker_graphSection_eq_iff_finrank_eq_one {S X : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.LocallyOfFinitePresentation f] [RelativeDimensionLE 1 f] {T : CategoryTheory.Over S} {D : (CategoryTheory.Limits.pullback T.hom f).IdealSheafData} (hD : D.IsRelativeEffectiveCartier (CategoryTheory.Limits.pullback.fst T.hom f)) : (∃ (x : T ⟶ CategoryTheory.Over.mk f), AlgebraicGeometry.Scheme.Hom.ker (graphSection x) = D) ↔ AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.CategoryStruct.comp D.subschemeι (CategoryTheory.Limits.pullback.fst T.hom f)) = 1

The graphs of points are the divisors of degree one. Let f : X ⟶ S be proper and locally of finite presentation with fibres of dimension at most one. For a scheme T over S, a relative effective Cartier divisor D on X_T = T ×_S X over T is the graph Γₓ of a T-point x of X over S if and only if D has degree one over T. The point x is then unique, by ker_graphSection_inj.