Ideal norms

This file defines the absolute ideal norm Ideal.absNorm (I : Ideal R) : ℕ as the cardinality of the quotient R ⧸ I (setting it to 0 if the cardinality is infinite).

Main definitions

• Submodule.cardQuot (S : Submodule R M): the cardinality of the quotient M ⧸ S, in ℕ. This maps ⊥ to 0 and ⊤ to 1.
• Ideal.absNorm (I : Ideal R): the absolute ideal norm, defined as the cardinality of the quotient R ⧸ I, as a bundled monoid-with-zero homomorphism.

Main results

• map_mul Ideal.absNorm: multiplicativity of the ideal norm is bundled in the definition of Ideal.absNorm
• Ideal.natAbs_det_basis_change: the ideal norm is given by the determinant of the basis change matrix
• Ideal.absNorm_span_singleton: the ideal norm of a principal ideal is the norm of its generator

noncomputable def Submodule.cardQuot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : ℕ

The cardinality of (M ⧸ S), if (M ⧸ S) is finite, and 0 otherwise. This is used to define the absolute ideal norm Ideal.absNorm.

theorem Submodule.cardQuot_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : S.cardQuot = Nat.card (M ⧸ S)

@[simp]

theorem Submodule.cardQuot_bot (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [Infinite M] : ⊥.cardQuot = 0

@[simp]

theorem Submodule.cardQuot_top (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : ⊤.cardQuot = 1

@[simp]

theorem Submodule.cardQuot_eq_one_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Submodule R M} : P.cardQuot = 1 ↔ P = ⊤

theorem cardQuot_mul_of_coprime {S : Type u_1} [CommRing S] {I J : Ideal S} (coprime : IsCoprime I J) : Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J

Multiplicity of the ideal norm, for coprime ideals. This is essentially just a repackaging of the Chinese Remainder Theorem.

theorem Ideal.mul_add_mem_pow_succ_inj {S : Type u_1} [CommRing S] (P : Ideal S) {i : ℕ} (a d d' e e' : S) (a_mem : a ∈ P ^ i) (e_mem : e ∈ P ^ (i + 1)) (e'_mem : e' ∈ P ^ (i + 1)) (h : d - d' ∈ P) : a * d + e - (a * d' + e') ∈ P ^ (i + 1)

If the d from Ideal.exists_mul_add_mem_pow_succ is unique, up to P, then so are the cs, up to P ^ (i + 1). Inspired by [Neukirch], proposition 6.1

theorem Ideal.exists_mul_add_mem_pow_succ {S : Type u_1} [CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} (a c : S) (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) (c_mem : c ∈ P ^ i) : ∃ (d : S), ∃ e ∈ P ^ (i + 1), a * d + e = c

If a ∈ P^i \ P^(i+1) and c ∈ P^i, then a * d + e = c for e ∈ P^(i+1). Ideal.mul_add_mem_pow_succ_unique shows the choice of d is unique, up to P. Inspired by [Neukirch], proposition 6.1

theorem Ideal.mem_prime_of_mul_mem_pow {S : Type u_1} [CommRing S] [IsDedekindDomain S] {P : Ideal S} [P_prime : P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} {a b : S} (a_notMem : a ∉ P ^ (i + 1)) (ab_mem : a * b ∈ P ^ (i + 1)) : b ∈ P

theorem Ideal.mul_add_mem_pow_succ_unique {S : Type u_1} [CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} (a d d' e e' : S) (a_notMem : a ∉ P ^ (i + 1)) (e_mem : e ∈ P ^ (i + 1)) (e'_mem : e' ∈ P ^ (i + 1)) (h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)) : d - d' ∈ P

The choice of d in Ideal.exists_mul_add_mem_pow_succ is unique, up to P. Inspired by [Neukirch], proposition 6.1

theorem cardQuot_pow_of_prime {S : Type u_1} [CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} : Submodule.cardQuot (P ^ i) = Submodule.cardQuot P ^ i

Multiplicity of the ideal norm, for powers of prime ideals.

theorem cardQuot_mul {S : Type u_1} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S) : Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J

Multiplicativity of the ideal norm in number rings.

noncomputable def Ideal.absNorm {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] : Ideal S →*₀ ℕ

The absolute norm of the ideal I : Ideal R is the cardinality of the quotient R ⧸ I.

theorem Ideal.absNorm_apply {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) : absNorm I = Submodule.cardQuot I

@[simp]

theorem Ideal.absNorm_bot {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] : absNorm ⊥ = 0

@[simp]

theorem Ideal.absNorm_top {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] : absNorm ⊤ = 1

