Euler's totient for ideals of a Dedekind domain

For an ideal I of an infinite Dedekind domain R whose quotient R ⧸ I is finite, this file counts the units of R ⧸ I in terms of the absolute norm N = Ideal.absNorm: #(R ⧸ I)ˣ = N I · ∏_{𝔭 ∣ I} (1 - (N 𝔭)⁻¹), the product running over the height-one primes dividing I. For R = ℤ this is Euler's product formula for the totient.

The set of primes dividing I is passed as a Finset S together with the characterisation ∀ v, v ∈ S ↔ v.asIdeal ∣ I, so that any concrete description of the prime divisors of I can be used directly.

Main results

• Ideal.card_units_quotient_pow_mul_absNorm: #(R ⧸ P ^ e)ˣ · N P = N (P ^ e) · (N P - 1) for a maximal ideal P and e ≠ 0.
• Ideal.card_units_quotient_mul_prod_absNorm: #(R ⧸ I)ˣ · ∏_{𝔭 ∈ S} N 𝔭 = N I · ∏_{𝔭 ∈ S} (N 𝔭 - 1) in ℕ, the analogue of Nat.totient_mul_prod_primeFactors.
• Ideal.card_units_quotient_eq_absNorm_mul_prod: #(R ⧸ I)ˣ = N I · ∏_{𝔭 ∈ S} (1 - (N 𝔭)⁻¹) in any field of characteristic zero, the analogue of Nat.totient_eq_mul_prod_factors.

theorem Ideal.card_units_quotient_pow_mul_absNorm {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Infinite R] (P : Ideal R) [P.IsMaximal] {e : ℕ} (he : e ≠ 0) [Finite (R ⧸ P ^ e)] : Nat.card (R ⧸ P ^ e)ˣ * absNorm P = absNorm (P ^ e) * (absNorm P - 1)

Units of the quotient by a prime power. For a maximal ideal P and e ≠ 0, #(R ⧸ P ^ e)ˣ · N P = N (P ^ e) · (N P - 1) in ℕ: the non-units of the local ring R ⧸ P ^ e are the residues lying in P, which make up 1 / N P of the quotient.

theorem Ideal.card_units_quotient_mul_prod_absNorm {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Infinite R] (I : Ideal R) [Finite (R ⧸ I)] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v ∈ S ↔ v.asIdeal ∣ I) : Nat.card (R ⧸ I)ˣ * ∏ v ∈ S, absNorm v.asIdeal = absNorm I * ∏ v ∈ S, (absNorm v.asIdeal - 1)

Euler's totient for ideals, multiplicative form: if S is the set of height-one primes dividing I and R ⧸ I is finite, then #(R ⧸ I)ˣ · ∏_{𝔭 ∈ S} N 𝔭 = N I · ∏_{𝔭 ∈ S} (N 𝔭 - 1). This is the analogue of Nat.totient_mul_prod_primeFactors; for the form with the factors 1 - (N 𝔭)⁻¹ in a field, see Ideal.card_units_quotient_eq_absNorm_mul_prod.

theorem Ideal.card_units_quotient_eq_absNorm_mul_prod {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Infinite R] {F : Type u_2} [Field F] [CharZero F] (I : Ideal R) [Finite (R ⧸ I)] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v ∈ S ↔ v.asIdeal ∣ I) : ↑(Nat.card (R ⧸ I)ˣ) = ↑(absNorm I) * ∏ v ∈ S, (1 - (↑(absNorm v.asIdeal))⁻¹)

Euler's totient for ideals: if S is the set of height-one primes dividing I and R ⧸ I is finite, then #(R ⧸ I)ˣ = N I · ∏_{𝔭 ∈ S} (1 - (N 𝔭)⁻¹) in any field of characteristic zero. This is the analogue of Nat.totient_eq_mul_prod_factors, which is stated over ℚ only; the identity in ℕ, free of inverses, is Ideal.card_units_quotient_mul_prod_absNorm.