Divisors of a Dedekind domain

This file identifies the group of nonzero fractional ideals of a Dedekind domain with the free abelian group on its height-one prime ideals. The coefficient of a prime v is the existing function FractionalIdeal.count K v.

Main definitions

• IsDedekindDomain.Divisor: the free abelian group on height-one prime ideals.
• FractionalIdeal.divisor: the divisor associated to a nonzero fractional ideal.
• FractionalIdeal.divisorEquiv: the additive equivalence between nonzero fractional ideals and divisors.
• FractionalIdeal.principalDivisor: the divisor of a nonzero element of the fraction field.

@[reducible, inline]

abbrev IsDedekindDomain.Divisor (R : Type u_1) [CommRing R] : Type u_1

The group of divisors supported on height-one prime ideals of a ring.

Equations

• IsDedekindDomain.Divisor R = (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

noncomputable def FractionalIdeal.divisor {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)ˣ) : IsDedekindDomain.Divisor R

The divisor of a nonzero fractional ideal.

Equations

• FractionalIdeal.divisor I = { support := Set.Finite.toFinset ⋯, toFun := fun (v : IsDedekindDomain.HeightOneSpectrum R) => FractionalIdeal.count K v ↑I, mem_support_toFun := ⋯ }

@[simp]

theorem FractionalIdeal.divisor_apply {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)ˣ) (v : IsDedekindDomain.HeightOneSpectrum R) : (divisor I) v = count K v ↑I

noncomputable def FractionalIdeal.ofDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (D : IsDedekindDomain.Divisor R) : (FractionalIdeal (nonZeroDivisors R) K)ˣ

Reconstruct a nonzero fractional ideal from a divisor.

Equations

• FractionalIdeal.ofDivisor K D = Units.mk0 (Finsupp.prod D fun (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) => ↑v.asIdeal ^ n) ⋯

@[simp]

theorem FractionalIdeal.count_ofDivisor {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (D : IsDedekindDomain.Divisor R) (v : IsDedekindDomain.HeightOneSpectrum R) : count K v ↑(ofDivisor K D) = D v

noncomputable def FractionalIdeal.divisorEquiv {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃+ IsDedekindDomain.Divisor R

Nonzero fractional ideals of a Dedekind domain are additively equivalent to its divisors.

Multiplication of fractional ideals corresponds to addition of divisors.

Equations

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

noncomputable def FractionalIdeal.principalFractionalIdeal {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Kˣ →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

The nonzero principal fractional ideal generated by an element of the fraction field.

Equations

• FractionalIdeal.principalFractionalIdeal = { toFun := fun (x : Kˣ) => Units.mk0 (FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x) ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FractionalIdeal.principalFractionalIdeal_apply_coe {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : Kˣ) : ↑(principalFractionalIdeal x) = spanSingleton (nonZeroDivisors R) ↑x

noncomputable def FractionalIdeal.principalDivisor {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Additive Kˣ →+ IsDedekindDomain.Divisor R

The principal divisor of a nonzero element of the fraction field.

Equations

• FractionalIdeal.principalDivisor = FractionalIdeal.divisorEquiv.toAddMonoidHom.comp (MonoidHom.toAdditive FractionalIdeal.principalFractionalIdeal)

@[simp]

theorem FractionalIdeal.principalDivisor_apply {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : Additive Kˣ) (v : IsDedekindDomain.HeightOneSpectrum R) : (principalDivisor x) v = count K v (spanSingleton (nonZeroDivisors R) ↑(Additive.toMul x))

noncomputable def FractionalIdeal.weightedDegree {R : Type u_1} [CommRing R] (w : Ideal R → ℕ) : IsDedekindDomain.Divisor R →+ ℤ

A weighted degree on divisors of a Dedekind domain.

Equations

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

@[simp]

theorem FractionalIdeal.weightedDegree_apply {R : Type u_1} [CommRing R] (w : Ideal R → ℕ) (D : IsDedekindDomain.Divisor R) : (weightedDegree w) D = Finsupp.sum D fun (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) => n * ↑(w v.asIdeal)

theorem FractionalIdeal.divisor_ideal_sum_eq_normalizedFactors_sum {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (J : Ideal R) (hJ : J ≠ ⊥) (w : Ideal R → ℕ) : have JU := Units.mk0 ↑J ⋯; (Finsupp.sum (divisor JU) fun (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) => n * ↑(w v.asIdeal)) = ↑(Multiset.map w (UniqueFactorizationMonoid.normalizedFactors J)).sum

The weighted degree of the divisor of a nonzero integral ideal is the weighted sum of its normalized prime factors. The weight is stated on ideals, so that it can later be chosen as a residue-field degree or an inertia-weighted residue-field degree.

theorem FractionalIdeal.weightedDegree_divisor_ideal {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (J : Ideal R) (hJ : J ≠ ⊥) (w : Ideal R → ℕ) : (weightedDegree w) (divisor (Units.mk0 ↑J ⋯)) = ↑(Multiset.map w (UniqueFactorizationMonoid.normalizedFactors J)).sum

Weighted degree of the divisor of a nonzero integral ideal.

theorem FractionalIdeal.weightedDegree_principal_mk' {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (w : Ideal R → ℕ) (x : Kˣ) (n : R) (d : ↥(nonZeroDivisors R)) (hnd : IsLocalization.mk' K n d = ↑x) : (weightedDegree w) (principalDivisor (Additive.ofMul x)) = ↑(Multiset.map w (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {n}))).sum - ↑(Multiset.map w (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑d}))).sum

If a nonzero fraction is represented by n / d, its weighted principal-divisor degree is the weighted factor degree of n minus that of d.