Prime ideals in ℕ and ℤ

Main results

• Ideal.isPrime_nat_iff: the prime ideals in ℕ are ⟨0⟩, ⟨p⟩ (for prime p), and ⟨2, 3⟩ = {1}ᶜ. The proof follows https://math.stackexchange.com/a/4224486.

• Ideal.isPrime_int_iff : the prime ideals in ℤ are ⟨0⟩ and ⟨p⟩ (for prime p).

instance instIsLocalRingNat : IsLocalRing ℕ

The natural numbers form a local semiring.

theorem Nat.mem_maximalIdeal_iff {n : ℕ} : n ∈ IsLocalRing.maximalIdeal ℕ ↔ n ≠ 1

theorem Nat.coe_maximalIdeal : ↑(IsLocalRing.maximalIdeal ℕ) = {1}ᶜ

theorem Nat.maximalIdeal_eq_span_two_three : IsLocalRing.maximalIdeal ℕ = Ideal.span {2, 3}

theorem Nat.one_mem_span_iff {s : Set ℕ} : 1 ∈ Ideal.span s ↔ 1 ∈ s

theorem Nat.one_mem_closure_iff {s : Set ℕ} : 1 ∈ AddSubmonoid.closure s ↔ 1 ∈ s

theorem Ideal.isPrime_nat_iff {P : Ideal ℕ} : P.IsPrime ↔ P = ⊥ ∨ P = IsLocalRing.maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}

theorem Ideal.map_comap_natCastRingHom_int {I : Ideal ℤ} : map (Nat.castRingHom ℤ) (comap (Nat.castRingHom ℤ) I) = I

theorem Ideal.isPrime_int_iff {P : Ideal ℤ} : P.IsPrime ↔ P = ⊥ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {↑p}

theorem ringKrullDim_nat : ringKrullDim ℕ = 2