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), and the relative ideal norm Ideal.spanNorm R (I : Ideal S) : Ideal S as the ideal spanned by the norms of elements in I.

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.
• Ideal.spanNorm R (I : Ideal S): the ideal spanned by the norms of elements in I. This is used to define Ideal.relNorm.
• Ideal.relNorm R (I : Ideal S): the relative ideal norm as a bundled monoid-with-zero morphism, defined as the ideal spanned by the norms of elements in I.

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
• map_mul Ideal.relNorm: multiplicativity of the relative ideal norm

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.

Equations

• Submodule.cardQuot S = AddSubgroup.index (Submodule.toAddSubgroup S)

@[simp]

theorem Submodule.cardQuot_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) [h : Fintype (M ⧸ S)] : Submodule.cardQuot S = Fintype.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] : Submodule.cardQuot ⊥ = 0

theorem Submodule.cardQuot_top (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : Submodule.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} : Submodule.cardQuot P = 1 ↔ P = ⊤

theorem cardQuot_mul_of_coprime {S : Type u_1} [CommRing S] [IsDomain S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S} {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 : S) (d : S) (d' : S) (e : S) (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 : Ideal.IsPrime P] (hP : P ≠ ⊥) [IsDedekindDomain S] {i : ℕ} (a : S) (c : S) (a_mem : a ∈ P ^ i) (a_not_mem : 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 : Ideal.IsPrime P] (hP : P ≠ ⊥) {i : ℕ} {a : S} {b : S} (a_not_mem : 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 : Ideal.IsPrime P] (hP : P ≠ ⊥) [IsDedekindDomain S] {i : ℕ} (a : S) (d : S) (d' : S) (e : S) (e' : S) (a_not_mem : 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] [IsDomain S] {P : Ideal S} [P_prime : Ideal.IsPrime P] (hP : P ≠ ⊥) [IsDedekindDomain S] [Module.Finite ℤ S] [Module.Free ℤ S] {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] [IsDomain S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S) (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] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] : Ideal S →*₀ ℕ

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

Equations

• Ideal.absNorm = { toZeroHom := { toFun := Submodule.cardQuot, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Ideal.natAbs_det_equiv {S : Type u_1} [CommRing S] [IsDomain 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) : Int.natAbs (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ AddMonoidHom.toIntLinearMap ↑e)) = Ideal.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] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ S) (I : Ideal S) (bI : Basis ι ℤ ↥I) : Int.natAbs ((Basis.det b) (Subtype.val ∘ ⇑bI)) = Ideal.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] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (r : S) : Ideal.absNorm (Ideal.span {r}) = Int.natAbs ((Algebra.norm ℤ) r)

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

theorem Ideal.norm_dvd_iff {S : Type u_1} [CommRing S] [IsDomain 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

def Ideal.spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) : Ideal R

Ideal.spanNorm R (I : Ideal S) is the ideal generated by mapping Algebra.norm R over I.

See also Ideal.relNorm.

Equations

• Ideal.spanNorm R I = Ideal.span (⇑(Algebra.norm R) '' ↑I)

@[simp]

theorem Ideal.spanNorm_bot (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Nontrivial S] [Module.Free R S] [Module.Finite R S] : Ideal.spanNorm R ⊥ = ⊥

@[simp]

theorem Ideal.spanNorm_eq_bot_iff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] {I : Ideal S} : Ideal.spanNorm R I = ⊥ ↔ I = ⊥

theorem Ideal.norm_mem_spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I : Ideal S} (x : S) (hx : x ∈ I) : (Algebra.norm R) x ∈ Ideal.spanNorm R I

@[simp]

theorem Ideal.spanNorm_singleton (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {r : S} : Ideal.spanNorm R (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}

@[simp]

theorem Ideal.spanNorm_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] : Ideal.spanNorm R ⊤ = ⊤

theorem Ideal.map_spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) {T : Type u_3} [CommRing T] (f : R →+* T) : Ideal.map f (Ideal.spanNorm R I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)

theorem Ideal.spanNorm_mono (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I : Ideal S} {J : Ideal S} (h : I ≤ J) : Ideal.spanNorm R I ≤ Ideal.spanNorm R J

theorem Ideal.spanNorm_localization (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) [Module.Finite R S] [Module.Free R S] (M : Submonoid R) {Rₘ : Type u_3} (Sₘ : Type u_4) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] : Ideal.spanNorm Rₘ (Ideal.map (algebraMap S Sₘ) I) = Ideal.map (algebraMap R Rₘ) (Ideal.spanNorm R I)

theorem Ideal.spanNorm_mul_spanNorm_le (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) (J : Ideal S) : Ideal.spanNorm R I * Ideal.spanNorm R J ≤ Ideal.spanNorm R (I * J)

theorem Ideal.spanNorm_mul_of_bot_or_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] (eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) (I : Ideal S) (J : Ideal S) : Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J

This condition eq_bot_or_top is equivalent to being a field. However, Ideal.spanNorm_mul_of_field is harder to apply since we'd need to upgrade a CommRing R instance to a Field R instance.

@[simp]

theorem Ideal.spanNorm_mul_of_field {S : Type u_2} [CommRing S] {K : Type u_3} [Field K] [Algebra K S] [IsDomain S] [Module.Finite K S] (I : Ideal S) (J : Ideal S) : Ideal.spanNorm K (I * J) = Ideal.spanNorm K I * Ideal.spanNorm K J

theorem Ideal.spanNorm_mul (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) (J : Ideal S) : Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J

Multiplicativity of Ideal.spanNorm. simp-normal form is map_mul (Ideal.relNorm R).

def Ideal.relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] : Ideal S →*₀ Ideal R

The relative norm Ideal.relNorm R (I : Ideal S), where R and S are Dedekind domains, and S is an extension of R that is finite and free as a module.

Equations

• Ideal.relNorm R = { toZeroHom := { toFun := Ideal.spanNorm R, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

theorem Ideal.relNorm_apply (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) : (Ideal.relNorm R) I = Ideal.span (⇑(Algebra.norm R) '' ↑I)

@[simp]

theorem Ideal.spanNorm_eq (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) : Ideal.spanNorm R I = (Ideal.relNorm R) I

@[simp]

theorem Ideal.relNorm_bot (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] : (Ideal.relNorm R) ⊥ = ⊥

@[simp]

theorem Ideal.relNorm_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] : (Ideal.relNorm R) ⊤ = ⊤

@[simp]

theorem Ideal.relNorm_eq_bot_iff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] {I : Ideal S} : (Ideal.relNorm R) I = ⊥ ↔ I = ⊥

theorem Ideal.norm_mem_relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) : (Algebra.norm R) x ∈ (Ideal.relNorm R) I

@[simp]

theorem Ideal.relNorm_singleton (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (r : S) : (Ideal.relNorm R) (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}

theorem Ideal.map_relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) {T : Type u_3} [CommRing T] (f : R →+* T) : Ideal.map f ((Ideal.relNorm R) I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)

theorem Ideal.relNorm_mono (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] {I : Ideal S} {J : Ideal S} (h : I ≤ J) : (Ideal.relNorm R) I ≤ (Ideal.relNorm R) J