The degree-zero divisor quotient model of abstract `Pic⁰` #

This file adds a small Layer A bridge for the Jacobian roadmap. The file TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic defines the abstract divisor class group Cl(X) of an order system and defines Pic⁰ as the kernel of the descended weighted degree on Cl(X). Classically, the same group is also described as degree-zero divisors modulo principal divisors. This file identifies those two descriptions.

For an order system S whose principal divisors have weighted degree zero, the natural map from weighted-degree-zero divisors to S.picZero w h,

D ↦ [D],

is surjective, and its kernel is the subgroup of weighted-degree-zero divisors whose underlying divisor is principal. The first isomorphism theorem then gives

(weighted-degree-zero divisors) / (principal divisors) ≃+ Pic⁰.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, specifically the item "Degree. ... Then Pic⁰ X = ker deg (as an abstract group; the functorial Pic⁰ is defined in Layer D)." No external mathematics is vendored; the proof uses Tau Ceti's existing WeilDivisor/OrderSystem API and Mathlib's quotient-group first isomorphism theorem.

Weighted degree-zero divisors modulo principal divisors #

source

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalSubgroupOfWeightedDegreeZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) :

AddSubgroup ↥(weightedDegreeZeroSubgroup w)

Principal divisors inside the weighted-degree-zero divisor group: a degree-zero divisor belongs to this subgroup exactly when its underlying divisor is principal.

Equations

S.principalSubgroupOfWeightedDegreeZero w = AddSubgroup.comap (TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegreeZeroSubgroup w).subtype S.principalSubgroup

Instances For

source

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_principalSubgroupOfWeightedDegreeZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} {D : ↥(weightedDegreeZeroSubgroup w)} :

D ∈ S.principalSubgroupOfWeightedDegreeZero w ↔ ↑D ∈ S.principalSubgroup

source

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroClassHom {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (w : X → ℤ) (h : S.IsWeightedDegreeZero w) :

↥(weightedDegreeZeroSubgroup w) →+ ↥(picZero w h)

The natural map from weighted-degree-zero divisors to the abstract degree-zero divisor class group Pic⁰, sending a divisor to its divisor class.

Equations

S.weightedDegreeZeroClassHom w h = { toFun := fun (D : ↥(TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegreeZeroSubgroup w)) => ⟨S.divisorClass ↑D, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_weightedDegreeZeroClassHom_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) (D : ↥(weightedDegreeZeroSubgroup w)) :

↑((S.weightedDegreeZeroClassHom w h) D) = S.divisorClass ↑D

source

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroClassHom_apply {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) (D : ↥(weightedDegreeZeroSubgroup w)) :

(S.weightedDegreeZeroClassHom w h) D = ⟨S.divisorClass ↑D, ⋯⟩

source

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroClassHom_surjective {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) :

Function.Surjective ⇑(S.weightedDegreeZeroClassHom w h)

The natural map from weighted-degree-zero divisors to Pic⁰ is surjective: every degree-zero divisor class has a weighted-degree-zero representative.

source

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroClassHom_eq_zero_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) {D : ↥(weightedDegreeZeroSubgroup w)} :

(S.weightedDegreeZeroClassHom w h) D = 0 ↔ ↑D ∈ S.principalSubgroup

source

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeZeroClassHom_ker {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) :

(S.weightedDegreeZeroClassHom w h).ker = S.principalSubgroupOfWeightedDegreeZero w

The kernel of the map from weighted-degree-zero divisors to Pic⁰ is exactly the subgroup of principal divisors inside the weighted-degree-zero divisor group.

source