Basic results on integral ideals of a number field

We study results about integral ideals of a number field K.

Main definitions and results

• Ideal.rootsOfUnityMapQuot : For I an integral ideal of K, the group morphism from the group of roots of unity of K of order n to (𝓞 K ⧸ I)ˣ.

• Ideal.rootsOfUnityMapQuot_injective: If the ideal I is nontrivial and its norm is coprime with n, then the map Ideal.rootsOfUnityMapQuot is injective.

• NumberField.torsionOrder_dvd_absNorm_sub_one: If the norm of the (nonzero) prime ideal P is coprime with the order of the torsion of K, then the norm of P is congruent to 1 modulo torsionOrder K.

• NumberField.torsionOrder_dvd_absNorm_sub_one': If the prime ideal P is unramified over ℤ and the norm of the prime of ℤ lying under P is different from 2, then the norm of P is congruent to 1 modulo torsionOrder K.

theorem IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] (hI : Ideal.absNorm I ≠ 1) {n : ℕ} {ζ : K} (hn : 2 ≤ n) (hζ : IsPrimitiveRoot ζ n) (h : (Ideal.Quotient.mk I) hζ.toInteger = 1) : ¬(Ideal.absNorm I).Coprime n

def Ideal.rootsOfUnityMapQuot {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) (n : ℕ) : ↥(rootsOfUnity n (NumberField.RingOfIntegers K)) →* (NumberField.RingOfIntegers K ⧸ I)ˣ

For I an integral ideal of K, the group morphism from the group of roots of unity of K of order n to (𝓞 K ⧸ I)ˣ.

Equations

• I.rootsOfUnityMapQuot n = (Units.map ↑(Ideal.Quotient.mk I)).domRestrict (rootsOfUnity n (NumberField.RingOfIntegers K))

@[simp]

theorem Ideal.rootsOfUnityMapQuot_apply {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) (n : ℕ) {x : (NumberField.RingOfIntegers K)ˣ} (hx : x ∈ rootsOfUnity n (NumberField.RingOfIntegers K)) : ↑((I.rootsOfUnityMapQuot n) ⟨x, hx⟩) = (Quotient.mk I) ↑x

def Ideal.torsionMapQuot {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) : ↥(NumberField.Units.torsion K) →* (NumberField.RingOfIntegers K ⧸ I)ˣ

For I an integral ideal of K, the group morphism from the torsion of K to (𝓞 K ⧸ I)ˣ.

Equations

• I.torsionMapQuot = (Units.map ↑(Ideal.Quotient.mk I)).domRestrict (NumberField.Units.torsion K)

@[simp]

theorem Ideal.torsionMapQuot_apply {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) {x : (NumberField.RingOfIntegers K)ˣ} (hx : x ∈ NumberField.Units.torsion K) : ↑(I.torsionMapQuot ⟨x, hx⟩) = (Quotient.mk I) ↑x

theorem Ideal.rootsOfUnityMapQuot_injective {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] (n : ℕ) [NeZero n] (hI₁ : absNorm I ≠ 1) (hI₂ : (absNorm I).Coprime n) : Function.Injective ⇑(I.rootsOfUnityMapQuot n)

theorem Ideal.rootsOfUnityMapQuot_inj {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] (n : ℕ) [NeZero n] (hI₁ : absNorm I ≠ 1) (hI₂ : (absNorm I).Coprime n) {x y : ↥(rootsOfUnity n (NumberField.RingOfIntegers K))} : (I.rootsOfUnityMapQuot n) x = (I.rootsOfUnityMapQuot n) y ↔ x = y

theorem IsPrimitiveRoot.idealQuotient_mk {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] {n : ℕ} [NeZero n] {ζ : NumberField.RingOfIntegers K} (hζ : IsPrimitiveRoot ζ n) (hI₁ : Ideal.absNorm I ≠ 1) (hI₂ : (Ideal.absNorm I).Coprime n) : IsPrimitiveRoot ((Ideal.Quotient.mk I) ζ) n

theorem Ideal.torsionMapQuot_injective {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] (hI₁ : absNorm I ≠ 1) (hI₂ : (absNorm I).Coprime (NumberField.Units.torsionOrder K)) : Function.Injective ⇑I.torsionMapQuot

If the ideal I is nontrivial and its norm is coprime with torsionOrder K, then the map Ideal.torsionMapQuot is injective.

See Ideal.torsionMapQuot_injective' for a version, with I a prime ideal, where this coprimality is replaced by I being unramified over ℤ.

theorem Ideal.torsionMapQuot_inj {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] (hI₁ : absNorm I ≠ 1) (hI₂ : (absNorm I).Coprime (NumberField.Units.torsionOrder K)) {x y : ↥(NumberField.Units.torsion K)} : I.torsionMapQuot x = I.torsionMapQuot y ↔ x = y

theorem Ideal.torsionMapQuot_injective' {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} [hP : P.IsPrime] (hP₁ : Algebra.IsUnramifiedAt ℤ P) (hP₂ : 2 < absNorm (under ℤ P)) : Function.Injective ⇑P.torsionMapQuot

If the prime ideal P is unramified over ℤ and the norm of the prime of ℤ lying under P is greater than 2, then the map Ideal.torsionMapQuot is injective.

See Ideal.torsionMapQuot_injective for a version where, instead, the norm of the ideal is assumed coprime with torsionOrder K.

theorem Ideal.torsionMapQuot_inj' {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} [hP : P.IsPrime] (hP₁ : Algebra.IsUnramifiedAt ℤ P) (hP₂ : 2 < absNorm (under ℤ P)) {x y : ↥(NumberField.Units.torsion K)} : P.torsionMapQuot x = P.torsionMapQuot y ↔ x = y

theorem NumberField.torsionOrder_dvd_absNorm_sub_one {K : Type u_1} [Field K] [NumberField K] {P : Ideal (RingOfIntegers K)} (hP₀ : P ≠ ⊥) (hP₁ : P.IsPrime) (hP₂ : (Ideal.absNorm P).Coprime (Units.torsionOrder K)) : Units.torsionOrder K ∣ Ideal.absNorm P - 1

If the norm of the (nonzero) prime ideal P is coprime with the order of the torsion of K, then the norm of P is congruent to 1 modulo torsionOrder K.

See NumberField.torsionOrder_dvd_absNorm_sub_one' for a version where this coprimality is replaced by P being unramified over ℤ.

theorem NumberField.torsionOrder_dvd_absNorm_sub_one' {K : Type u_1} [Field K] [NumberField K] {P : Ideal (RingOfIntegers K)} [hP : P.IsPrime] (hP₁ : Algebra.IsUnramifiedAt ℤ P) (hP₂ : Ideal.absNorm (Ideal.under ℤ P) ≠ 2) : Units.torsionOrder K ∣ Ideal.absNorm P - 1

If the prime ideal P is unramified over ℤ and the norm of the prime of ℤ lying under P is different from 2, then the norm of P is congruent to 1 modulo torsionOrder K.

See NumberField.torsionOrder_dvd_absNorm_sub_one for a version where, instead, the norm of P is assumed coprime with torsionOrder K.

instance instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal {K : Type u_1} [Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] [I.IsMaximal] : Finite (NumberField.RingOfIntegers K ⧸ I)