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

A ring R is locally factorial if all of its localizations at prime ideals are unique factorization monoids.

structure LocallyFactorialDivisors.HeightOnePrime (R : Type u_1) [CommRing R] [IsDomain R] : Type u_1

A height-one prime is a nonzero prime ideal (used for Weil divisors).

• asIdeal : Ideal R
• isPrime : self.asIdeal.IsPrime
• ne_bot : self.asIdeal ≠ ⊥

theorem LocallyFactorialDivisors.HeightOnePrime.ext {R : Type u_1} {inst✝ : CommRing R} {inst✝¹ : IsDomain R} {x y : HeightOnePrime R} (asIdeal : x.asIdeal = y.asIdeal) : x = y

theorem LocallyFactorialDivisors.HeightOnePrime.ext_iff {R : Type u_1} {inst✝ : CommRing R} {inst✝¹ : IsDomain R} {x y : HeightOnePrime R} : x = y ↔ x.asIdeal = y.asIdeal

@[reducible, inline]

abbrev LocallyFactorialDivisors.WeilDivisorGroup (R : Type u_1) [CommRing R] [IsDomain R] : Type u_1

The group of Weil divisors, formal ℤ-linear combinations of height-one primes.

@[reducible, inline]

abbrev LocallyFactorialDivisors.CartierDivisorGroup (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Type u_2

The Cartier divisor group, identified with the unit group of fractional ideals in the fraction field.

def LocallyFactorialDivisors.heightOnePrimeEquiv (R : Type u_1) [CommRing R] [IsDomain R] : HeightOnePrime R ≃ IsDedekindDomain.HeightOneSpectrum R

Identification between HeightOnePrime and Mathlib's HeightOneSpectrum.

def LocallyFactorialDivisors.weilDivisorEquiv (R : Type u_1) [CommRing R] [IsDomain R] : WeilDivisorGroup R ≃+ (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

The additive equivalence between the local WeilDivisorGroup and the version indexed by Mathlib's HeightOneSpectrum.

theorem LocallyFactorialDivisors.weil_iso_cartier_of_locally_factorial (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (hlf : IsLocallyFactorial R) : Nonempty (CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R))

For a locally factorial domain, the Cartier divisor group is isomorphic to the multiplicative form of the Weil divisor group (Thm 15.1, Lec 15): the map DW ↔ DC is an isomorphism.

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

Every Dedekind domain is locally factorial, since localizations at primes are DVRs (and DVRs are UFDs).

theorem LocallyFactorialDivisors.smooth_isLocallyFactorial (R : Type u_1) [CommRing R] [IsDomain R] (hsmooth : ∀ (P : Ideal R) [inst : P.IsPrime], IsRegularLocalRing (Localization.AtPrime P)) : IsLocallyFactorial R

If every localization at a prime is a regular local ring, then R is locally factorial (Auslander–Buchsbaum).

noncomputable def LocallyFactorialDivisors.fractionalIdealToWeil {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 →₀ ℤ

Convert a fractional ideal to a Weil divisor by taking valuations at each height-one prime.

@[simp]

theorem LocallyFactorialDivisors.fractionalIdealToWeil_apply {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) (v : IsDedekindDomain.HeightOneSpectrum R) : (fractionalIdealToWeil K I) v = FractionalIdeal.count K v I

The value of fractionalIdealToWeil at a prime v is the valuation count.

noncomputable def LocallyFactorialDivisors.cartierToWeil {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ

The Cartier-to-Weil map: send a Cartier divisor (a unit fractional ideal) to its associated Weil divisor.

@[simp]

theorem LocallyFactorialDivisors.cartierToWeil_apply {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (v : IsDedekindDomain.HeightOneSpectrum R) : (cartierToWeil K u) v = FractionalIdeal.count K v ↑u

Pointwise formula for cartierToWeil.

theorem LocallyFactorialDivisors.cartierToWeil_one {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : cartierToWeil K 1 = 0

The unit Cartier divisor maps to the zero Weil divisor.

theorem LocallyFactorialDivisors.cartierToWeil_mul {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u₁ u₂ : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : cartierToWeil K (u₁ * u₂) = cartierToWeil K u₁ + cartierToWeil K u₂

cartierToWeil is multiplicative: product becomes sum of valuations.

theorem LocallyFactorialDivisors.cartierToWeil_inv {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : cartierToWeil K u⁻¹ = -cartierToWeil K u

Inverting a Cartier divisor negates its associated Weil divisor.

theorem LocallyFactorialDivisors.cartierToWeil_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 (cartierToWeil K)

The Cartier-to-Weil map is injective: a fractional ideal is determined by its collection of valuations.

noncomputable def LocallyFactorialDivisors.weilToCartierIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : FractionalIdeal (nonZeroDivisors R) K

Construct a fractional ideal from a Weil divisor by taking the product of prime power factors.

theorem LocallyFactorialDivisors.height_one_coe_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : ↑v.asIdeal ≠ 0

A nonzero height-one prime ideal gives a nonzero fractional ideal.

theorem LocallyFactorialDivisors.weilToCartierIdeal_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : weilToCartierIdeal K D ≠ 0

The fractional ideal coming from a Weil divisor is nonzero.

theorem LocallyFactorialDivisors.cartierToWeil_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 (cartierToWeil K)

The Cartier-to-Weil map is surjective: every Weil divisor comes from a Cartier divisor.

theorem LocallyFactorialDivisors.weil_eq_cartier_dedekind {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Bijective (cartierToWeil K)

On a Dedekind domain, the Cartier-to-Weil map is a bijection.

noncomputable def LocallyFactorialDivisors.cartierToWeilMonoidHom {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 (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

The Cartier-to-Weil map packaged as a monoid homomorphism into the multiplicative form of the Weil divisor group.

noncomputable def LocallyFactorialDivisors.cartierToWeilMulEquiv {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (_hlf : IsLocallyFactorial R) : (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃* Multiplicative (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

The Cartier-to-Weil map upgraded to a multiplicative equivalence, assuming local factoriality.

theorem LocallyFactorialDivisors.weil_iso_cartier_of_dedekind {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (hlf : IsLocallyFactorial R) : Nonempty (CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R))

Cartier and Weil divisor groups are isomorphic on a Dedekind (locally factorial) domain.

@[reducible, inline]

abbrev LocallyFactorialDivisors.PicardGroup (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Type u_2

The Picard group: Cartier divisors modulo principal Cartier divisors.

noncomputable def LocallyFactorialDivisors.picard_iso_classGroup (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ClassGroup R ≃* PicardGroup R K

The Picard group is naturally isomorphic to the ideal class group.

noncomputable def LocallyFactorialDivisors.PrincipalWeilDivisors (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (e : CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R)) : Subgroup (Multiplicative (WeilDivisorGroup R))

Principal Weil divisors are the image of principal Cartier divisors under the chosen isomorphism e.

@[reducible, inline]

abbrev LocallyFactorialDivisors.WeilDivisorClassGroup (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (e : CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R)) : Type u_1

The Weil divisor class group, Weil divisors modulo principal Weil divisors.

noncomputable def LocallyFactorialDivisors.pic_iso_cl (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (e : CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R)) : PicardGroup R K ≃* WeilDivisorClassGroup R K e

The Picard group is isomorphic to the Weil divisor class group via e.

theorem LocallyFactorialDivisors.pic_iso_cl_of_locally_factorial (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (hlf : IsLocallyFactorial R) : ∃ (e : CartierDivisorGroup R K ≃* Multiplicative (WeilDivisorGroup R)), Nonempty (ClassGroup R ≃* WeilDivisorClassGroup R K e)

For a locally factorial domain, the class group is isomorphic to the Weil divisor class group via the Cartier–Weil identification (Thm 15.1, Lec 15).

theorem locally_factorial_height_one_locally_principal_aux (R : Type u_1) [CommRing R] [IsDomain R] (hlf : LocallyFactorialDivisors.IsLocallyFactorial R) (I : Ideal R) (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)

Auxiliary version: in a locally factorial domain, a nonzero ideal whose only nonzero prime subideal is itself becomes principal in every localization at a prime.

theorem locally_factorial_height_one_locally_principal (R : Type u_1) [CommRing R] [IsDomain R] (hlf : LocallyFactorialDivisors.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)

In a locally factorial domain, any height-one prime becomes principal after localization at any prime.