The kernel of the principal-divisor map

This file records the exactness at the rational-function side of the formal divisor-class sequence built in TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic.

For an order system S : OrderSystem X G, the homomorphism S.principalHom : G →+ WeilDivisor X sends a function to its principal divisor. Its kernel is the subgroup of functions with zero order at every point. Quotienting G by this kernel gives the abstract group of principal divisors, canonically identified with S.principalSubgroup.

In geometric applications, G is the additive form of the multiplicative group of a function field. After additional geometric input identifying the zero-principal-divisor functions with constants, this quotient specializes to rational functions modulo constants, embedded as principal divisors before taking the divisor class quotient.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, specifically the "principal divisors" and "Cl(X) ≅ Pic X" prerequisite lane: the class group is the quotient by principal divisors, and this file packages the source-side quotient that maps onto that subgroup. It reuses Tau Ceti's OrderSystem.principalHom API and Mathlib's first isomorphism theorem for quotient groups; no external mathematics is vendored.

The kernel of the principal-divisor map

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalKernel {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : AddSubgroup G

The subgroup of functions whose principal divisor is zero.

In geometric applications this is the subgroup quotiented out before passing from rational functions to principal divisors. Identifying it with constants requires additional geometric input, such as a global-units or constant-field theorem.

Equations

• S.principalKernel = S.principalHom.ker

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_principalKernel {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {g : G} : g ∈ S.principalKernel ↔ S.principalDivisor g = 0

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_principalKernel_iff_forall_ord_eq_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {g : G} : g ∈ S.principalKernel ↔ ∀ (x : X), (S.ord x) g = 0

A function has zero principal divisor exactly when all of its orders vanish.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.zero_mem_principalKernel {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : 0 ∈ S.principalKernel

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalKernel_eq_bot_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.principalKernel = ⊥ ↔ Function.Injective ⇑S.principalHom

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalHom_injective_of_principalKernel_eq_bot {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (h : S.principalKernel = ⊥) : Function.Injective ⇑S.principalHom

If the only function with zero principal divisor is zero, the principal-divisor map is injective.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalKernel_eq_bot_of_principalHom_injective {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (h : Function.Injective ⇑S.principalHom) : S.principalKernel = ⊥

An injective principal-divisor map has trivial kernel.

Principal divisors as a quotient of functions

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.PrincipalFunctionClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : Type u_2

The quotient of the function group by functions with zero principal divisor.

In geometric applications this is the group of rational functions modulo the subgroup with zero principal divisor. Under further hypotheses identifying that subgroup with the base-field constants, it specializes to the usual rational-functions-modulo-constants group.

Equations

• S.PrincipalFunctionClass = (G ⧸ S.principalKernel)

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.PrincipalFunctionClass →+ WeilDivisor X

The principal divisor associated to a function class, as a homomorphism into all Weil divisors.

Equations

• S.principalFunctionClassDivisor = QuotientAddGroup.kerLift S.principalHom

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.principalFunctionClassDivisor ↑g = S.principalDivisor g

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor_injective {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : Function.Injective ⇑S.principalFunctionClassDivisor

The map from function classes to principal divisors is injective.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor_mem_principalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (q : S.PrincipalFunctionClass) : S.principalFunctionClassDivisor q ∈ S.principalSubgroup

Every divisor attached to a function class is principal.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor_range {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.principalFunctionClassDivisor.range = S.principalSubgroup

The image of function classes in all Weil divisors is exactly the subgroup of principal divisors.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassEquivPrincipalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) : S.PrincipalFunctionClass ≃+ ↥S.principalSubgroup

The quotient of functions by the zero-principal-divisor subgroup is canonically equivalent to the subgroup of principal divisors.

Equations

• S.principalFunctionClassEquivPrincipalSubgroup = (QuotientAddGroup.quotientKerEquivRange S.principalHom).trans (AddEquiv.addSubgroupCongr ⋯)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassEquivPrincipalSubgroup_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (g : G) : S.principalFunctionClassEquivPrincipalSubgroup ↑g = ⟨S.principalDivisor g, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_principalFunctionClassEquivPrincipalSubgroup {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (q : S.PrincipalFunctionClass) : ↑(S.principalFunctionClassEquivPrincipalSubgroup q) = S.principalFunctionClassDivisor q

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalFunctionClassDivisor_eq_zero_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {q : S.PrincipalFunctionClass} : S.principalFunctionClassDivisor q = 0 ↔ q = 0

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.principalDivisor_eq_iff_mk_eq_mk {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {g h : G} : S.principalDivisor g = S.principalDivisor h ↔ ↑g = ↑h

Equality of principal divisors is equality of the corresponding function classes.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mk_eq_mk_iff_principalDivisor_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {g h : G} : ↑g = ↑h ↔ S.principalDivisor g = S.principalDivisor h

Two functions define the same class modulo the zero-principal-divisor subgroup exactly when their principal divisors are equal.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mk_eq_zero_iff_principalDivisor_eq_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {g : G} : ↑g = 0 ↔ S.principalDivisor g = 0

A function class is zero exactly when the representative has zero principal divisor.