Ideal of ℤ

We prove results about ideals of ℤ or ideals of extensions of ℤ.

In particular, for I an ideal of a ring R extending ℤ, we prove several results about absNorm (under ℤ I) which is the smallest positive integer contained in I.

Main definitions and results

• Int.ideal_span_isMaximal_of_prime: the ideal generated by a prime number is maximal.

• Int.liesOver_span_absNorm: the ideal generated by absNorm (under ℤ I) lies under I.

• Int.absNorm_under_eq_sInf: the predicate that the absNorm (under ℤ I) is the smallest positive integer in I.

• Int.absNorm_under_dvd_absNorm: absNorm (under ℤ I) divides the norm of I.

• Nat.absNorm_under_prime: If P is a prime ideal, then absNorm (under ℤ P) is a prime number.

theorem Int.card_ideal_quot (n : ℕ) : Nat.card (ℤ ⧸ Ideal.span {↑n}) = n

instance Int.ideal_span_isMaximal_of_prime (p : ℕ) [Fact (Nat.Prime p)] : (Ideal.span {↑p}).IsMaximal

theorem Int.ringChar_idealQuot (n : ℕ) : ringChar (ℤ ⧸ Ideal.span {↑n}) = n

instance Int.liesOver_span_absNorm {R : Type u_1} [Ring R] (I : Ideal R) : I.LiesOver (Ideal.span {↑(Ideal.absNorm (Ideal.under ℤ I))})

theorem Int.cast_mem_ideal_iff {R : Type u_1} [Ring R] {I : Ideal R} {d : ℤ} : ↑d ∈ I ↔ ↑(Ideal.absNorm (Ideal.under ℤ I)) ∣ d

theorem Int.absNorm_under_mem {R : Type u_1} [Ring R] (I : Ideal R) : ↑(Ideal.absNorm (Ideal.under ℤ I)) ∈ I

theorem Int.absNorm_under_eq_sInf {R : Type u_1} [Ring R] (I : Ideal R) : Ideal.absNorm (Ideal.under ℤ I) = sInf {d : ℕ | 0 < d ∧ ↑d ∈ I}

theorem Int.absNorm_under_dvd_absNorm {S : Type u_2} [CommRing S] [IsDedekindDomain S] (I : Ideal S) : Ideal.absNorm (Ideal.under ℤ I) ∣ Ideal.absNorm I

theorem Ideal.ringChar_quot {S : Type u_2} [CommRing S] (I : Ideal S) : ringChar (S ⧸ I) = absNorm (under ℤ I)

theorem Nat.absNorm_under_prime {R : Type u_1} [CommRing R] [IsDomain R] [Algebra.IsIntegral ℤ R] (P : Ideal R) [P.IsPrime] [NeZero P] : Prime (Ideal.absNorm (Ideal.under ℤ P))