feat(RingTheory/Artinian): the collection of maximal ideals in an art…

…inian ring is finite (#9087)

Co-PR: #9088 (minimal prime ideals in Noetherian ring are finite)

Mathlib/RingTheory/Artinian.lean

@@ -498,4 +498,27 @@ instance isMaximal_of_isPrime (p : Ideal R) [p.IsPrime] : p.IsMaximal :=
       localization_surjective (nonZeroDivisors (R ⧸ p)) (FractionRing (R ⧸ p))⟩).isField _
     <| Field.toIsField <| FractionRing (R ⧸ p)
 
+lemma isPrime_iff_isMaximal (p : Ideal R) : p.IsPrime ↔ p.IsMaximal :=
+  ⟨fun _ ↦ isMaximal_of_isPrime p, fun h ↦ h.isPrime⟩
+
+variable (R) in
+lemma primeSpectrum_finite : {I : Ideal R | I.IsPrime}.Finite := by
+  set Spec := {I : Ideal R | I.IsPrime}
+  obtain ⟨_, ⟨s, rfl⟩, H⟩ := set_has_minimal
+    (range (Finset.inf · Subtype.val : Finset Spec → Ideal R)) ⟨⊤, ∅, by simp⟩
+  refine ⟨⟨s, fun p ↦ ?_⟩⟩
+  classical
+  obtain ⟨q, hq1, hq2⟩ := p.2.inf_le'.mp <| inf_eq_right.mp <|
+    inf_le_right.eq_of_not_lt (H (p ⊓ s.inf Subtype.val) ⟨insert p s, by simp⟩)
+  rwa [← Subtype.ext <| (@isMaximal_of_isPrime _ _ _ _ q.2).eq_of_le p.2.1 hq2]
+
+variable (R) in
+/--
+[Stacks Lemma 00J7](https://stacks.math.columbia.edu/tag/00J7)
+-/
+lemma maximal_ideals_finite : {I : Ideal R | I.IsMaximal}.Finite := by
+  simp_rw [← isPrime_iff_isMaximal]
+  apply primeSpectrum_finite R
+
+
 end IsArtinianRing