English
A scheme is Noetherian iff there exists a finite affine open cover with Noetherian rings of global sections.
Русский
Схема Ноетериевая тогда и только тогда, когда существует конечное афинное покрытие с Ноетериевскими кольцами глобальных секций.
LaTeX
$$$\forall 𝒰\text{ finite affine open cover},\; \text{IsNoetherian}(X) \iff \forall i, \text{IsNoetherianRing}(\Gamma(𝒰.X_i, ⊤)).$$$
Lean4
/-- A Noetherian scheme has a Noetherian underlying topological space. -/
@[stacks 01OZ]
instance (priority := 100) noetherianSpace [IsNoetherian X] : NoetherianSpace X :=
by
apply TopologicalSpace.noetherian_univ_iff.mp
let 𝒰 := X.affineCover.finiteSubcover
rw [← 𝒰.iUnion_range]
suffices ∀ i : 𝒰.I₀, NoetherianSpace (Set.range <| (𝒰.f i).base) by apply NoetherianSpace.iUnion
intro i
have : IsAffine (𝒰.X i) := by
rw [X.affineCover.finiteSubcover_X]
apply Scheme.isAffine_affineCover
let U : X.affineOpens := ⟨Scheme.Hom.opensRange (𝒰.f i), isAffineOpen_opensRange _⟩
convert noetherianSpace_of_isAffineOpen U.1 U.2
apply IsLocallyNoetherian.component_noetherian
