The degree image and quotient at a weight-one base point

This file gives the weight-one counterparts of the general degree-image and degree-quotient results of TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Image.Basic, using the splitting theory of TauCeti.AlgebraicGeometry.WeilDivisor.Degree.Splitting. These corollaries specialise to a weight-one base point: the range statement is derived from the general degree-image API, while the quotient equivalence keeps the explicit inverse supplied by the splitting section.

DegreeImage computes the image of the descended weighted degree unconditionally, (weightedDegreeClass w h).range = AddSubgroup.closure (Set.range w), and identifies the degree quotient Cl(X) ⧸ Pic⁰ with that image. Those results are independent of the weight-one splitting; this file adds the corollaries that do use it. DegreeSplitting shows that a weight-one base point makes the descended weighted degree surjective, with the degree section n ↦ n • [x₀] as an explicit right inverse. So:

• weightedDegreeClass_range_eq_top_of_weight_one restates surjectivity at the AddSubgroup level as (weightedDegreeClass w h).range = ⊤, the weight-one special case of the general weightedDegreeClass_range_eq_top;
• classGroupQuotientPicZeroEquivIntOfWeightOne builds Cl(X) ⧸ Pic⁰ ≃+ ℤ from that right inverse, giving an explicit inverse and, together with DegreeSplitting's Cl(X) ≃+ picZero × ℤ, exhibiting the degree as the projection to the ℤ factor.

This advances the same TauCetiRoadmap/JacobianChallenge/README.md, Layer A targets as DegreeImage; it reuses DegreeImage's image computation, DegreeSplitting's degreeSection / weightedDegreeClass_surjective, and Mathlib's QuotientAddGroup.quotientKerEquivOfRightInverse.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_range_eq_top_of_weight_one {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) : (weightedDegreeClass w h).range = ⊤

With a weight-one base point the descended weighted degree hits all of ℤ; this is the weight-one specialization of weightedDegreeClass_range_eq_top.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivIntOfWeightOne {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) : S.ClassGroup ⧸ picZero w h ≃+ ℤ

The degree quotient at a weight-one base point. With a weight-one base point the degree section n ↦ n • [x₀] is a genuine right inverse of the descended weighted degree, so the class group modulo the abstract Pic⁰ is ℤ, Cl(X) ⧸ Pic⁰ ≃+ ℤ, with an explicit inverse. Together with DegreeSplitting's Cl(X) ≃+ picZero × ℤ this exhibits the degree as the projection to the ℤ factor.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivIntOfWeightOne_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (c : S.ClassGroup) : (S.classGroupQuotientPicZeroEquivIntOfWeightOne w h hx₀) ↑c = (weightedDegreeClass w h) c

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupQuotientPicZeroEquivIntOfWeightOne_symm_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) {x₀ : X} (hx₀ : w x₀ = 1) (n : ℤ) : (S.classGroupQuotientPicZeroEquivIntOfWeightOne w h hx₀).symm n = ↑((S.degreeSection x₀) n)