# Documentation

Mathlib.RingTheory.Ideal.Norm

# 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] [] [Module R M] (S : ) :

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

Instances For
@[simp]
theorem Submodule.cardQuot_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) [h : Fintype (M S)] :
@[simp]
theorem Submodule.cardQuot_bot (R : Type u_1) (M : Type u_2) [Ring R] [] [Module R M] [] :
theorem Submodule.cardQuot_top (R : Type u_1) (M : Type u_2) [Ring R] [] [Module R M] :
@[simp]
theorem Submodule.cardQuot_eq_one_iff {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {P : } :
P =
theorem cardQuot_mul_of_coprime {S : Type u_1} [] [] [] [] [] {I : } {J : } (coprime : I 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} [] (P : ) {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} [] [] {P : } [P_prime : ] (hP : P ) [] {i : } (a : S) (c : S) (a_mem : a P ^ i) (a_not_mem : ¬a P ^ (i + 1)) (c_mem : c P ^ i) :
d e, 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} [] [] [] {P : } [P_prime : ] (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} [] [] {P : } [P_prime : ] (hP : P ) [] {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} [] [] {P : } [P_prime : ] (hP : P ) [] [] [] {i : } :

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

theorem cardQuot_mul {S : Type u_1} [] [] [] [] [] (I : ) (J : ) :

Multiplicativity of the ideal norm in number rings.

noncomputable def Ideal.absNorm {S : Type u_1} [] [] [] [] [] [] :

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

Instances For
theorem Ideal.absNorm_apply {S : Type u_1} [] [] [] [] [] [] (I : ) :
Ideal.absNorm I =
@[simp]
theorem Ideal.absNorm_bot {S : Type u_1} [] [] [] [] [] [] :
Ideal.absNorm = 0
@[simp]
theorem Ideal.absNorm_top {S : Type u_1} [] [] [] [] [] [] :
Ideal.absNorm = 1
@[simp]
theorem Ideal.absNorm_eq_one_iff {S : Type u_1} [] [] [] [] [] [] {I : } :
Ideal.absNorm I = 1 I =
theorem Ideal.absNorm_ne_zero_iff {S : Type u_1} [] [] [] [] [] [] (I : ) :
Ideal.absNorm I 0 Finite (S I)
theorem Ideal.natAbs_det_equiv {S : Type u_1} [] [] [] [] [] [] (I : ) {E : Type u_2} [AddEquivClass E S { x // x I }] (e : E) :
Int.natAbs (LinearMap.det ()) = 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} [] [] [] [] [] [] {ι : Type u_2} [] [] (b : Basis ι S) (I : ) (bI : Basis ι { x // x I }) :
Int.natAbs (↑() (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} [] [] [] [] [] [] (r : S) :
Ideal.absNorm (Ideal.span {r}) = Int.natAbs (↑() r)
theorem Ideal.absNorm_dvd_absNorm_of_le {S : Type u_1} [] [] [] [] [] [] {I : } {J : } (h : J I) :
Ideal.absNorm I Ideal.absNorm J
theorem Ideal.absNorm_dvd_norm_of_mem {S : Type u_1} [] [] [] [] [] [] {I : } {x : S} (h : x I) :
↑(Ideal.absNorm I) ↑() x
@[simp]
theorem Ideal.absNorm_span_insert {S : Type u_1} [] [] [] [] [] [] (r : S) (s : Set S) :
Ideal.absNorm (Ideal.span (insert r s)) gcd (Ideal.absNorm ()) (Int.natAbs (↑() r))
theorem Ideal.irreducible_of_irreducible_absNorm {S : Type u_1} [] [] [] [] [] [] {I : } (hI : Irreducible (Ideal.absNorm I)) :
theorem Ideal.isPrime_of_irreducible_absNorm {S : Type u_1} [] [] [] [] [] [] {I : } (hI : Irreducible (Ideal.absNorm I)) :
theorem Ideal.prime_of_irreducible_absNorm_span {S : Type u_1} [] [] [] [] [] [] {a : S} (ha : a 0) (hI : Irreducible (Ideal.absNorm (Ideal.span {a}))) :
theorem Ideal.absNorm_mem {S : Type u_1} [] [] [] [] [] [] (I : ) :
↑(Ideal.absNorm I) I
theorem Ideal.span_singleton_absNorm_le {S : Type u_1} [] [] [] [] [] [] (I : ) :
Ideal.span {↑(Ideal.absNorm I)} I
theorem Ideal.finite_setOf_absNorm_eq {S : Type u_1} [] [] [] [] [] [] [] {n : } (hn : 0 < n) :
Set.Finite {I | Ideal.absNorm I = n}
def Ideal.spanNorm (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] (I : ) :

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

See also Ideal.relNorm.

Instances For
@[simp]
theorem Ideal.spanNorm_bot (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] :
@[simp]
theorem Ideal.spanNorm_eq_bot_iff {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] [] [] {I : } :
theorem Ideal.norm_mem_spanNorm (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] {I : } (x : S) (hx : x I) :
↑() x
@[simp]
theorem Ideal.spanNorm_singleton (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] {r : S} :
@[simp]
theorem Ideal.spanNorm_top (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] :
theorem Ideal.map_spanNorm (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] (I : ) {T : Type u_3} [] (f : R →+* T) :
Ideal.map f () = Ideal.span (f ↑() '' I)
theorem Ideal.spanNorm_mono (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] {I : } {J : } (h : I J) :
theorem Ideal.spanNorm_localization (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] (I : ) [] [] (M : ) {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ₘ] [] [] :
theorem Ideal.spanNorm_mul_spanNorm_le (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] (I : ) (J : ) :
theorem Ideal.spanNorm_mul_of_bot_or_top (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] (eq_bot_or_top : ∀ (I : ), I = I = ) (I : ) (J : ) :
Ideal.spanNorm R (I * 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} [] {K : Type u_3} [] [Algebra K S] [] [] (I : ) (J : ) :
Ideal.spanNorm K (I * J) = *
theorem Ideal.spanNorm_mul (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (I : ) (J : ) :
Ideal.spanNorm R (I * J) = *

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

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

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.

Instances For
theorem Ideal.relNorm_apply (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (I : ) :
↑() I = Ideal.span (↑() '' I)
@[simp]
theorem Ideal.spanNorm_eq (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (I : ) :
= ↑() I
@[simp]
theorem Ideal.relNorm_bot (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] :
↑() =
@[simp]
theorem Ideal.relNorm_top (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] :
↑() =
@[simp]
theorem Ideal.relNorm_eq_bot_iff {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] {I : } :
↑() I = I =
theorem Ideal.norm_mem_relNorm (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (I : ) {x : S} (hx : x I) :
↑() x ↑() I
@[simp]
theorem Ideal.relNorm_singleton (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (r : S) :
↑() (Ideal.span {r}) = Ideal.span {↑() r}
theorem Ideal.map_relNorm (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] (I : ) {T : Type u_3} [] (f : R →+* T) :
Ideal.map f (↑() I) = Ideal.span (f ↑() '' I)
theorem Ideal.relNorm_mono (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] [] [] [] [] [] [] {I : } {J : } (h : I J) :
↑() I ↑() J