# mathlib3documentation

ring_theory.ideal.norm

# Ideal norms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the absolute ideal norm ideal.abs_norm (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.span_norm R (I : ideal S) : ideal S as the ideal spanned by the norms of elements in I.

## Main definitions #

• submodule.card_quot (S : submodule R M): the cardinality of the quotient M ⧸ S, in ℕ. This maps ⊥ to 0 and ⊤ to 1.
• ideal.abs_norm (I : ideal R): the absolute ideal norm, defined as the cardinality of the quotient R ⧸ I, as a bundled monoid-with-zero homomorphism.
• ideal.span_norm R (I : ideal S): the ideal spanned by the norms of elements in I. This is used to define ideal.rel_norm.
• ideal.rel_norm 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.abs_norm: multiplicativity of the ideal norm is bundled in the definition of ideal.abs_norm
• ideal.nat_abs_det_basis_change: the ideal norm is given by the determinant of the basis change matrix
• ideal.abs_norm_span_singleton: the ideal norm of a principal ideal is the norm of its generator
• map_mul ideal.rel_norm: multiplicativity of the relative ideal norm
noncomputable def submodule.card_quot {R : Type u_1} {M : Type u_2} [ring R] [ M] (S : M) :

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

Equations
@[simp]
theorem submodule.card_quot_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] (S : M) [fintype (M S)] :
@[simp]
theorem submodule.card_quot_bot (R : Type u_1) (M : Type u_2) [ring R] [ M] [infinite M] :
@[simp]
theorem submodule.card_quot_top (R : Type u_1) (M : Type u_2) [ring R] [ M] :
@[simp]
theorem submodule.card_quot_eq_one_iff {R : Type u_1} {M : Type u_2} [ring R] [ M] {P : M} :
theorem card_quot_mul_of_coprime {S : Type u_1} [comm_ring S] [is_domain S] [ S] [ S] {I J : ideal S} (coprime : I J = ) :
(I * J).card_quot =

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} [comm_ring S] [is_domain 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} [comm_ring S] [is_domain S] {P : ideal S} [P_prime : P.is_prime] (hP : P ) {i : } (a c : S) (a_mem : a P ^ i) (a_not_mem : a P ^ (i + 1)) (c_mem : c P ^ i) :
(d e : S) (H : 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} [comm_ring S] [is_domain S] {P : ideal S} [P_prime : P.is_prime] (hP : P ) {i : } {a 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} [comm_ring S] [is_domain S] {P : ideal S} [P_prime : P.is_prime] (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

theorem card_quot_pow_of_prime {S : Type u_1} [comm_ring S] [is_domain S] {P : ideal S} [P_prime : P.is_prime] (hP : P ) [ S] [ S] {i : } :
(P ^ i).card_quot =

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

theorem card_quot_mul {S : Type u_1} [comm_ring S] [is_domain S] [ S] [ S] (I J : ideal S) :
(I * J).card_quot =

Multiplicativity of the ideal norm in number rings.

noncomputable def ideal.abs_norm {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] :

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

Equations
theorem ideal.abs_norm_apply {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (I : ideal S) :
@[simp]
theorem ideal.abs_norm_bot {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] :
@[simp]
theorem ideal.abs_norm_top {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] :
@[simp]
theorem ideal.abs_norm_eq_one_iff {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {I : ideal S} :
I =
theorem ideal.abs_norm_ne_zero_iff {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (I : ideal S) :
finite (S I)
theorem ideal.nat_abs_det_equiv {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (I : ideal S) {E : Type u_2} [ I] (e : E) :

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 nat_abs_det_basis_change for a more familiar formulation of this result.

theorem ideal.nat_abs_det_basis_change {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {ι : Type u_2} [fintype ι] [decidable_eq ι] (b : S) (I : ideal S) (bI : I) :
((b.det) (coe bI)).nat_abs =

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.abs_norm_span_singleton {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (r : S) :
theorem ideal.abs_norm_dvd_abs_norm_of_le {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {I J : ideal S} (h : J I) :
theorem ideal.abs_norm_dvd_norm_of_mem {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {I : ideal S} {x : S} (h : x I) :
@[simp]
theorem ideal.abs_norm_span_insert {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (r : S) (s : set S) :
theorem ideal.irreducible_of_irreducible_abs_norm {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {I : ideal S} (hI : irreducible ) :
theorem ideal.is_prime_of_irreducible_abs_norm {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {I : ideal S} (hI : irreducible ) :
theorem ideal.prime_of_irreducible_abs_norm_span {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] {a : S} (ha : a 0) (hI : irreducible (ideal.abs_norm (ideal.span {a}))) :
theorem ideal.abs_norm_mem {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (I : ideal S) :
theorem ideal.span_singleton_abs_norm_le {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] (I : ideal S) :
I
theorem ideal.finite_set_of_abs_norm_eq {S : Type u_1} [comm_ring S] [is_domain S] [infinite S] [ S] [ S] [char_zero S] {n : } (hn : 0 < n) :
{I : | = n}.finite
def ideal.span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (I : ideal S) :

ideal.span_norm R (I : ideal S) is the ideal generated by mapping algebra.norm R over I.

See also ideal.rel_norm.

Equations
@[simp]
theorem ideal.span_norm_bot (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [nontrivial S] [ S] [ S] :
@[simp]
theorem ideal.span_norm_eq_bot_iff {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] {I : ideal S} :
I =
theorem ideal.norm_mem_span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {I : ideal S} (x : S) (hx : x I) :
@[simp]
theorem ideal.span_norm_singleton (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {r : S} :
@[simp]
theorem ideal.span_norm_top (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem ideal.map_span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (I : ideal S) {T : Type u_3} [comm_ring T] (f : R →+* T) :
theorem ideal.span_norm_mono (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {I J : ideal S} (h : I J) :
theorem ideal.span_norm_localization (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (I : ideal S) [ S] [ S] (M : submonoid R) {Rₘ : Type u_3} (Sₘ : Type u_4) [comm_ring Rₘ] [ Rₘ] [comm_ring Sₘ] [ Sₘ] [algebra Rₘ Sₘ] [ Sₘ] [ Rₘ Sₘ] [ Sₘ] [ Rₘ] [ Sₘ] :
(ideal.map Sₘ) I) = ideal.map Rₘ) I)
theorem ideal.span_norm_mul_span_norm_le (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (I J : ideal S) :
* (I * J)
theorem ideal.span_norm_mul_of_bot_or_top (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (eq_bot_or_top : (I : ideal R), I = I = ) (I J : ideal S) :
(I * J) = *

This condition eq_bot_or_top is equivalent to being a field. However, span_norm_mul_of_field is harder to apply since we'd need to upgrade a comm_ring R instance to a field R instance.

@[simp]
theorem ideal.span_norm_mul_of_field {S : Type u_2} [comm_ring S] {K : Type u_1} [field K] [ S] [is_domain S] [ S] (I J : ideal S) :
(I * J) = *
theorem ideal.span_norm_mul (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (I J : ideal S) :
(I * J) = *

Multiplicativity of ideal.span_norm. simp-normal form is map_mul (ideal.rel_norm R).

def ideal.rel_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] :

The relative norm ideal.rel_norm 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
theorem ideal.rel_norm_apply (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (I : ideal S) :
@[simp]
theorem ideal.span_norm_eq (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (I : ideal S) :
= I
@[simp]
theorem ideal.rel_norm_bot (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] :
@[simp]
theorem ideal.rel_norm_top (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] :
@[simp]
theorem ideal.rel_norm_eq_bot_iff {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] {I : ideal S} :
theorem ideal.norm_mem_rel_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (I : ideal S) {x : S} (hx : x I) :
@[simp]
theorem ideal.rel_norm_singleton (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (r : S) :
theorem ideal.map_rel_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] (I : ideal S) {T : Type u_3} [comm_ring T] (f : R →+* T) :
theorem ideal.rel_norm_mono (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] [is_domain R] [is_domain S] [ S] [ S] {I J : ideal S} (h : I J) :
I J