Weil divisors as finite integer combinations of points #
This file provides the first, purely combinatorial piece of the Jacobian roadmap's Layer A: Weil divisors are finite formal integer sums of points. The scheme-theoretic predicates which decide which points are codimension-one points, the principal-divisor map, and the comparison with Cartier divisors are deliberately not bundled here; those are later geometric constructions.
The API here records the free-abelian-group operations needed before that geometry exists:
point divisors, effectivity, pushforward of formal sums along a map of point sets, and both
the unweighted degree and the weighted degree used for curves over a field. It also packages
the degree-zero subgroups that later receive principal divisors and model the abstract
Pic⁰ kernel before the Picard functor and Picard scheme exist.
For a curve over k, the intended weighted degree has weight
x ↦ [κ(x) : k]; this file only supplies the formal finite-sum operation against an arbitrary
integer-valued weight.
This advances the Tau Ceti Jacobian roadmap, Layer A, "Divisors on a curve: Weil divisors
⊕_x ℤ", "Degree", and "Pic⁰ X = ker deg (as an abstract group)".
A Weil divisor on a type of points X is a finite formal integer sum of points of X.
Equations
Instances For
The coefficient of a point in a Weil divisor.
Instances For
A point lies in the support of a Weil divisor exactly when its coefficient is nonzero. This
is the coeff-level restatement of Finsupp.mem_support_iff.
The prime/point divisor supported at a single point with coefficient 1.
Equations
Instances For
The scaled point divisor b • ofPoint a is the single spike Finsupp.single a b. This is the
ofPoint/Finsupp.single bridge in its integer-scaled form, shared by the divisor files that
expand a divisor into its point contributions.
A divisor is effective when every coefficient is nonnegative.
Equations
- D.IsEffective = ∀ (x : X), 0 ≤ D.coeff x
Instances For
A nonzero effective divisor has some point with positive coefficient.
Effective Weil divisors form an additive submonoid of the group of all Weil divisors.
Equations
- TauCeti.AlgebraicGeometry.WeilDivisor.effectiveSubmonoid X = { carrier := {D : TauCeti.AlgebraicGeometry.WeilDivisor X | D.IsEffective}, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
Push forward a formal divisor along a map of point sets by summing coefficients over fibres. Geometric pushforward of Weil divisors will specialize this once the relevant point maps and residue-degree factors are available.
Equations
Instances For
The explicit unfolding equation for formal pushforward: pushforward f D is D.mapDomain f.
Use this for manual rewriting rather than as a simp normal form.
The coefficient of the pushed-forward divisor at y is the sum of the coefficients over
the fibre of f above y.
The unweighted degree of a Weil divisor, summing its coefficients. On a curve over a
non-algebraically-closed field, use weightedDegree with residue-field degrees instead.
Instances For
On a nonempty point type the unweighted degree map is surjective: a single point has degree
1, so its integer multiples realise every degree.
The weighted degree of a Weil divisor against an integer-valued weight on points.
For a curve over k, the intended weight is x ↦ [κ(x) : k].
Equations
Instances For
The image of the weighted degree homomorphism is the subgroup of ℤ generated by the
weights. The point divisors generate the free abelian group of Weil divisors and
weightedDegree w (ofPoint x) = w x, so the image is AddSubgroup.closure (Set.range w); being
a subgroup of ℤ, it is d·ℤ for a unique d ≥ 0, the index of the weights.
An effective divisor has nonnegative weighted degree when all weights are nonnegative.
With strictly positive weights on the support, an effective divisor has weighted degree zero iff it is zero.
With strictly positive weights on the support, an effective divisor of weighted degree zero is zero.
With strictly positive weights, an effective divisor has weighted degree zero iff it is zero.
With strictly positive weights, an effective divisor of weighted degree zero is zero.
With strictly positive weights, a nonzero effective divisor has positive weighted degree.
An effective divisor has nonnegative degree.
An effective divisor has degree zero iff it is zero.
An effective divisor of degree zero is zero.
A nonzero effective divisor has positive degree.
The subgroup of divisors of unweighted degree zero.
For a smooth proper curve over an algebraically closed field this is the formal divisor group
whose quotient by principal divisors gives the abstract degree-zero Picard group. Over a
general field, use weightedDegreeZeroSubgroup with residue-field degrees as weights.
Equations
Instances For
An effective divisor lying in the unweighted degree-zero subgroup is zero.
The formal divisor [x] - [y], a basic source of degree-zero divisors.
Equations
Instances For
Point differences telescope additively: [x] - [y] + ([y] - [z]) = [x] - [z].
Reversing a point difference negates it.
Pushforward as a homomorphism on unweighted degree-zero divisors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The subgroup of divisors of weighted degree zero for a weight function on points.
For a curve over a field k, the intended weight is x ↦ [κ(x) : k], giving the formal
degree-zero divisor group before principal divisors are introduced.
Equations
Instances For
The degree-corrected representative of a divisor in the weighted degree-zero divisor group.
For a weight-one base point x₀, this is D - weightedDegree(D) • [x₀], viewed as a
weighted-degree-zero divisor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For strictly positive weights, an effective divisor lying in the weighted degree-zero subgroup is zero.
Degree-corrected point divisors #
The divisor [x] - w(x)[x₀].
For the geometric weight w x = [κ(x) : k] and a rational base point x₀ with w x₀ = 1,
this is the degree-zero divisor underlying the Abel-Jacobi class of the closed point x.
In the algebraically closed/unweighted specialization, this recovers pointDifference x x₀.
Equations
Instances For
The degree-corrected point divisor is [x] minus w x copies of the base point [x₀].
This exposes the definition as a public equation for use across modules.
At the constant weight 1, the degree-corrected point divisor is the usual point
difference. This lets unweighted API reuse the weighted construction.
If the point has weight 1, the degree-corrected point divisor is the usual point
difference.
Coefficients of the degree-corrected point divisor, used as the pointwise simp form of
weightedPointBaseDifference.
The support of [x] - w(x)[x₀] is contained in {x, x₀}.
If the base point has weight 1, the divisor [x₀] - w(x₀)[x₀] is zero.
The weighted degree of [x] - w(x)[x₀] is w(x) * (1 - w(x₀)).
If the base point has weight 1, then [x] - w(x)[x₀] has weighted degree zero.
Changing the base point in the weighted point-base divisor translates it by
w(x) • ([x₀] - [y₀]).
The difference between the weighted point-base divisors for two base points is
w(x) • ([x₀] - [y₀]).
Subtracting two degree-corrected point divisors with the same base point cancels the base term when the two points have equal weight.
Pushforward as a homomorphism on weighted degree-zero divisors, when the target weight pulls back to the source weight.
Equations
- One or more equations did not get rendered due to their size.