Documentation

Mathlib.AlgebraicGeometry.Noetherian

Noetherian and Locally Noetherian Schemes #

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

Main definitions #

Main results #

References #

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

A scheme X is locally Noetherian if š’Ŗā‚“(U) is Noetherian for all affine U.

Instances
    source
    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

    source
    theorem AlgebraicGeometry.isLocallyNoetherian_of_affine_cover {X : Scheme} {Ī¹ : Sort u_1} {S : Ī¹ ā†’ ā†‘X.affineOpens} (hS : ā؆ (i : Ī¹), ā†‘(S i) = āŠ¤) (hS' : āˆ€ (i : Ī¹), IsNoetherianRing ā†‘(X.presheaf.obj (Opposite.op ā†‘(S i)))) :
    IsLocallyNoetherian X

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

    source
    theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top {X : Scheme} {Ī¹ : Sort u_1} {S : Ī¹ ā†’ ā†‘X.affineOpens} (hS : ā؆ (i : Ī¹), ā†‘(S i) = āŠ¤) :
    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.

    source
    theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover {X : Scheme} (š’° : X.OpenCover) [āˆ€ (i : š’°.Iā‚€), IsAffine (š’°.X i)] :
    IsLocallyNoetherian X ā†” āˆ€ (i : š’°.Iā‚€), IsNoetherianRing ā†‘((š’°.X i).presheaf.obj (Opposite.op āŠ¤))

    A version of isLocallyNoetherian_iff_of_iSup_eq_top using Scheme.OpenCover.

    source
    theorem AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion {X Y : Scheme} (f : X āŸ¶ Y) [IsOpenImmersion f] [IsLocallyNoetherian Y] :
    IsLocallyNoetherian X
    source
    theorem AlgebraicGeometry.isLocallyNoetherian_iff_openCover {X : Scheme} (š’° : X.OpenCover) :
    IsLocallyNoetherian X ā†” āˆ€ (i : š’°.Iā‚€), 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.

    source
    instance AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier {R : CommRingCat} [IsNoetherianRing ā†‘R] :
    TopologicalSpace.NoetherianSpace ā†„(Spec R)

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

    source
    theorem AlgebraicGeometry.noetherianSpace_of_isAffine {X : Scheme} [IsAffine X] [IsNoetherianRing ā†‘(X.presheaf.obj (Opposite.op āŠ¤))] :
    TopologicalSpace.NoetherianSpace ā†„X
    source
    theorem AlgebraicGeometry.noetherianSpace_of_isAffineOpen {X : Scheme} (U : X.Opens) (hU : IsAffineOpen U) [IsNoetherianRing ā†‘(X.presheaf.obj (Opposite.op U))] :
    TopologicalSpace.NoetherianSpace ā†„ā†‘U
    source
    @[instance 100]
    instance AlgebraicGeometry.instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion {X Z : Scheme} [IsLocallyNoetherian X] {f : Z āŸ¶ X} [IsOpenImmersion f] :
    QuasiCompact f

    Any open immersion Z āŸ¶ X with X locally Noetherian is quasi-compact.

    source
    @[instance 100]
    instance AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace {X : Scheme} [IsLocallyNoetherian X] :
    QuasiSeparatedSpace ā†„X

    A locally Noetherian scheme is quasi-separated.

    source
    class AlgebraicGeometry.IsNoetherian (X : Scheme) extends AlgebraicGeometry.IsLocallyNoetherian X, CompactSpace ā†„X :
    Prop

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

    Instances
      source
      theorem AlgebraicGeometry.isNoetherian_iff (X : Scheme) :
      IsNoetherian X ā†” IsLocallyNoetherian X āˆ§ CompactSpace ā†„X
      source
      theorem AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top {X : Scheme} {Ī¹ : Sort u_1} [Finite Ī¹] {S : Ī¹ ā†’ ā†‘X.affineOpens} (hS : ā؆ (i : Ī¹), ā†‘(S i) = āŠ¤) :
      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.

      source
      theorem AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover {X : Scheme} {š’° : X.OpenCover} [Finite š’°.Iā‚€] [āˆ€ (i : š’°.Iā‚€), IsAffine (š’°.X i)] :
      IsNoetherian X ā†” āˆ€ (i : š’°.Iā‚€), IsNoetherianRing ā†‘((š’°.X i).presheaf.obj (Opposite.op āŠ¤))

      A version of isNoetherian_iff_of_finite_iSup_eq_top using Scheme.OpenCover.

      source
      @[instance 100]
      instance AlgebraicGeometry.IsNoetherian.noetherianSpace {X : Scheme} [IsNoetherian X] :
      TopologicalSpace.NoetherianSpace ā†„X

      A Noetherian scheme has a Noetherian underlying topological space.

      source
      @[instance 100]
      instance AlgebraicGeometry.quasiCompact_of_noetherianSpace_source {X Y : Scheme} [TopologicalSpace.NoetherianSpace ā†„X] (f : X āŸ¶ Y) :
      QuasiCompact f

      Any morphism of schemes f : X āŸ¶ Y with X Noetherian is quasi-compact.

      source
      instance AlgebraicGeometry.instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier {R : CommRingCat} [IsNoetherianRing ā†‘R] :
      IsLocallyNoetherian (Spec R)

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

      source
      @[instance 100]
      instance AlgebraicGeometry.instIsNoetherianRingCarrierOfIsLocallyNoetherianSpec {R : CommRingCat} [IsLocallyNoetherian (Spec R)] :
      IsNoetherianRing ā†‘R
      source
      instance AlgebraicGeometry.instIsNoetherianSpecOfIsNoetherianRingCarrier {R : CommRingCat} [IsNoetherianRing ā†‘R] :
      IsNoetherian (Spec R)

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

      source
      instance AlgebraicGeometry.instIsNoetherianSpecOfOfIsNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] :
      IsNoetherian (Spec (CommRingCat.of R))
      source
      instance AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian {X : Scheme} [IsLocallyNoetherian X] {x : ā†„X} :
      IsNoetherianRing ā†‘(X.presheaf.stalk x)
      source
      theorem AlgebraicGeometry.isNoetherian_Spec {R : CommRingCat} :
      IsNoetherian (Spec R) ā†” IsNoetherianRing ā†‘R

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

      source
      theorem AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian {X : Scheme} [IsNoetherian X] :
      (irreducibleComponents ā†„X).Finite

      A Noetherian scheme has a finite number of irreducible components.