@[simp]

theorem Ideal.absNorm_eq_one_iff {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I : Ideal S} : absNorm I = 1 ↔ I = ⊤

theorem Ideal.absNorm_ne_zero_iff {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) : absNorm I ≠ 0 ↔ Finite (S ⧸ I)

theorem Ideal.absNorm_dvd_absNorm_of_le {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I J : Ideal S} (h : J ≤ I) : absNorm I ∣ absNorm J

theorem Ideal.irreducible_of_irreducible_absNorm {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I : Ideal S} (hI : Irreducible (absNorm I)) : Irreducible I

theorem Ideal.isPrime_of_irreducible_absNorm {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I : Ideal S} (hI : Irreducible (absNorm I)) : I.IsPrime

theorem Ideal.prime_of_irreducible_absNorm_span {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {a : S} (ha : a ≠ 0) (hI : Irreducible (absNorm (span {a}))) : Prime a

theorem Ideal.absNorm_mem {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) : ↑(absNorm I) ∈ I

theorem Ideal.span_singleton_absNorm_le {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) : span {↑(absNorm I)} ≤ I

theorem Ideal.span_singleton_absNorm {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I : Ideal S} (hI : Nat.Prime (absNorm I)) : span {↑(absNorm I)} = comap (algebraMap ℤ S) I

theorem Ideal.natAbs_det_equiv {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S) {E : Type u_2} [EquivLike E S ↥I] [AddEquivClass E S ↥I] (e : E) : (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Let e : S ≃ I be an additive isomorphism (therefore a ℤ-linear equiv). Then an alternative way to compute the norm of I is given by taking the determinant of e. See natAbs_det_basis_change for a more familiar formulation of this result.

theorem Ideal.natAbs_det_basis_change {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ S) (I : Ideal S) (bI : Module.Basis ι ℤ ↥I) : (b.det (Subtype.val ∘ ⇑bI)).natAbs = absNorm I

Let b be a basis for S over ℤ and bI a basis for I over ℤ of the same dimension. Then an alternative way to compute the norm of I is given by taking the determinant of bI over b.

@[simp]

theorem Ideal.absNorm_span_singleton {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (r : S) : absNorm (span {r}) = ((Algebra.norm ℤ) r).natAbs

theorem Ideal.absNorm_dvd_norm_of_mem {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S} {x : S} (h : x ∈ I) : ↑(absNorm I) ∣ (Algebra.norm ℤ) x

@[simp]

theorem Ideal.absNorm_span_insert {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (r : S) (s : Set S) : absNorm (span (insert r s)) ∣ gcd (absNorm (span s)) ((Algebra.norm ℤ) r).natAbs

theorem Ideal.absNorm_eq_zero_iff {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S} : absNorm I = 0 ↔ I = ⊥

theorem Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S} : absNorm I ≠ 0 ↔ I ∈ nonZeroDivisors (Ideal S)

theorem Ideal.absNorm_pos_iff_mem_nonZeroDivisors {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S} : 0 < absNorm I ↔ I ∈ nonZeroDivisors (Ideal S)

theorem Ideal.absNorm_ne_zero_of_nonZeroDivisors {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : ↥(nonZeroDivisors (Ideal S))) : absNorm ↑I ≠ 0

theorem Ideal.absNorm_pos_of_nonZeroDivisors {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : ↥(nonZeroDivisors (Ideal S))) : 0 < absNorm ↑I

theorem Ideal.finite_setOf_absNorm_eq {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] [CharZero S] (n : ℕ) : {I : Ideal S | absNorm I = n}.Finite

theorem Ideal.finite_setOf_absNorm_le {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] [CharZero S] (n : ℕ) : {I : Ideal S | absNorm I ≤ n}.Finite

theorem Ideal.finite_setOf_absNorm_le₀ {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] [CharZero S] (n : ℕ) : {I : ↥(nonZeroDivisors (Ideal S)) | absNorm ↑I ≤ n}.Finite

theorem Ideal.card_norm_le_eq_card_norm_le_add_one {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (n : ℕ) [CharZero S] : Nat.card { I : Ideal S // absNorm I ≤ n } = Nat.card { I : ↥(nonZeroDivisors (Ideal S)) // absNorm ↑I ≤ n } + 1

theorem Ideal.norm_dvd_iff {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {x : S} (hx : Prime ((Algebra.norm ℤ) x)) {y : ℤ} : (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y

@[simp]

theorem Int.ideal_span_absNorm_eq_self (J : Ideal ℤ) : Ideal.span {↑(Ideal.absNorm J)} = J