@[reducible, inline]

abbrev DivisorsPicard.WeilDivisorGroup (Y : Type u_1) : Type u_1

The Weil divisor group DW(Y) on Y (Def 29, Lec 14): finitely supported ℤ-valued formal sums on Y, viewed as the free abelian group on points of Y.

def DivisorsPicard.WeilDivisor.IsEffective {Y : Type u_1} (D : WeilDivisorGroup Y) : Prop

A Weil divisor is effective when all coefficients are non-negative.

theorem DivisorsPicard.pic_eq_divC_mod_principal (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] {I : Ideal A} (hI : I ∈ nonZeroDivisors (Ideal A)) : ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I

An ideal class in the class group is trivial iff the ideal is principal: a concrete realization of Pic = DC / principals (Cor 19, Lec 15) for Dedekind domains.

def DivisorsPicard.CartierDivisor.LinearlyEquivalent (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (I J : ↥(nonZeroDivisors (Ideal A))) : Prop

Two Cartier divisors (i.e. non-zero ideals) are linearly equivalent when they represent the same class in the Picard group.

theorem DivisorsPicard.ufd_dedekind_is_pid (R : Type u_1) [CommRing R] [IsDedekindDomain R] [UniqueFactorizationMonoid R] : IsPrincipalIdealRing R

A UFD that is also a Dedekind domain is a PID.

theorem DivisorsPicard.classGroup_subsingleton_of_ufd_dedekind (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] [UniqueFactorizationMonoid R] : Subsingleton (ClassGroup R)

For a Dedekind domain that is also a UFD, the ideal class group is trivial, i.e. Pic is trivial: every ideal is principal.

theorem DivisorsPicard.ufd_prime_contains_prime (R : Type u_1) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (P : Ideal R) [hP : P.IsPrime] (hne : P ≠ ⊥) : ∃ p ∈ P, Prime p

In a UFD, every non-zero prime ideal contains a prime element.

noncomputable def DivisorsPicard.cartierToWeilDivisor (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) : WeilDivisorGroup (IsDedekindDomain.HeightOneSpectrum R)

The Cartier-to-Weil divisor map: send a fractional ideal to its valuation data, recording for each height-one prime the order of vanishing.

theorem DivisorsPicard.weilCartierFactorization (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} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (cartierToWeilDivisor R K I) v = I

Reconstruct a non-zero fractional ideal from its Weil divisor data via the finite product over height-one primes raised to the orders of vanishing.

noncomputable def DivisorsPicard.cartierToWeilFun (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)ˣ) : WeilDivisorGroup (IsDedekindDomain.HeightOneSpectrum R)

Restriction of the Cartier-to-Weil map to invertible fractional ideals.

