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 quotientM ⧸ S, inℕ. This maps⊥to0and⊤to1.ideal.abs_norm (I : ideal R): the absolute ideal norm, defined as the cardinality of the quotientR ⧸ I, as a bundled monoid-with-zero homomorphism.ideal.span_norm R (I : ideal S): the ideal spanned by the norms of elements inI. This is used to defineideal.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 inI.
Main results #
map_mul ideal.abs_norm: multiplicativity of the ideal norm is bundled in the definition ofideal.abs_normideal.nat_abs_det_basis_change: the ideal norm is given by the determinant of the basis change matrixideal.abs_norm_span_singleton: the ideal norm of a principal ideal is the norm of its generatormap_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]
[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)] :
S.card_quot = fintype.card (M ⧸ S)
@[simp]
theorem
submodule.card_quot_top
(R : Type u_1)
(M : Type u_2)
[ring R]
[add_comm_group M]
[module R M] :
theorem
card_quot_mul_of_coprime
{S : Type u_1}
[comm_ring S]
[is_domain S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{I J : ideal S}
(coprime : I ⊔ J = ⊤) :
(I * J).card_quot = submodule.card_quot I * submodule.card_quot 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}
[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) :
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) :
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.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)) :
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 : ℕ} :
(P ^ i).card_quot = submodule.card_quot P ^ i
Multiplicity of the ideal norm, for powers of prime ideals.
theorem
card_quot_mul
{S : Type u_1}
[comm_ring S]
[is_domain S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I J : ideal S) :
(I * J).card_quot = submodule.card_quot I * submodule.card_quot J
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]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S] :
The absolute norm of the ideal I : ideal R is the cardinality of the quotient R ⧸ I.
Equations
- ideal.abs_norm = {to_fun := submodule.card_quot semiring.to_module, map_zero' := _, map_one' := _, map_mul' := _}
theorem
ideal.abs_norm_apply
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I : ideal S) :
@[simp]
theorem
ideal.abs_norm_bot
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S] :
@[simp]
theorem
ideal.abs_norm_top
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S] :
@[simp]
theorem
ideal.abs_norm_eq_one_iff
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{I : ideal S} :
theorem
ideal.abs_norm_ne_zero_iff
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I : ideal S) :
theorem
ideal.nat_abs_det_equiv
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I : ideal S)
{E : Type u_2}
[add_equiv_class E S ↥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]
[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.
@[simp]
theorem
ideal.abs_norm_span_singleton
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(r : S) :
⇑ideal.abs_norm (ideal.span {r}) = (⇑(algebra.norm ℤ) r).nat_abs
theorem
ideal.abs_norm_dvd_abs_norm_of_le
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ 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]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{I : ideal S}
{x : S}
(h : x ∈ I) :
↑(⇑ideal.abs_norm I) ∣ ⇑(algebra.norm ℤ) x
@[simp]
theorem
ideal.abs_norm_span_insert
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(r : S)
(s : set S) :
⇑ideal.abs_norm (ideal.span (has_insert.insert r s)) ∣ gcd_monoid.gcd (⇑ideal.abs_norm (ideal.span s)) (⇑(algebra.norm ℤ) r).nat_abs
theorem
ideal.irreducible_of_irreducible_abs_norm
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{I : ideal S}
(hI : irreducible (⇑ideal.abs_norm I)) :
theorem
ideal.is_prime_of_irreducible_abs_norm
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{I : ideal S}
(hI : irreducible (⇑ideal.abs_norm I)) :
I.is_prime
theorem
ideal.prime_of_irreducible_abs_norm_span
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
{a : S}
(ha : a ≠ 0)
(hI : irreducible (⇑ideal.abs_norm (ideal.span {a}))) :
prime a
theorem
ideal.abs_norm_mem
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I : ideal S) :
↑(⇑ideal.abs_norm I) ∈ I
theorem
ideal.span_singleton_abs_norm_le
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
(I : ideal S) :
ideal.span {↑(⇑ideal.abs_norm I)} ≤ I
theorem
ideal.finite_set_of_abs_norm_eq
{S : Type u_1}
[comm_ring S]
[is_domain S]
[infinite S]
[is_dedekind_domain S]
[module.free ℤ S]
[module.finite ℤ S]
[char_zero S]
{n : ℕ}
(hn : 0 < n) :
{I : ideal S | ⇑ideal.abs_norm I = n}.finite
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 R
ideal.span_norm R (I : ideal S) is the ideal generated by mapping algebra.norm R over I.
See also ideal.rel_norm.
Equations
- ideal.span_norm R I = ideal.span (⇑(algebra.norm R) '' ↑I)
@[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] :
ideal.span_norm R ⊥ = ⊥
@[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) :
⇑(algebra.norm R) x ∈ ideal.span_norm R 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} :
ideal.span_norm R (ideal.span {r}) = ideal.span {⇑(algebra.norm R) r}
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) :
ideal.span_norm R I ≤ ideal.span_norm R 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ₘ] :
ideal.span_norm Rₘ (ideal.map (algebra_map S Sₘ) I) = ideal.map (algebra_map R Rₘ) (ideal.span_norm R I)
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) :
ideal.span_norm R I * ideal.span_norm R J ≤ ideal.span_norm R (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]
[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) :
ideal.span_norm R (I * J) = ideal.span_norm R I * ideal.span_norm R 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]
[algebra K S]
[is_domain S]
[module.finite K S]
(I J : ideal S) :
ideal.span_norm K (I * J) = ideal.span_norm K I * ideal.span_norm K J
theorem
ideal.span_norm_mul
(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) :
ideal.span_norm R (I * J) = ideal.span_norm R I * ideal.span_norm R 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]
[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] :
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
- ideal.rel_norm R = {to_fun := ideal.span_norm R _inst_3, map_zero' := _, map_one' := _, map_mul' := _}
theorem
ideal.rel_norm_apply
(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) :
⇑(ideal.rel_norm R) I = ideal.span (⇑(algebra.norm R) '' ↑I)
@[simp]
theorem
ideal.span_norm_eq
(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) :
ideal.span_norm R I = ⇑(ideal.rel_norm R) I
@[simp]
theorem
ideal.rel_norm_bot
(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] :
⇑(ideal.rel_norm R) ⊥ = ⊥
@[simp]
theorem
ideal.rel_norm_top
(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] :
⇑(ideal.rel_norm R) ⊤ = ⊤
@[simp]
theorem
ideal.rel_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]
[is_dedekind_domain R]
[is_dedekind_domain S]
[module.finite R S]
[module.free R S]
{I : ideal S} :
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) :
⇑(algebra.norm R) x ∈ ⇑(ideal.rel_norm R) I
@[simp]
theorem
ideal.rel_norm_singleton
(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]
(r : S) :
⇑(ideal.rel_norm R) (ideal.span {r}) = ideal.span {⇑(algebra.norm R) r}
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) :
ideal.map f (⇑(ideal.rel_norm R) I) = ideal.span (⇑f ∘ ⇑(algebra.norm R) '' ↑I)
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) :
⇑(ideal.rel_norm R) I ≤ ⇑(ideal.rel_norm R) J