Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.Degree

Relative degrees of scheme-theoretic Weil divisors #

This file specializes WeilDivisor.weightedDegree to the residue-degree weights associated to a scheme morphism. For a curve over a field, applied to its structure morphism, this is the divisor degree Σ_x [κ(x) : k] · ord_x.

The composition formula records how these weights change through successive scheme morphisms. This supplies the residue-field-weighted divisor degree required in Layer A of the Jacobian challenge roadmap.

source
noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
SchemeWeilDivisor X →+ ℤ

The degree of a scheme-theoretic Weil divisor weighted by the residue degrees of f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (D : SchemeWeilDivisor X) :
    (relativeDegree f) D = Finsupp.sum D fun (x : CodimensionOnePoint X) (n : ℤ) => n * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

    The relative degree is the finite sum of coefficients times residue degrees.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_ofPoint {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : CodimensionOnePoint X) :
    (relativeDegree f) (WeilDivisor.ofPoint x) = ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

    A prime divisor has relative degree equal to the residue degree of its generic point.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (D : SchemeWeilDivisor X) :
    (relativeDegree (CategoryTheory.CategoryStruct.comp f g)) D = (WeilDivisor.weightedDegree fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree g (f ↑x)) * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)) D

    Relative degree along a composite uses the product of the successive residue degrees.

    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_nonneg {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {D : SchemeWeilDivisor X} (hD : WeilDivisor.IsEffective D) :
    0 ≤ (relativeDegree f) D

    An effective divisor has nonnegative relative degree: residue degrees are nonnegative.