Coprime multiplicativity of the ideal norm counting function #
A nonzero ideal whose norm is m * n, with m and n coprime, has a
unique factorization into ideals of norms m and n.
theorem
NairTenenbaum.ideals_isRelPrime_of_coprime_norm
{K : Type u_1}
[Field K]
[NumberField K]
{I J : Ideal (NumberField.RingOfIntegers K)}
(h : (Ideal.absNorm I).Coprime (Ideal.absNorm J))
:
IsRelPrime I J
theorem
NairTenenbaum.ideal_factorization_unique_of_coprime_norm
{K : Type u_1}
[Field K]
[NumberField K]
{I J I' J' : Ideal (NumberField.RingOfIntegers K)}
(hI : Ideal.absNorm I = Ideal.absNorm I')
(hJ : Ideal.absNorm J = Ideal.absNorm J')
(hcop : (Ideal.absNorm I).Coprime (Ideal.absNorm J))
(h : I * J = I' * J')
:
theorem
NairTenenbaum.exists_ideal_factors_of_coprime_norm
{K : Type u_1}
[Field K]
[NumberField K]
{I : Ideal (NumberField.RingOfIntegers K)}
{m n : ℕ}
(hm : 0 < m)
(hn : 0 < n)
(hcop : m.Coprime n)
(hI : Ideal.absNorm I = m * n)
:
∃ (A : Ideal (NumberField.RingOfIntegers K)) (B : Ideal (NumberField.RingOfIntegers K)),
A * B = I ∧ Ideal.absNorm A = m ∧ Ideal.absNorm B = n
noncomputable def
NairTenenbaum.idealNormMulEquiv
{K : Type u_1}
[Field K]
[NumberField K]
{m n : ℕ}
(hm : 0 < m)
(hn : 0 < n)
(hcop : m.Coprime n)
:
{ I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = m } × { J : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm J = n } ≃ { L : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm L = m * n }
Multiplication identifies ideals of coprime product norm with pairs of ideals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
NairTenenbaum.idealNormCount_mul_of_coprime
{K : Type u_1}
[Field K]
[NumberField K]
{m n : ℕ}
(hcop : m.Coprime n)
: