@[reducible, inline]

abbrev SmoothCurveDivisors.WeilDivisorGroupCurve (R : Type u_1) [CommRing R] : Type u_1

Weil divisor group of a smooth curve: the free abelian group on the height-one points (closed points) of Spec R.

def SmoothCurveDivisors.countFinite (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) : {v : IsDedekindDomain.HeightOneSpectrum R | FractionalIdeal.count K v I ≠ 0}.Finite

For a fractional ideal I, only finitely many height-one primes appear non-trivially in the factorization.

noncomputable def SmoothCurveDivisors.fwdFun (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ

Divisor of a fractional ideal: sends an invertible fractional ideal I to its formal sum of valuations Σ v_P(I) · [P] over height-one primes P.

noncomputable def SmoothCurveDivisors.bwdFun (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (f : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : (FractionalIdeal (nonZeroDivisors R) K)ˣ

Fractional ideal from a divisor: sends a finitely supported f : v ↦ nᵥ to the product ∏ᵥ Pᵥ^{nᵥ}, the corresponding invertible fractional ideal.

theorem SmoothCurveDivisors.eq_of_count_eq (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {I J : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (hJ : J ≠ 0) (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), FractionalIdeal.count K v I = FractionalIdeal.count K v J) : I = J

Two non-zero fractional ideals with the same valuation at every height-one prime are equal — unique factorization for Dedekind domains.

theorem SmoothCurveDivisors.bwd_fwd (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : bwdFun R K (fwdFun R K I) = I

Left-inverse: rebuilding a fractional ideal from its valuation vector recovers the original ideal.

theorem SmoothCurveDivisors.fwd_bwd (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (f : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : fwdFun R K (bwdFun R K f) = f

Right-inverse: reading off the valuation vector of the ideal ∏ Pᵥ^{nᵥ} gives back (nᵥ).

theorem SmoothCurveDivisors.fwd_mul (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (I J : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : fwdFun R K (I * J) = fwdFun R K I + fwdFun R K J

Multiplicativity of the divisor map: div(I · J) = div(I) + div(J).

noncomputable def SmoothCurveDivisors.weilDivisor_sum_of_points_equiv (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃+ (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

Divisor isomorphism for a smooth curve: the group of invertible fractional ideals (with multiplication) is isomorphic, as an additive group, to the free abelian group on the height-one primes.

noncomputable def SmoothCurveDivisors.weilDivisor_sum_of_points (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ →+ IsDedekindDomain.HeightOneSpectrum R →₀ ℤ

The underlying additive homomorphism of weilDivisor_sum_of_points_equiv.

theorem SmoothCurveDivisors.weilDivisor_sum_of_points_injective (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Injective ⇑(weilDivisor_sum_of_points R K)

Injectivity: distinct invertible fractional ideals have distinct divisors.

theorem SmoothCurveDivisors.weilDivisor_sum_of_points_surjective (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Surjective ⇑(weilDivisor_sum_of_points R K)

Surjectivity: every Weil divisor on a smooth curve is the divisor of some invertible fractional ideal.

noncomputable def SmoothCurveDivisors.weilDivisorClassGroup_iso_pic (R : Type u_1) [CommRing R] [IsDomain R] : ClassGroup R ≃* CommRing.Pic R

Class group ≅ Picard group for a Dedekind domain R: the ideal class group of R agrees with the Picard group of Spec R. This is the algebraic incarnation of "divisor classes = line bundles" on a smooth curve.