Degree of Cartier divisors on a curve

The order of a Cartier divisor at each codimension-one point gives its associated Weil divisor. Taking the residue-degree-weighted sum of those orders defines its degree. On a proper curve the degree of a principal Cartier divisor is zero, so principal translation preserves degree.

On a Noetherian integral curve with discrete valuation rings at codimension-one points, the Weil--Cartier equivalence preserves degree and restricts to an equivalence of degree-zero divisors. When the curve is proper over a field and the first cohomology of its structure sheaf is finite dimensional, the comparison of their divisor sheaves identifies this degree with the Euler-characteristic degree of the associated line bundle.

References

• R. Hartshorne, Algebraic Geometry, Chapter II, Section 6 and Chapter IV, Section 1.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) : CartierDivisor X →+ ℤ

The degree of a Cartier divisor relative to f, obtained by weighting its orders at codimension-one points by their residue degrees.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree_apply {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) (D : CartierDivisor X) : (relativeDegree f) D = (SchemeWeilDivisor.relativeDegree f) D.toWeilDivisor

The Cartier degree is the degree of the associated Weil divisor.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree_eq_sum {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) (D : CartierDivisor X) : (relativeDegree f) D = Finsupp.sum D.toWeilDivisor fun (x : CodimensionOnePoint X) (n : ℤ) => n * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

The degree of a Cartier divisor is the finite sum of its orders times residue degrees.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.degreeZero {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) : AddSubgroup (CartierDivisor X)

The degree-zero Cartier divisors form the kernel of the degree homomorphism.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.degreeZero f = (TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree f).ker

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.mem_degreeZero_iff {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) (D : CartierDivisor X) : D ∈ degreeZero f ↔ (relativeDegree f) D = 0

A Cartier divisor has degree zero exactly when its weighted order sum vanishes.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_equivCartierDivisor {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (f : X ⟶ Y) (D : SchemeWeilDivisor X) : (Scheme.CartierDivisor.relativeDegree f) ((equivCartierDivisor hX) D) = (relativeDegree f) D

The Weil--Cartier equivalence preserves residue-degree-weighted degree.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.degreeZeroEquivCartierDivisor {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (f : X ⟶ Y) : ↥(relativeDegree f).ker ≃+ ↥(Scheme.CartierDivisor.degreeZero f)

The Weil--Cartier equivalence restricts to degree-zero divisors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.degreeZeroEquivCartierDivisor_apply {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (f : X ⟶ Y) (D : ↥(relativeDegree f).ker) : ↑((degreeZeroEquivCartierDivisor hX f) D) = (equivCartierDivisor hX) ↑D

The degree-zero Weil--Cartier equivalence sends a divisor to its Cartier divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.degreeZeroEquivCartierDivisor_symm_apply {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (f : X ⟶ Y) (D : ↥(Scheme.CartierDivisor.degreeZero f)) : ↑((degreeZeroEquivCartierDivisor hX f).symm D) = (↑D).toWeilDivisor

The inverse degree-zero equivalence sends a Cartier divisor to its associated Weil divisor.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree_principalCartierDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)] [FiniteDimensional k (Modules.Cohomology (InvertibleSheaf.trivial X).obj 1)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (g : Additive (↑X.functionField)ˣ) : (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) ((principalCartierDivisorAddHom X) g) = 0

A principal Cartier divisor has degree zero on a proper integral curve.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.relativeDegree_add_principalCartierDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)] [FiniteDimensional k (Modules.Cohomology (InvertibleSheaf.trivial X).obj 1)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : CartierDivisor X) (g : Additive (↑X.functionField)ˣ) : (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) (D + (principalCartierDivisorAddHom X) g) = (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D

Translation by a principal Cartier divisor preserves degree on a proper curve.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalCartierDivisor_mem_degreeZero {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)] [FiniteDimensional k (Modules.Cohomology (InvertibleSheaf.trivial X).obj 1)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (g : Additive (↑X.functionField)ˣ) : (principalCartierDivisorAddHom X) g ∈ degreeZero (X ↘ AlgebraicGeometry.Spec ↧k)

Principal Cartier divisors lie in the degree-zero subgroup.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.eulerDegree_toLineBundleClass {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)] [FiniteDimensional k (Modules.Cohomology (InvertibleSheaf.trivial X).obj 1)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : CartierDivisor X) : LineBundleClass.eulerDegree k D.toLineBundleClass = (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D

The Euler-characteristic degree of the line bundle of a Cartier divisor equals its residue-degree-weighted degree.