Additivity of degree on smooth proper curves

On a connected smooth proper curve over a field, the Euler-characteristic degree of a tensor product is the sum of the degrees. The geometric hypotheses suffice: regularity gives integral local rings and discrete valuation rings in codimension one, and properness gives finite-dimensional first cohomology. No rational point or perfectness of the field is required.

The field-valued fibres of a smooth proper geometrically connected family of relative dimension one satisfy these hypotheses. Consequently degree is additive on the Picard group of every such fibre. This is the fibrewise calculation which makes the classes of degree zero on every geometric fibre closed under tensor product.

Main results

• LineBundleClass.eulerDegree_mul_of_smooth: additivity on connected smooth proper curves;
• LineBundleClass.eulerDegree_mul_fieldValuedBaseChange: additivity on all field-valued fibres of a smooth proper geometrically connected family of curves.

References

• R. Hartshorne, Algebraic Geometry, Chapter IV, Section 1.
• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.5.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree_mul_of_smooth (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.SmoothOfRelativeDimension 1 (X ↘ AlgebraicGeometry.Spec ↧k)] [ConnectedSpace ↥X] (a b : LineBundleClass X) : eulerDegree k (a * b) = eulerDegree k a + eulerDegree k b

The Euler-characteristic degree is additive on a connected smooth proper curve over any field. Integrality, discrete valuation stalks, and finiteness of cohomology follow from the geometric hypotheses; no rational point is required.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree_mul_fieldValuedBaseChange {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] (k : Type u) [Field k] (s : AlgebraicGeometry.Spec ↧k ⟶ S) (a b : LineBundleClass (CategoryTheory.Limits.pullback s f)) : eulerDegree k (a * b) = eulerDegree k a + eulerDegree k b

On every field-valued fibre of a smooth proper geometrically connected family of curves, the Euler-characteristic degree is additive. The point may have values in an arbitrary field, including an imperfect field.