Relative effective Cartier divisors of degree zero and one are representable #
Let f : X ⟶ S be a proper family of curves. The symmetric power Symᵈ X should represent the
functor Div^d_{X/S} of relative effective Cartier divisors of degree d. This file proves the
two cases d = 0 and d = 1, where Sym⁰ X = S and Sym¹ X = X.
- Degree zero. A relative effective Cartier divisor
DonX_ToverTis finite flat overT, and its rank vanishes exactly off its image. SoDhas degree zero exactly when it is empty, andDiv⁰_{X/S}is the one-point functor, represented byS. - Degree one. When
fis moreover smooth of relative dimension one, sending aT-pointxofXoverSto its graphΓₓ ⊆ X_Tis a natural transformationgraphDivisorfrom the functor of points ofXtoDiv_{X/S}. It is injective, and its image is exactlyDiv¹_{X/S}(a degree-one divisor is the image of a unique section ofX_T ⟶ T). So it corestricts to a natural isomorphismHom_S(-, X) ≅ Div¹_{X/S}, andXrepresentsDiv¹_{X/S}.
Main declarations #
TauCeti.AlgebraicGeometry.mem_relativeEffectiveCartierDegreeSubfunctor_zero_obj_iff: the divisors of degree zero are the empty divisor;- the instances
Uniqueon the values ofDiv⁰_{X/S}and(relativeEffectiveCartierDegreeSubfunctor f 0).toFunctor.IsRepresentable; TauCeti.AlgebraicGeometry.range_graphDivisor: the image of the graph divisor isDiv¹_{X/S};TauCeti.AlgebraicGeometry.graphDivisorDegreeOne: the graph divisor as a natural transformationHom_S(-, X) ⟶ Div¹_{X/S}, which is an isomorphism;TauCeti.AlgebraicGeometry.graphDivisorDegreeOne_app_basePoint: under it, the base point given by a sectionx₀corresponds to the degree-one divisorx₀_Ton every base change;- the instance
(relativeEffectiveCartierDegreeSubfunctor f 1).toFunctor.IsRepresentable.
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.
The only divisor of degree zero is the empty divisor. For a proper f : X ⟶ S with
fibres of dimension at most one, a relative effective Cartier divisor on X_T over T has
degree zero exactly when it is the empty divisor ⊤.
On every base change, the empty divisor is the unique divisor of degree zero.
S represents Div⁰_{X/S}: the functor of divisors of degree zero is represented by the
terminal object S of the category of S-schemes.
The graphs of points are exactly the divisors of degree one: for a smooth proper f of
relative dimension one, the image of the graph divisor Hom_S(-, X) ⟶ Div_{X/S} is the
subfunctor Div¹_{X/S} of relative effective Cartier divisors of degree one.
The graph divisor of degree one: for a smooth proper f : X ⟶ S 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 of degree one, sending a T-point to
its graph. It is an isomorphism, so X represents Div¹_{X/S}.
Instances For
Composing the graph divisor of degree one with the inclusion Div¹_{X/S} ⟶ Div_{X/S} gives
the graph divisor.
Composing the graph divisor of degree one with the inclusion Div¹_{X/S} ⟶ Div_{X/S} gives
the graph divisor.
The divisor underlying the graph divisor of degree one of x is the graph divisor of x.
X represents Div¹_{X/S}: the graph divisor of degree one is an isomorphism.
X represents Div¹_{X/S}, through the graph divisor of degree one.
Under the isomorphism Hom_S(-, X) ≅ Div¹_{X/S}, the base point T ⟶ S ⟶ X given by a
section x₀ of f corresponds to the degree-one divisor of the base-changed section
x₀_T : T ⟶ X_T.