ringKrullDim_nat — Mathlib

English

The ring Krull dimension of the natural numbers is 2.

Русский

Крулль размерность кольца ℕ равна 2.

LaTeX

$$$\operatorname{ringKrullDim}(\mathbb{N}) = 2$$$

Lean4

theorem ringKrullDim_nat : ringKrullDim ℕ = 2 :=
  by
  refine le_antisymm (iSup_le fun s ↦ le_of_not_gt fun hs ↦ ?_) ?_
  · replace hs : 2 < s.length := ENat.coe_lt_coe.mp (WithBot.coe_lt_coe.mp hs)
    let s := s.take ⟨3, by cutsat⟩
    have : NeZero s.length := ⟨three_ne_zero⟩
    have h1 : ⊥ < (s 1).asIdeal := bot_le.trans_lt (s.step 0)
    obtain hmax | ⟨p, hp, hsp⟩ := (Ideal.isPrime_nat_iff.mp (s 1).2).resolve_left h1.ne'
    · exact (le_maximalIdeal_of_isPrime (s 2).asIdeal).not_gt (hmax.symm.trans_lt (s.step 1))
    obtain hmax | ⟨q, hq, hsq⟩ := (Ideal.isPrime_nat_iff.mp (s 2).2).resolve_left (h1.trans (s.step 1)).ne'
    · exact (le_maximalIdeal_of_isPrime (s 3).asIdeal).not_gt (hmax.symm.trans_lt (s.step 2))
    ·
      exact
        hq.not_isUnit <|
          (Ideal.span_singleton_lt_span_singleton.mp
                ((hsp.symm.trans_lt (s.step 1)).trans_eq hsq)).isUnit_of_irreducible_right
            hp
  · refine
      le_iSup_of_le
        ⟨2,
          ![⊥, ⟨_, (span_singleton_prime two_ne_zero).mpr <| Nat.prime_iff.mp Nat.prime_two⟩,
            ⟨_, (maximalIdeal.isMaximal ℕ).isPrime⟩],
          fun i ↦ ?_⟩
        le_rfl
    fin_cases i
    · exact bot_lt_iff_ne_bot.mpr (Ideal.span_singleton_eq_bot.not.mpr two_ne_zero)
    · simp_rw [Nat.maximalIdeal_eq_span_two_three]
      exact
        SetLike.lt_iff_le_and_exists.mpr
          ⟨Ideal.span_mono (by simp), 3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Похожие утверждения