Documentation

Mathlib.AlgebraicGeometry.Artinian

Artinian and Locally Artinian Schemes #

We define and prove basic properties about Artinian and locally Artinian Schemes.

Main definitions #

Main results #

TODO(Brian-Nugent): Show that all Artinian schemes are affine.

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

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

Instances
    source
    instance AlgebraicGeometry.IsLocallyArtinian.isLocallyNoetherian {X : Scheme} [h : IsLocallyArtinian X] :
    IsLocallyNoetherian X
    source
    instance AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine {X : Scheme} [h : IsLocallyArtinian X] [IsAffine X] :
    IsArtinianRing ā†‘(X.presheaf.obj (Opposite.op āŠ¤))
    source
    theorem AlgebraicGeometry.IsLocallyArtinian.of_topologicalKrullDim_le_zero {X : Scheme} [IsLocallyNoetherian X] (h : topologicalKrullDim ā†„X ā‰¤ 0) :
    IsLocallyArtinian X
    source
    theorem AlgebraicGeometry.IsLocallyArtinian.of_isLocallyNoetherian_of_discreteTopology {X : Scheme} [IsLocallyNoetherian X] [DiscreteTopology ā†„X] :
    IsLocallyArtinian X
    source
    instance AlgebraicGeometry.instIsLocallyArtinianToScheme {X : Scheme} [IsLocallyArtinian X] {U : X.Opens} :
    IsLocallyArtinian ā†‘U
    source
    instance AlgebraicGeometry.instIsLocallyArtinianXScheme {X : Scheme} [IsLocallyArtinian X] {U : X.OpenCover} (i : U.Iā‚€) :
    IsLocallyArtinian (U.X i)
    source
    @[instance 100]
    instance AlgebraicGeometry.IsLocallyArtinian.discreteTopology {X : Scheme} [IsLocallyArtinian X] :
    DiscreteTopology ā†„X
    source
    @[deprecated AlgebraicGeometry.IsLocallyArtinian.discreteTopology (since := "2026-01-14")]
    theorem AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine {X : Scheme} [IsLocallyArtinian X] :
    DiscreteTopology ā†„X

    Alias of AlgebraicGeometry.IsLocallyArtinian.discreteTopology.

    source
    theorem AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology {X : Scheme} :
    IsLocallyArtinian X ā†” IsLocallyNoetherian X āˆ§ DiscreteTopology ā†„X
    source
    theorem AlgebraicGeometry.IsLocallyArtinian.of_isImmersion {X Y : Scheme} (f : X āŸ¶ Y) [IsImmersion f] [IsLocallyArtinian Y] :
    IsLocallyArtinian X
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.isLocallyArtinianScheme_Spec {R : CommRingCat} :
    IsLocallyArtinian (Spec R) ā†” IsArtinianRing ā†‘R

    A commutative ring R is Artinian if and only if Spec R is an Artinian scheme.

    source
    theorem AlgebraicGeometry.isLocallyArtinian_iff_openCover {X : Scheme} (š’° : X.OpenCover) :
    IsLocallyArtinian X ā†” āˆ€ (i : š’°.Iā‚€), IsLocallyArtinian (š’°.X i)
    source
    theorem AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover {X : Scheme} {Ī¹ : Type u_1} {U : Ī¹ ā†’ X.Opens} (hU : TopologicalSpace.IsOpenCover U) (hU' : āˆ€ (i : Ī¹), IsAffineOpen (U i)) :
    IsLocallyArtinian X ā†” āˆ€ (i : Ī¹), IsArtinianRing ā†‘(X.presheaf.obj (Opposite.op (U i)))
    source
    class AlgebraicGeometry.IsArtinianScheme (X : Scheme) extends AlgebraicGeometry.IsLocallyArtinian X, CompactSpace ā†„X :
    Prop

    A scheme is Artinian if it is locally Artinian and quasi-compact

    Instances
      source
      theorem AlgebraicGeometry.isArtinianScheme_iff (X : Scheme) :
      IsArtinianScheme X ā†” IsLocallyArtinian X āˆ§ CompactSpace ā†„X
      source
      @[instance 100]
      instance AlgebraicGeometry.IsArtinianScheme.finite {X : Scheme} [IsArtinianScheme X] :
      Finite ā†„X

      The underlying type of an Artinian Scheme is finite

      source
      @[instance 100]
      instance AlgebraicGeometry.IsArtinianScheme.isNoetherianScheme {X : Scheme} [IsArtinianScheme X] :
      IsNoetherian X
      source
      theorem AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology {X : Scheme} :
      IsArtinianScheme X ā†” IsNoetherian X āˆ§ DiscreteTopology ā†„X

      A scheme is Artinian if and only if it is Noetherian and has the discrete topology.

      source
      instance AlgebraicGeometry.instIsArtinianSchemeSpecOfIsArtinianRingCarrier {R : CommRingCat} [IsArtinianRing ā†‘R] :
      IsArtinianScheme (Spec R)
      source
      theorem AlgebraicGeometry.Scheme.isArtinianScheme_Spec {R : CommRingCat} :
      IsArtinianScheme (Spec R) ā†” IsArtinianRing ā†‘R

      A commutative ring R is Artinian if and only if Spec R is an Artinian scheme