@[reducible, inline]

abbrev WeilDivisor.Group (Y : Type u_1) : Type u_1

Group of Weil divisors on a "set of codim-1 subvarieties" Y (Def 29, Lec 14): the free abelian group on Y, modelled as finitely supported ℤ-valued functions.

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

A Weil divisor is effective iff all of its coefficients are nonnegative.

noncomputable def WeilDivisor.single {Y : Type u_1} (D : Y) (n : ℤ) : Group Y

The Weil divisor n · [D] consisting of n copies of a single codim-1 subvariety D.

def WeilDivisor.coeff {Y : Type u_1} (D : Group Y) (y : Y) : ℤ

The coefficient of a Weil divisor D along a codim-1 subvariety y.

noncomputable def WeilDivisor.equivFreeAbelianGroup (Y : Type u_1) : Group Y ≃+ FreeAbelianGroup Y

Identification of the Weil divisor group with the abstract free abelian group on Y.

@[reducible, inline]

abbrev WeilDivisor.DedekindGroup (R : Type u_1) [CommRing R] : Type u_1

For a Dedekind domain, the Weil divisor group is the free abelian group on the height-one primes.

theorem WeilDivisor.isEffective_zero (Y : Type u_1) : IsEffective 0

The zero divisor is effective.

theorem WeilDivisor.isEffective_add {Y : Type u_1} {D₁ D₂ : Group Y} (h₁ : IsEffective D₁) (h₂ : IsEffective D₂) : IsEffective (D₁ + D₂)

A sum of effective divisors is effective.