quasiCompact_of_noetherianSpace_source

English

A scheme is Noetherian if finitely many affine opens cover it and each corresponding ring is Noetherian.

Русский

Схема Ноетериевая, если конечное число афинных открытий покрывает её и соответствующие кольца Ноетериевые.

LaTeX

$$$[\text{Finite } 𝒰] \Rightarrow \text{IsNoetherian}(X) \iff \forall i, \text{IsNoetherianRing}(\Gamma(𝒰.X_i, ⊤)).$$$

Lean4

/-- Any morphism of schemes `f : X ⟶ Y` with `X` Noetherian is quasi-compact. -/
@[stacks 01P0]
instance (priority := 100) quasiCompact_of_noetherianSpace_source {X Y : Scheme} [NoetherianSpace X] (f : X ⟶ Y) :
    QuasiCompact f :=
  ⟨fun _ _ _ => NoetherianSpace.isCompact _⟩

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