Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isLocallyNoetherian_iff_openCover

∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsLocallyNoetherian (𝒰.X i)

If 𝒰 is an open cover of a scheme X, then X is locally Noetherian if and only if 𝒰.X i are all locally Noetherian.

Defined in

Mathlib.AlgebraicGeometry.Noetherian

Cited by

2 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound