Noetherian and Locally Noetherian Schemes

We introduce the concept of (locally) Noetherian schemes, giving definitions, equivalent conditions, and basic properties.

Main definitions

• AlgebraicGeometry.IsLocallyNoetherian: A scheme is locally Noetherian if the components of the structure sheaf at each affine open are Noetherian rings.

• AlgebraicGeometry.IsNoetherian: A scheme is Noetherian if it is locally Noetherian and quasi-compact as a topological space.

Main results

• AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover: A scheme is locally Noetherian if and only if it is covered by affine opens whose sections are Noetherian rings.

• AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace: A locally Noetherian scheme is quasi-separated.

• AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover: A scheme is Noetherian if and only if it is covered by finitely many affine opens whose sections are Noetherian rings.

• AlgebraicGeometry.IsNoetherian.noetherianSpace: A Noetherian scheme is topologically a Noetherian space.

References

• Stacks: Noetherian Schemes
• [Robin Hartshorne, Algebraic Geometry][Har77]

class AlgebraicGeometry.IsLocallyNoetherian (X : AlgebraicGeometry.Scheme) : Prop

A scheme X is locally Noetherian if 𝒪ₓ(U) is Noetherian for all affine U.

• component_noetherian : ∀ (U : ↑X.affineOpens), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑U))

theorem AlgebraicGeometry.IsLocallyNoetherian.component_noetherian {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocallyNoetherian X] (U : ↑X.affineOpens) : IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑U))

theorem AlgebraicGeometry.isNoetherianRing_of_away {R : Type u} [CommRing R] (S : Finset R) (hS : Ideal.span ↑S = ⊤) (hN : ∀ (s : { x : R // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)) : IsNoetherianRing R

Let R be a ring, and f i a finite collection of elements of R generating the unit ideal. If the localization of R at each f i is noetherian, so is R.

We follow the proof given in [Har77], Proposition II.3.2

theorem AlgebraicGeometry.isLocallyNoetherian_of_affine_cover {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} {S : ι → ↑X.affineOpens} (hS : ⨆ (i : ι), ↑(S i) = ⊤) (hS' : ∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i)))) : AlgebraicGeometry.IsLocallyNoetherian X

If a scheme X has a cover by affine opens whose sections are Noetherian rings, then X is locally Noetherian.

theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} {S : ι → ↑X.affineOpens} (hS : ⨆ (i : ι), ↑(S i) = ⊤) : AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i)))

A scheme is locally Noetherian if and only if it is covered by affine opens whose sections are noetherian rings.

See [Har77], Proposition II.3.2.

theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] : AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing ↑((𝒰.obj i).presheaf.obj (Opposite.op ⊤))

A version of isLocallyNoetherian_iff_of_iSup_eq_top using Scheme.OpenCover.

theorem AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsLocallyNoetherian Y] : AlgebraicGeometry.IsLocallyNoetherian X

theorem AlgebraicGeometry.isLocallyNoetherian_iff_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.IsLocallyNoetherian (𝒰.obj i)

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

instance AlgebraicGeometry.instNoetherianSpaceαTopologicalSpaceCarrierCommRingCatSpecOfIsNoetherianRingCommRing {R : CommRingCat} [IsNoetherianRing ↑R] : TopologicalSpace.NoetherianSpace ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace

If R is a noetherian ring, Spec R is a noetherian topological space.

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.noetherianSpace_of_isAffine {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ⊤))] : TopologicalSpace.NoetherianSpace ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.noetherianSpace_of_isAffineOpen {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op U))] : TopologicalSpace.NoetherianSpace ↑↑(↑U).toPresheafedSpace

@[instance 100]

instance AlgebraicGeometry.instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion {X : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] {f : Z ⟶ X} [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.QuasiCompact f

Any open immersion Z ⟶ X with X locally Noetherian is quasi-compact.

Stacks: Lemma 01OX

Equations

• ⋯ = ⋯

@[instance 100]

instance AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] : QuasiSeparatedSpace ↑↑X.toPresheafedSpace

A locally Noetherian scheme is quasi-separated.

Stacks: Lemma 01OY

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isNoetherian_iff (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.IsNoetherian X ↔ AlgebraicGeometry.IsLocallyNoetherian X ∧ CompactSpace ↑↑X.toPresheafedSpace

class AlgebraicGeometry.IsNoetherian (X : AlgebraicGeometry.Scheme) extends AlgebraicGeometry.IsLocallyNoetherian , CompactSpace : Prop

A scheme X is Noetherian if it is locally Noetherian and compact.

theorem AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} [Finite ι] {S : ι → ↑X.affineOpens} (hS : ⨆ (i : ι), ↑(S i) = ⊤) : AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i)))

A scheme is Noetherian if and only if it is covered by finitely many affine opens whose sections are noetherian rings.

theorem AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover {X : AlgebraicGeometry.Scheme} {𝒰 : X.OpenCover} [Finite 𝒰.J] [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] : AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing ↑((𝒰.obj i).presheaf.obj (Opposite.op ⊤))

A version of isNoetherian_iff_of_finite_iSup_eq_top using Scheme.OpenCover.

@[instance 100]

instance AlgebraicGeometry.IsNoetherian.noetherianSpace {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] : TopologicalSpace.NoetherianSpace ↑↑X.toPresheafedSpace

A Noetherian scheme has a Noetherian underlying topological space.

Stacks, Lemma 01OZ

Equations

• ⋯ = ⋯

@[instance 100]

instance AlgebraicGeometry.quasiCompact_of_noetherianSpace_source {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↑↑X.toPresheafedSpace] (f : X ⟶ Y) : AlgebraicGeometry.QuasiCompact f

Any morphism of schemes f : X ⟶ Y with X Noetherian is quasi-compact.

Stacks, Lemma 01P0

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.instIsLocallyNoetherianSpecOfIsNoetherianRingαCommRing {R : CommRingCat} [IsNoetherianRing ↑R] : AlgebraicGeometry.IsLocallyNoetherian (AlgebraicGeometry.Spec R)

If R is a Noetherian ring, Spec R is a locally Noetherian scheme.

Equations

• ⋯ = ⋯

@[instance 100]

instance AlgebraicGeometry.instIsNoetherianRingαCommRingOfIsLocallyNoetherianSpec {R : CommRingCat} [AlgebraicGeometry.IsLocallyNoetherian (AlgebraicGeometry.Spec R)] : IsNoetherianRing ↑R

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.instIsNoetherianSpecOfIsNoetherianRingαCommRing {R : CommRingCat} [IsNoetherianRing ↑R] : AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec R)

If R is a Noetherian ring, Spec R is a Noetherian scheme.

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.instIsNoetherianSpecOfOfIsNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] : AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec (CommRingCat.of R))

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isNoetherian_Spec {R : CommRingCat} : AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec R) ↔ IsNoetherianRing ↑R

R is a Noetherian ring if and only if Spec R is a Noetherian scheme.

theorem AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] : (irreducibleComponents ↑↑X.toPresheafedSpace).Finite

A Noetherian scheme has a finite number of irreducible components.

Stacks, Lemma 0BA8