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.

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)ˣ.

@[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)ˣ.

@[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 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

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.

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