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.

For the product formula on a proper curve, this file also supplies the exact finite-sum normal form and the first geometric case: a rational function extending to a global section has zero principal divisor. On a proper integral scheme every nonzero global section is a unit, so the remaining product-formula obligation consists precisely of rational functions which do not extend globally.

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.

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.

@[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.

@[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.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.instNonemptyCarrierCarrierCommRingCatToSchemeTopOpens {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.baseFieldToFunctionField {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) : K →+* ↑X.functionField

The field map from the base field of an integral scheme to its function field, induced by the structure morphism. It is the composite through global sections and the generic stalk.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionGenericMorphism {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : AlgebraicGeometry.Spec (CommRingCat.of ↑X.functionField) ⟶ ProjectiveLine.scheme K

The generic-point morphism to the projective line attached to a nonzero rational function on an integral scheme over K. Its homogeneous coordinates are [g : 1].

Extending this morphism over a regular proper curve and comparing its zero and infinity fibres is the geometric route to the remaining non-global case of the product formula.

Equations

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

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_orderSystem_principalDivisor_apply {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) (g : Additive (↑X.functionField)ˣ) : (relativeDegree f) ((orderSystem X).principalDivisor g) = ∑ x ∈ ((orderSystem X).principalDivisor g).support, (orderAt x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

The relative degree of a principal divisor for the concrete scheme order system is the finite residue-degree-weighted sum of its geometric orders of vanishing. This is the exact finite-sum target of the product formula.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem_isWeightedDegreeZero_iff {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) : ((orderSystem X).IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)) ↔ ∀ (g : Additive (↑X.functionField)ˣ), ∑ x ∈ ((orderSystem X).principalDivisor g).support, (orderAt x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x) = 0

The weighted-degree-zero assertion for the concrete scheme order system is equivalent to the explicit residue-degree-weighted finite sum. This exposes the mathematical product formula without any abstract order-system wrapper.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isWeightedDegreeZero_of_ord_eq_orderAt {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ Y) (S : WeilDivisor.OrderSystem (CodimensionOnePoint X) (Additive (↑X.functionField)ˣ)) (hord : S.ord = orderAt) (hConcrete : (orderSystem X).IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)) : S.IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

Transport the geometric weighted-degree-zero theorem to any abstract order system whose order homomorphisms are exactly Mathlib's scheme-theoretic orders of vanishing. This is the permanent adapter consumed by the proper-curve Challenge contract; finite-support proof fields need not be propositionally identified.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_eq_zero_of_eq_germToFunctionField {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (U : X.Opens) [Nonempty ↥↑U] {a : ↑(X.presheaf.obj (Opposite.op U))} (ha : IsUnit a) (x : CodimensionOnePoint X) (hx : ↑x ∈ U) (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) a) : (orderAt x) g = 0

A rational function represented by a unit on an open neighbourhood has order zero at every codimension-one point of that neighbourhood.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalDivisor_eq_zero_of_eq_germToFunctionField_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : IsUnit a) (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : (orderSystem X).principalDivisor g = 0

A rational function which is represented by a unit on all of an integral Noetherian scheme has zero principal divisor for the concrete scheme order system.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalDivisor_eq_zero_of_proper_of_eq_germToFunctionField_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsProper f] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : (orderSystem X).principalDivisor g = 0

On a proper integral scheme, every rational function extending to a global section has zero principal divisor. Properness is used through the theorem that the global-section ring of an integral universally closed scheme over a field is a field.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_principalDivisor_eq_zero_of_proper_of_eq_germToFunctionField_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsProper f] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : (relativeDegree f) ((orderSystem X).principalDivisor g) = 0

Consequently, every globally represented rational function on a proper integral scheme has relative degree zero for any target morphism. This is the global-function case of the proper curve product formula, stated using the concrete order system from Scheme.Order.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem_isWeightedDegreeZero_of_nonGlobal {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsProper f] (h : ∀ (g : Additive (↑X.functionField)ˣ), (¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) → (relativeDegree f) ((orderSystem X).principalDivisor g) = 0) : (orderSystem X).IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

To prove the product formula on a proper integral scheme it is enough to treat rational functions which do not extend to a global section. The complementary case is discharged by principalDivisor_eq_zero_of_proper_of_eq_germToFunctionField_top; no product-formula content is placed in an assumption-bearing structure.