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

source

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

S.cardQuot = S.toAddSubgroup.index

Instances For

source

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)

source

@[simp]

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

⊥.cardQuot = 0

source

@[simp]

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

⊤.cardQuot = 1

source

@[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 = ⊤

source

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.

source

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

source

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_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

source

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_not_mem : a ∉ P ^ (i + 1)) (ab_mem : a * b ∈ P ^ (i + 1)) :

b ∈ P

source

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_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

source

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.

source

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.

source

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.

Equations

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

Instances For

source

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

Ideal.absNorm I = Submodule.cardQuot I

source

@[simp]

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

Ideal.absNorm ⊥ = 0

source

@[simp]

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

Ideal.absNorm ⊤ = 1

source

@[simp]

theorem Ideal.absNorm_eq_one_iff {S : Type u_1} [CommRing S] [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] {I : Ideal S} :

Ideal.absNorm I = 1 ↔ I = ⊤

source

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

Ideal.absNorm I ≠ 0 ↔ Finite (S ⧸ I)

source

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) :

Ideal.absNorm I ∣ Ideal.absNorm J

source

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

Irreducible I

source

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

I.IsPrime

source

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 (Ideal.absNorm (Ideal.span {a}))) :

Prime a

source

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

↑(Ideal.absNorm I) ∈ I

source

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

Ideal.span {↑(Ideal.absNorm I)} ≤ I

source

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

Ideal.span {↑(Ideal.absNorm I)} = Ideal.comap (algebraMap ℤ S) I

source

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 = 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.

source

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 : Basis ι ℤ S) (I : Ideal S) (bI : Basis ι ℤ ↥I) :

(b.det (Subtype.val ∘ ⇑bI)).natAbs = 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.

source

@[simp]