The divisor class group of a Dedekind domain is its ideal class group

For a Dedekind domain R with fraction field K, TauCeti.AlgebraicGeometry.WeilDivisor.Dedekind.Basic packages the height-one spectrum of R as the points of an affine curve and the order of vanishing of a rational function as the order system OrderSystem.ofDedekindDomain R K; its class group (OrderSystem.ofDedekindDomain R K).ClassGroup is the free Weil-divisor group on the height-one primes modulo principal divisors. TauCeti.AlgebraicGeometry.WeilDivisor.FractionalIdealDivisor.Basic adds the Cartier side, the isomorphism fractionalIdealDivisorAddEquiv between invertible fractional ideals and Weil divisors, and records that it carries principal fractional ideals to principal divisors. Both files explicitly leave the quotient-level comparison open. This file supplies it.

The isomorphism fractionalIdealDivisorAddEquiv R K sends the subgroup of principal fractional ideals (toPrincipalIdeal R K).range onto the subgroup of principal divisors, so it descends to an isomorphism of quotients

classGroupAddEquiv : (OrderSystem.ofDedekindDomain R K).ClassGroup ≃+ Additive (ClassGroup R),

the Weil-divisor divisor class group of the affine Dedekind curve identified with Mathlib's ideal class group ClassGroup R. It is characterized by sending the class of the Weil divisor of an invertible fractional ideal I to the ideal class of I, and its inverse sends the ideal class of I back to the divisor class of the divisor of I; in particular the class of the point divisor [v] of a height-one prime v is the ideal class of v.

This is the affine, scheme-free form of the Jacobian roadmap's Cl(X) ≅ Pic X dictionary (TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "the dictionaries Cartier ≃ line bundles ... Cl(X) ≅ Pic X"), realized for the Dedekind model before the global Picard scheme exists. It reuses Tau Ceti's fractionalIdealDivisorAddEquiv and OrderSystem.ofDedekindDomain API and Mathlib's ClassGroup R, ClassGroup.equiv (independence of the fraction field) and QuotientAddGroup.congr; no external mathematics is vendored.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : (OrderSystem.ofDedekindDomain R K).ClassGroup ≃+ Additive (ClassGroup R)

The divisor class group of the affine Dedekind curve is the ideal class group.

For a Dedekind domain R with fraction field K, the Weil-divisor divisor class group (OrderSystem.ofDedekindDomain R K).ClassGroup of the height-one spectrum is isomorphic to the ideal class group ClassGroup R, via the isomorphism fractionalIdealDivisorAddEquiv R K of invertible fractional ideals with Weil divisors descended to the quotient by principal divisors/ideals. This is the affine Cl(X) ≅ Pic X of the Jacobian roadmap. See classGroupAddEquiv_divisorClass_fractionalIdealDivisor and classGroupAddEquiv_symm_ofMul_mk for the characterizing formulas.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv_divisorClass_fractionalIdealDivisor {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (classGroupAddEquiv R K) ((OrderSystem.ofDedekindDomain R K).divisorClass ((fractionalIdealDivisor R K) (Additive.ofMul I))) = Additive.ofMul ((ClassGroup.mk K) I)

The class group isomorphism sends the class of the Weil divisor of an invertible fractional ideal I to the ideal class of I. Together with the surjectivity of fractionalIdealDivisor and of divisorClass this pins down classGroupAddEquiv on every element.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv_symm_ofMul_mk {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (classGroupAddEquiv R K).symm (Additive.ofMul ((ClassGroup.mk K) I)) = (OrderSystem.ofDedekindDomain R K).divisorClass ((fractionalIdealDivisor R K) (Additive.ofMul I))

The inverse of the class group isomorphism sends the ideal class of an invertible fractional ideal I to the divisor class of the Weil divisor of I. This is the canonical inverse formula, dual to classGroupAddEquiv_divisorClass_fractionalIdealDivisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv_divisorClass {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (D : WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : (classGroupAddEquiv R K) ((OrderSystem.ofDedekindDomain R K).divisorClass D) = Additive.ofMul ((ClassGroup.mk K) (Additive.toMul ((fractionalIdealDivisorAddEquiv R K).symm D)))

The class group isomorphism on a general divisor class: the class of a Weil divisor D maps to the ideal class of the invertible fractional ideal ∏_v v ^ (D v) recovered from D.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv_divisorClass_ofPoint {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : (classGroupAddEquiv R K) ((OrderSystem.ofDedekindDomain R K).divisorClass (ofPoint v)) = Additive.ofMul ((ClassGroup.mk K) (Units.mk0 ↑v.asIdeal ⋯))

Non-vacuity: the class group isomorphism sends the class of the point divisor [v] of a height-one prime v to the ideal class of v, viewed as an invertible fractional ideal.