mathlib3 documentation

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 #

Main results #

noncomputable def submodule.card_quot {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group 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.abs_norm.

Equations
@[simp]
theorem submodule.card_quot_apply {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S : submodule R M) [fintype (M S)] :
@[simp]
theorem submodule.card_quot_bot (R : Type u_1) (M : Type u_2) [ring R] [add_comm_group M] [module R M] [infinite M] :
@[simp]
theorem submodule.card_quot_top (R : Type u_1) (M : Type u_2) [ring R] [add_comm_group M] [module R M] :
@[simp]
theorem submodule.card_quot_eq_one_iff {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {P : submodule R M} :

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 ) [is_dedekind_domain S] {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] [is_dedekind_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 ) [is_dedekind_domain S] {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 ) [is_dedekind_domain S] [module.finite S] [module.free S] {i : } :

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

Multiplicativity of the ideal norm in number rings.

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

Equations

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] [is_dedekind_domain S] [module.free S] [module.finite S] {ι : Type u_2} [fintype ι] [decidable_eq ι] (b : basis ι S) (I : ideal S) (bI : basis ι 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.

def ideal.span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R 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] [algebra R S] [nontrivial S] [module.free R S] [module.finite R S] :
@[simp]
theorem ideal.span_norm_eq_bot_iff {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] [is_domain R] [is_domain S] [module.free R S] [module.finite R S] {I : ideal S} :
theorem ideal.norm_mem_span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R 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] [algebra R S] {r : S} :
@[simp]
theorem ideal.span_norm_top (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :
theorem ideal.map_span_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R 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] [algebra R 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] [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) [comm_ring Rₘ] [algebra R Rₘ] [comm_ring Sₘ] [algebra S Sₘ] [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] [is_localization M Rₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] :
theorem ideal.span_norm_mul_span_norm_le (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] (I J : ideal S) :
theorem ideal.span_norm_mul_of_bot_or_top (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] [is_domain R] [is_domain S] [module.free R S] [module.finite R S] (eq_bot_or_top : (I : ideal R), I = I = ) (I J : ideal S) :

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] [algebra K S] [is_domain S] [module.finite K S] (I J : ideal S) :

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

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
@[simp]
@[simp]
theorem ideal.norm_mem_rel_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] [is_domain R] [is_domain S] [is_dedekind_domain R] [is_dedekind_domain S] [module.finite R S] [module.free R S] (I : ideal S) {x : S} (hx : x I) :
theorem ideal.map_rel_norm (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] [is_domain R] [is_domain S] [is_dedekind_domain R] [is_dedekind_domain S] [module.finite R S] [module.free R 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] [algebra R S] [is_domain R] [is_domain S] [is_dedekind_domain R] [is_dedekind_domain S] [module.finite R S] [module.free R S] {I J : ideal S} (h : I J) :