noncomputable def DivisorsPicard.weilToCartierFun (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (D : WeilDivisorGroup (IsDedekindDomain.HeightOneSpectrum R)) : (FractionalIdeal (nonZeroDivisors R) K)ˣ

The Weil-to-Cartier map: build an invertible fractional ideal as the product of prime ideals raised to the orders specified by the Weil divisor.

noncomputable def DivisorsPicard.cartierWeilIso (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃* Multiplicative (WeilDivisorGroup (IsDedekindDomain.HeightOneSpectrum R))

The multiplicative isomorphism between invertible fractional ideals (the Cartier divisor group) and the free abelian group on height-one primes (the Weil divisor group), proving DC ≃ DW for a Dedekind domain.

noncomputable def DivisorsPicard.picIsomCartierQuotPrincipal (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ClassGroup R ≃* (FractionalIdeal (nonZeroDivisors R) K)ˣ ⧸ (toPrincipalIdeal R K).range

Pic(R) = DC(R) / principals: the class group is isomorphic to the quotient of invertible fractional ideals by principal fractional ideals (Cor 19, Lec 15).

def DivisorsPicard.IsLocallyFactorial (R : Type u_1) [CommRing R] [IsDomain R] : Prop

A ring is locally factorial when each localization at a prime ideal is a UFD; the hypothesis under which Weil and Cartier divisors agree.

theorem DivisorsPicard.dvr_is_ufd (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : UniqueFactorizationMonoid R

A discrete valuation ring is a UFD.

theorem DivisorsPicard.dvr_is_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsPrincipalIdealRing R

A discrete valuation ring is a PID.

theorem DivisorsPicard.dedekind_isLocallyFactorial (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] : IsLocallyFactorial R

Every Dedekind domain is locally factorial: localizations at primes are DVRs (non-zero primes) or fields (the zero prime), both of which are UFDs.

instance DivisorsPicard.dedekind_localization_dvr (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (P : Ideal R) [P.IsPrime] (hP : P ≠ ⊥) : IsDiscreteValuationRing (Localization.AtPrime P)

Localizing a Dedekind domain at a non-zero prime gives a DVR.

instance DivisorsPicard.dedekind_localization_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (P : Ideal R) [P.IsPrime] (hP : P ≠ ⊥) : IsPrincipalIdealRing (Localization.AtPrime P)

Localizing a Dedekind domain at a non-zero prime gives a PID.

theorem DivisorsPicard.ufd_height_one_prime_isPrincipal (R : Type u_1) [CommRing R] [UniqueFactorizationMonoid R] (P : Ideal R) [hP : P.IsPrime] (hne : P ≠ ⊥) (hmin : ∀ (Q : Ideal R) [Q.IsPrime], Q ≤ P → Q ≠ ⊥ → Q = P) : Submodule.IsPrincipal P

In a UFD, every minimal non-zero prime (i.e. height-one prime) is principal, generated by a prime element.

theorem DivisorsPicard.ideal_locally_principal_of_locally_factorial (R : Type u_1) [CommRing R] [IsDomain R] (hlf : IsLocallyFactorial R) (I : Ideal R) [hI : I.IsPrime] (hIne : I ≠ ⊥) (hht1 : ∀ (Q : Ideal R) [Q.IsPrime], Q ≤ I → Q ≠ ⊥ → Q = I) (P : Ideal R) [hPprime : P.IsPrime] : Submodule.IsPrincipal (Ideal.map (algebraMap R (Localization.AtPrime P)) I)

Under local factoriality, a height-one prime ideal becomes principal after localizing at any prime: this is the local condition relating Weil and Cartier divisors.

theorem DivisorsPicard.ideal_locally_principal_dedekind (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (I P : Ideal R) [P.IsPrime] (hP : P ≠ ⊥) : Submodule.IsPrincipal (Ideal.map (algebraMap R (Localization.AtPrime P)) I)

Any ideal in a Dedekind domain becomes principal after localizing at a non-zero prime, since the localization is a DVR (hence PID).

theorem DivisorsPicard.classGroup_measures_weil_cartier_obstruction (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : Ideal R) (hI : I ∈ nonZeroDivisors (Ideal R)) : ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I

The class group measures the obstruction between Weil and Cartier divisors: a non-zero ideal represents the trivial class iff it is already principal.

theorem DivisorsPicard.pic_affine_line_trivial (k : Type u_1) [Field k] : Fintype.card (ClassGroup (Polynomial k)) = 1

The Picard group of the affine line A¹_k = Spec k[x] is trivial, since k[x] is a PID.

instance DivisorsPicard.mvPolynomial_ufd (k : Type u_1) [Field k] (σ : Type u_2) : UniqueFactorizationMonoid (MvPolynomial σ k)

Polynomial rings in arbitrarily many variables over a field are UFDs.

theorem DivisorsPicard.power_series_ufd_of_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : UniqueFactorizationMonoid (PowerSeries R)

The power series ring over a PID is a UFD.

theorem DivisorsPicard.classNumber_one_of_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : Fintype.card (ClassGroup R) = 1

The class number of a PID is one: every PID has trivial Picard group.

theorem DivisorsPicard.classGroup_trivial_iff_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] [Fintype (ClassGroup R)] : Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R

For a Dedekind domain, the class group is trivial iff the ring is a PID.

theorem DivisorsPicard.fg_torsionfree_free_of_pid (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [NoZeroSMulDivisors R M] : Module.Free R M

Finitely generated torsion-free modules over a PID are free: a key step in classifying coherent sheaves on A¹ and in proving Grothendieck-Birkhoff.

@[reducible, inline]

abbrev DivisorsPicard.CartierDivisorGroupUnits (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Type u_2

The Cartier divisor group DC(A) (Def 30, Lec 15), realized as the units of the monoid of fractional ideals.

@[reducible, inline]

abbrev DivisorsPicard.CartierDivisorGroup' (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Type u_2

Alternative spelling of CartierDivisorGroupUnits over a general domain.

def DivisorsPicard.principalDivisorMap_Def31 (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Kˣ →* (FractionalIdeal (nonZeroDivisors A) K)ˣ

The principal divisor map (Def 31, Lec 15) sending a unit of K to the fractional ideal it spans; its image is the subgroup of principal divisors.

def DivisorsPicard.PrincipalCartierDivisors (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Subgroup (FractionalIdeal (nonZeroDivisors A) K)ˣ

The subgroup of principal Cartier divisors, i.e. the image of the principal divisor map.

theorem DivisorsPicard.mem_principalCartierDivisors_iff (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (D : (FractionalIdeal (nonZeroDivisors A) K)ˣ) : D ∈ PrincipalCartierDivisors A K ↔ ∃ (x : K), FractionalIdeal.spanSingleton (nonZeroDivisors A) x = ↑D

Membership criterion: a Cartier divisor is principal iff some element of K spans it as a singleton fractional ideal.

@[reducible, inline]

abbrev DivisorsPicard.PicardGroupQuot (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Type u_2

The Picard group as the quotient DC / principals, the abelian group from Cor 19.