Prove2Me

A Noetherian scheme has finitely many irreducible components

Proved
NoetherianScheme.finite_irreducibleComponents

by Lucas · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynoetherian

Let XX be a Noetherian scheme. Then the set of irreducible components of XX (the maximal irreducible closed subsets of its underlying space) is finite.

Preamble
import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField
Formal statement
namespace NoetherianScheme

theorem finite_irreducibleComponents (X : Scheme.{u}) (hX : IsNoetherianScheme X) :
    (irreducibleComponents X).Finite := by sorry

end NoetherianScheme
Source
Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), section "Properties and Noetherian hypotheses": "Any Noetherian scheme can only have finitely many irreducible components." [1] = Stacks Project Lemma 28.5.7 (Tag 0BA8).
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph