18.9. More topics🔗

Here are a few more pointers to relevant objects in algebraic geometry, that we don't explain in detail here.

There is no AlgebraicGeometry.Variety and there will most likely never be such a definition. But you are free to create your local definition of variety (downstream of mathlib), for example like so:

class Variety {X : Scheme} {k : Type} [Field k]
      (s : X ⟶ Spec (.of k)) : Prop
    extends IsSeparated s, LocallyOfFiniteType s

Function field of a scheme.

AlgebraicGeometry.Scheme.functionField.{u_1} (X : Scheme) [IrreducibleSpace ↥X] : CommRingCat#check Scheme.functionField

(Locally) Noetherian schemes.

AlgebraicGeometry.IsLocallyNoetherian.{u_1} (X : Scheme) : Prop#check IsLocallyNoetherian
AlgebraicGeometry.IsNoetherian.{u_1} (X : Scheme) : Prop#check IsNoetherian

Projective spectrum of a graded ring.

variable {σ : Type} {A : Type}
variable [CommRing A] [SetLike σ A] [AddSubgroupClass σ A]
variable (𝒜 : ℕ → σ) [GradedRing 𝒜]
Proj 𝒜 : Scheme#check Proj 𝒜