Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Image.Basic

The image of the degree map and the degree quotient Cl(X)/Pic⁰ #

This file computes the image of the (weighted) degree homomorphism and identifies the quotient of the divisor class group by the abstract Pic⁰, continuing the Jacobian roadmap's Layer A.

TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic builds, for an OrderSystem S whose principal divisors have weighted degree zero, the descended weighted degree weightedDegreeClass on the class group Cl(X) and its kernel picZero, the abstract Pic⁰. TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Splitting then shows that a weight-one base point makes the descended degree surjective and splits Cl(X) ≃+ picZero × ℤ. That file's docstring flags the general case, where there is no weight-one point: "the image of the weighted degree map is d·ℤ for the index d of the residue degrees". This file supplies exactly that general picture. Everything here is independent of the weight-one splitting theory, so it imports only Principal; the weight-one corollaries built on degreeSection / weightedDegreeClass_surjective live in the downstream TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Image.Splitting, after DegreeSplitting.

The image of the weighted degree on Weil divisors is computed unconditionally, before any principal-divisor hypothesis, by weightedDegree_range in the base TauCeti.AlgebraicGeometry.WeilDivisor.Basic file: since the point divisors generate the free abelian group of Weil divisors and weightedDegree w (ofPoint x) = w x, the image is the subgroup of ℤ generated by the weights,

(weightedDegree w).range = AddSubgroup.closure (Set.range w).

Every subgroup of ℤ is d·ℤ for a unique d ≥ 0, so this is the promised index d. This file descends that computation to the class group: when principal divisors have weighted degree zero, (weightedDegreeClass w h).range = AddSubgroup.closure (Set.range w), and Noether's first isomorphism theorem then identifies the degree quotient

Cl(X) ⧸ Pic⁰ ≃+ (weightedDegreeClass w h).range,

the degree quotient of the class group (the divisor-class analogue of Pic/Pic⁰; no Picard scheme or Néron–Severi construction is built here). When the weights generate all of ℤ — for instance from a weight-one base point — this image is ⊤, recovering Cl(X) ⧸ Pic⁰ ≃+ ℤ and reconciling with the splitting of DegreeSplitting. In the unweighted setting the degree map is already surjective on a nonempty point type.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Degree" and "Pic⁰ X = ker deg (as an abstract group)", by computing the image of the degree map and identifying the degree quotient of the class group with it. It reuses Tau Ceti's WeilDivisor and OrderSystem API together with Mathlib's AddSubgroup.closure and first-isomorphism (QuotientAddGroup.quotientKerEquivRange / quotientKerEquivOfSurjective) machinery; no external mathematics is vendored.

The image of the degree on the class group #

source
theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_range {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) :
(weightedDegreeClass w h).range = AddSubgroup.closure (Set.range w)

The image of the descended weighted degree on the class group is the same subgroup of ℤ generated by the weights. The class map divisorClass is surjective, so it does not change the image of the degree; the value is weightedDegree_range transported through the quotient.

source
theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_range_eq_top {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (hw : AddSubgroup.closure (Set.range w) = ⊤) :
(weightedDegreeClass w h).range = ⊤

The descended weighted degree hits all of ℤ exactly when the weights generate ℤ, i.e. AddSubgroup.closure (Set.range w) = ⊤. This is the general surjectivity criterion; a weight-one base point is the special case weightedDegreeClass_range_eq_top_of_weight_one, but weights such as 2 and 3 already generate ℤ with no weight-one point.

The degree quotient Cl(X)/Pic⁰ #

source
noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivDegreeRange {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) :
S.ClassGroup ⧸ picZero w h ≃+ ↥(weightedDegreeClass w h).range

The degree quotient. The class group modulo the abstract Pic⁰ is isomorphic to the image of the degree, Cl(X) ⧸ Pic⁰ ≃+ (weightedDegreeClass w h).range. This is Noether's first isomorphism theorem for the descended weighted degree, whose kernel is picZero by definition; the image is AddSubgroup.closure (Set.range w) by weightedDegreeClass_range. It is the degree quotient of the class group, the divisor-class analogue of Pic/Pic⁰; no Picard scheme is constructed here.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_classGroupQuotientPicZeroEquivDegreeRange_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (c : S.ClassGroup) :
    ↑((S.classGroupQuotientPicZeroEquivDegreeRange w h) ↑c) = (weightedDegreeClass w h) c
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivDegreeRange_symm_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (c : S.ClassGroup) :
    (S.classGroupQuotientPicZeroEquivDegreeRange w h).symm ⟨(weightedDegreeClass w h) c, ⋯⟩ = ↑c
    source
    noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivInt {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (hsurj : Function.Surjective ⇑(weightedDegreeClass w h)) :
    S.ClassGroup ⧸ picZero w h ≃+ ℤ

    The degree quotient at a surjective degree. When the descended weighted degree is surjective — equivalently when the weights generate ℤ, see weightedDegreeClass_range_eq_top — the class group modulo the abstract Pic⁰ is ℤ, Cl(X) ⧸ Pic⁰ ≃+ ℤ. A weight-one base point is the special case classGroupQuotientPicZeroEquivIntOfWeightOne.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivInt_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (hsurj : Function.Surjective ⇑(weightedDegreeClass w h)) (c : S.ClassGroup) :
      (S.classGroupQuotientPicZeroEquivInt w h hsurj) ↑c = (weightedDegreeClass w h) c
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivInt_symm_weightedDegreeClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) (hsurj : Function.Surjective ⇑(weightedDegreeClass w h)) (c : S.ClassGroup) :
      (S.classGroupQuotientPicZeroEquivInt w h hsurj).symm ((weightedDegreeClass w h) c) = ↑c

      The inverse of classGroupQuotientPicZeroEquivInt sends weightedDegreeClass w h c back to the class [c]. Since weightedDegreeClass w h is surjective this characterises the inverse on all of ℤ, so downstream code need not unfold the choice-based right inverse.