English
A scheme is locally Noetherian iff every member of an open cover is locally Noetherian.
Русский
Схема локально Ноетерова тогда и только тогда, когда каждый элемент открытого покрытия локально Ноетерова.
LaTeX
$$$\text{IsLocallyNoetherian}(X) \iff \forall i, \text{IsLocallyNoetherian}(\mathcal{U}_i).$$$
Lean4
/-- If `𝒰` is an open cover of a scheme `X`, then `X` is locally Noetherian if and only if
`𝒰.X i` are all locally Noetherian. -/
theorem isLocallyNoetherian_iff_openCover (𝒰 : Scheme.OpenCover X) :
IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i) :=
by
constructor
· intro h i
exact isLocallyNoetherian_of_isOpenImmersion (𝒰.f i)
· rw [isLocallyNoetherian_iff_of_affine_openCover (𝒰 := 𝒰.affineRefinement.openCover)]
intro h i
exact
@isNoetherianRing_of_ringEquiv _ _ _ _
(IsOpenImmersion.ΓIsoTop (PreZeroHypercover.f _ i.2)).symm.commRingCatIsoToRingEquiv
(IsLocallyNoetherian.component_noetherian ⟨_, isAffineOpen_opensRange _⟩)
