The degree-zero subfunctor of the relative Picard presheaf #
Let f : X ⟶ S be a morphism of schemes and T a scheme over S, with base change
X_T = T ×_S X. A point ξ : Spec Ω ⟶ T with values in a field Ω has the fibre
X_ξ = Spec Ω ×_S X, a scheme over Ω mapping to X_T. The fibre degree of a line-bundle
class a on X_T at ξ is the Euler-characteristic degree χ(a|_{X_ξ}) - χ(𝒪_{X_ξ}) over Ω
of its restriction to X_ξ (LineBundleClass.eulerDegree). Since every line bundle on Spec Ω
is trivial, the fibre degree does not see classes pulled back from T, so it is defined on the
relative Picard presheaf T ↦ Pic(X_T) / Pic(T) (relativePicardFiberDegree). It is natural:
the fibre degree of the pullback of a class along T' ⟶ T at ξ' is the fibre degree of the
class at the composite point Spec Ω ⟶ T' ⟶ T (relativePicardFiberDegree_map).
The classes whose fibre degree vanishes at every geometric point, that is at every point with
values in an algebraically closed field, therefore form a subfunctor
relativePicardDegreeZeroSubfunctor of the relative Picard presheaf. When f is a smooth proper
curve with geometrically connected fibres, this is the functor Pic⁰_{X/S} of line bundles of
degree zero on every geometric fibre, before representability.
On a fibre which is a proper integral curve over Ω with discrete valuation rings as
codimension-one local rings, the fibre degree is additive (relativePicardFiberDegree_mul), by
Riemann–Roch on that curve, and a class has fibre degree zero there exactly when its restriction
lies in Pic⁰ of the fibre, LineBundleClass.picZero (relativePicardFiberDegree_mk_eq_zero_iff).
Every field-valued fibre of a smooth proper geometrically connected family of curves is such a
curve, so for such f the fibre degree is additive at every point
(relativePicardFiberDegree_mul_of_smooth) and the degree-zero subfunctor is closed under
products and inverses (mul_mem_relativePicardDegreeZeroSubfunctor_obj,
inv_mem_relativePicardDegreeZeroSubfunctor_obj). It is then a presheaf of commutative groups
relativePicardDegreeZeroFunctor, with inclusion relativePicardDegreeZeroFunctorι into the
relative Picard presheaf. For a scheme over a field which is not a
proper curve, LineBundleClass.eulerDegree takes the same junk values as the truncated Euler
characteristic Scheme.Modules.eulerCharBelow; the definitions here make sense in general, but
they are only the degree and Pic⁰ for families of curves. Local constancy of the degree in flat
families and representability are not treated here.
Main declarations #
TauCeti.AlgebraicGeometry.relativePicardFiberDegree: the degree on the fibre over a pointSpec Ω ⟶ Tof a section ofT ↦ Pic(X_T) / Pic(T);TauCeti.AlgebraicGeometry.relativePicardFiberDegree_mk: its value on the class of a line bundle onX_T;TauCeti.AlgebraicGeometry.relativePicardFiberDegree_map: its naturality inT;TauCeti.AlgebraicGeometry.relativePicardFiberDegree_mul: its additivity on a fibre which is a curve;TauCeti.AlgebraicGeometry.relativePicardFiberDegree_mk_eq_zero_iff: on a fibre which is a curve, degree zero is membership inPic⁰of the fibre;TauCeti.AlgebraicGeometry.relativePicardFiberDegree_mul_of_smooth: its additivity at every point, for a smooth proper geometrically connected family of curves;TauCeti.AlgebraicGeometry.relativePicardDegreeZeroSubfunctor: the subfunctor of classes of degree zero on every geometric fibre;TauCeti.AlgebraicGeometry.mul_mem_relativePicardDegreeZeroSubfunctor_obj,TauCeti.AlgebraicGeometry.inv_mem_relativePicardDegreeZeroSubfunctor_obj: for a smooth proper geometrically connected family of curves, it is closed under products and inverses.TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor: for such a family,Pic⁰_{X/S}as a presheaf of commutative groups, with inclusionTauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctorιinto the relative Picard presheaf, sections built byTauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor.mk, and morphisms into it lifted byTauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor.liftand compared byTauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor.hom_ext.
References #
- S. Bosch, W. Lütkebohmert, M. Raynaud, Néron Models, Section 8.4.
- S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.5.
The degree on the fibre over a point ξ : Spec Ω ⟶ T of a section of the relative
Picard presheaf T ↦ Pic(X_T) / Pic(T): the Euler-characteristic degree over Ω of the
restriction of a representing line-bundle class to the fibre Spec Ω ×_S X of X_T over ξ
(relativePicardFiberDegree_mk). It is well defined because line-bundle classes pulled back from
T are trivial on the fibre.
Instances For
The fibre degree of the class of a line bundle on X_T at ξ : Spec Ω ⟶ T is the
Euler-characteristic degree over Ω of its pullback to the fibre Spec Ω ×_S X.
The identity of Pic(X_T) / Pic(T) has degree zero on every fibre.
The fibre degree is additive on a fibre which is a curve. If the fibre
X_ξ = Spec Ω ×_S X over ξ : Spec Ω ⟶ T is a proper integral curve over Ω whose
codimension-one local rings are discrete valuation rings and whose H¹(X_ξ, 𝒪) is
finite-dimensional, then the fibre degree at ξ is additive on Pic(X_T) / Pic(T).
The fibre degree of a family of curves is additive. For a smooth proper geometrically
connected morphism f of relative dimension one, the fibre degree at every point
ξ : Spec Ω ⟶ T is additive on Pic(X_T) / Pic(T), since every field-valued fibre of f is a
connected smooth proper curve (LineBundleClass.eulerDegree_mul_fieldValuedBaseChange).
For a smooth proper geometrically connected family of curves, the fibre degree of an inverse is the negative of the fibre degree.
On a fibre which is a curve, degree zero is membership in Pic⁰ of the fibre. If the
fibre X_ξ = Spec Ω ×_S X over ξ : Spec Ω ⟶ T is a proper integral curve over Ω whose
codimension-one local rings are discrete valuation rings and whose H¹(X_ξ, 𝒪) is
finite-dimensional, then the class of a line bundle on X_T has fibre degree zero at ξ exactly
when its restriction to X_ξ lies in Pic⁰ X_ξ (LineBundleClass.picZero).
Naturality of the fibre degree. For a morphism T' ⟶ T over S and a point
ξ' : Spec Ω ⟶ T', the fibre degree at ξ' of the pullback of a section from T to T' is
its fibre degree at the composite point Spec Ω ⟶ T' ⟶ T.
The degree-zero subfunctor Pic⁰_{X/S} of the relative Picard presheaf
T ↦ Pic(X_T) / Pic(T) of f : X ⟶ S: at a scheme T over S, the classes whose
fibre degree vanishes at every geometric point Spec Ω ⟶ T, with Ω algebraically closed. It is
a subfunctor by naturality of the fibre degree (relativePicardFiberDegree_map).
The fibre degree is the degree of a line bundle on a fibre that is a proper curve, where it is
additive (relativePicardFiberDegree_mul). So this is Pic⁰_{X/S} for families of such curves. For
other f, the condition inherits the junk values of LineBundleClass.eulerDegree.
Instances For
A section of T ↦ Pic(X_T) / Pic(T) lies in Pic⁰_{X/S} exactly when its fibre degree
vanishes at every geometric point of T.
The identity of Pic(X_T) / Pic(T) lies in Pic⁰_{X/S}.
For a smooth proper geometrically connected family of curves, Pic⁰_{X/S} is closed under
products in Pic(X_T) / Pic(T).
For a smooth proper geometrically connected family of curves, Pic⁰_{X/S} is closed under
inverses in Pic(X_T) / Pic(T).
For a smooth proper geometrically connected family of curves, Pic⁰_{X/S}(T) as a subgroup
of Pic(X_T) / Pic(T): the classes of degree zero on every geometric fibre, that is the sections
of relativePicardDegreeZeroSubfunctor at T.
Instances For
A section of T ↦ Pic(X_T) / Pic(T) lies in the subgroup Pic⁰_{X/S}(T) exactly when it is
a section of the degree-zero subfunctor.
The degree-zero Picard functor Pic⁰_{X/S} of a smooth proper geometrically connected
family of curves f : X ⟶ S, as a presheaf of commutative groups on schemes over S: it sends
T to the subgroup relativePicardDegreeZeroSubgroup f T of Pic(X_T) / Pic(T), and a morphism
over S to the restriction of the pullback map of the relative Picard presheaf.
Instances For
The value of the degree-zero Picard functor at T is the subgroup Pic⁰_{X/S}(T) of
Pic(X_T) / Pic(T).
The section of Pic⁰_{X/S} at T given by a section of T ↦ Pic(X_T) / Pic(T) of degree
zero on every geometric fibre.
Instances For
Restrict a group homomorphism to the degree-zero relative Picard functor when all of its values have fibrewise degree zero.
Instances For
The degree-zero Picard functor Pic⁰_{X/S} acts on the section
relativePicardDegreeZeroFunctor.mk f c hc by the pullback map of the relative Picard presheaf
T ↦ Pic(X_T) / Pic(T).
The inclusion of the degree-zero Picard functor Pic⁰_{X/S} into the relative Picard
presheaf T ↦ Pic(X_T) / Pic(T), as a morphism of presheaves of commutative groups.
Instances For
The inclusion relativePicardDegreeZeroFunctorι sends the section
relativePicardDegreeZeroFunctor.mk f c hc of Pic⁰_{X/S} to c.
Restricting a group homomorphism to the degree-zero relative Picard functor and then forgetting the degree-zero proof recovers the original homomorphism.
The inclusion relativePicardDegreeZeroFunctorι sends a section of Pic⁰_{X/S} to a section
of T ↦ Pic(X_T) / Pic(T) of degree zero on every geometric fibre.
The inclusion relativePicardDegreeZeroFunctorι is injective on sections.
Lift a morphism α : F ⟶ H ⋙ relativePicardPresheaf f of presheaves of commutative groups
whose sections all have degree zero on every geometric fibre to a morphism into the degree-zero
Picard functor Pic⁰_{X/S} (restricted along H).
Instances For
The lift relativePicardDegreeZeroFunctor.lift f α hα sends a section c to a section of
Pic⁰_{X/S} whose image under the inclusion is α.app T c.
The lift relativePicardDegreeZeroFunctor.lift f α hα followed by the inclusion of
Pic⁰_{X/S} is α.
The lift relativePicardDegreeZeroFunctor.lift f α hα followed by the inclusion of
Pic⁰_{X/S} is α.
Two morphisms into Pic⁰_{X/S} (restricted along H) are equal once they agree after the
inclusion into the relative Picard presheaf.
For a morphism α : F ⟶ relativePicardPresheaf f of presheaves on (Over S)ᵒᵖ, the lift
relativePicardDegreeZeroFunctor.lift f α hα (along H := 𝟭 _) followed by the inclusion of
Pic⁰_{X/S} is α.
For a morphism α : F ⟶ relativePicardPresheaf f of presheaves on (Over S)ᵒᵖ, the lift
relativePicardDegreeZeroFunctor.lift f α hα (along H := 𝟭 _) followed by the inclusion of
Pic⁰_{X/S} is α.
Two morphisms into Pic⁰_{X/S} are equal once they agree after the inclusion into the
relative Picard presheaf.
The set-valued degree-zero subfunctor and the underlying set-valued functor of its commutative-group structure have the same sections and pullback maps.
Instances For
The comparison from the set-valued degree-zero subfunctor to the underlying group-valued functor sends a section to the same class with its degree-zero proof.