Structures · Geometry
AlgebraicGeometry.IsLocallyArtinian
A scheme X is locally Artinian if 𝒪ₓ(U) is Artinian for all affine U.
- Defined in
- Mathlib.AlgebraicGeometry.Artinian
- Shape
- One type argument · adds isArtinianRing_presheaf_obj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsLocallyArtinian is also a
Provided automatically by
Concrete types that are instances3
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.PreZeroHypercover.X
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite
- AlgebraicGeometry.IsLocallyArtinian.of_isImmersion
- AlgebraicGeometry.instIsLocallyArtinianXScheme
- AlgebraicGeometry.instIsLocallyArtinianToScheme
- AlgebraicGeometry.IsFinite.of_locallyQuasiFinite
- AlgebraicGeometry.IsLocallyArtinian.discreteTopology
- AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine
- AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine
- AlgebraicGeometry.IsLocallyArtinian.isLocallyNoetherian
- AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj