Schemes in mathlib

This file contains an introduction to scheme theory in mathlib.

Prime spectrum of a ring

The unbundled vs. bundled barrier.

The composition of two ring homomorphisms can be expressed as:

The first approach is called unbundled and the second one bundled: In the first version, the CommRing structure on R is provided as a separate argument. It is unbundled from the type R. In the second version, the CommRing structure is bundled with the type in a term R : CommRingCat.

Note that we have to write R →+* S in the first case to talk about a ring homomorphism f. This is because R S : Type. In the case of R S : CommRingCat, the types contain enough information to infer that R ⟶ S denotes a ring homomorphism.

Moreover, in the bundled version we can use the notation f ≫ g to denote composition of the ring homomorphisms f and g.

Most of the topology and commutative algebra library is written in the unbundled style. But to talk about the category of commutative rings or the category of topological spaces, this category needs a type of objects.

Note: This requires open CategoryTheory!

Definition of Scheme

As you would expect, a Scheme is defined as a locally ringed space that is locally isomorphic to the spectrum of a ring.

One of the reasons we use the bundled approach for Schemes, is the heavy reliance on category theoretical constructions.

Affine schemes

Categories and functors

We have already seen examples of categories, but not yet examples of functors.

Stalks, residue fields and fibres

def Stalks.fiber {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) : AlgebraicGeometry.Scheme

The fibre of f over y is, by definition, the fibre product

X ×[Y] Spec κ(y) ------> Spec κ(y)
      |                       |
      |                       |
      v                       |
      X --------------------> Y

Equations

• Stalks.fiber f y = CategoryTheory.Limits.pullback f (Y.fromSpecResidueField y)

def Stalks.fiberι {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) : fiber f y ⟶ X

The immersion X ×[Y] Spec κ(y) ⟶ X.

Equations

• Stalks.fiberι f y = CategoryTheory.Limits.pullback.fst f (Y.fromSpecResidueField y)

def Stalks.fiberToSpecResidueField {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) : fiber f y ⟶ AlgebraicGeometry.Spec (Y.residueField y)

The projection X ×[Y] Spec κ(y) ⟶ Spec κ(y).

Equations

• Stalks.fiberToSpecResidueField f y = CategoryTheory.Limits.pullback.snd f (Y.fromSpecResidueField y)

In mathlib these are called Hom.fiber, Hom.fiberι and Hom.fiberToSpecResidueField and we can for example write f.fiber.

Subschemes

Open subschemes

Instead of working with U : X.Opens, it is often convenient to allow arbitrary open immersions instead.

Closed subschemes

Properties of morphisms

Mathlib knows many properties of morphisms. Browsing the AlgebraicGeometry/Morphisms folder gives an overview. The properties are defined as type classes.

Morphism properties

Reduction to affine case

(Open) covers

Any reduction to a local problem starts with an (affine) open cover. These can be pulled back along morphisms, refined, etc.

Properties of properties

Example: Flat morphisms

class Flat {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

• flat_of_isAffineOpen (U : Y.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat

theorem flat_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Flat f ↔ ∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat

instance instHasRingHomPropertyFlatFlat : AlgebraicGeometry.HasRingHomProperty @Flat fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Flat

def stalkMapIsoOfIsPullback {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} (g : Y ⟶ Z) (h : CategoryTheory.IsPullback fst snd f g) [AlgebraicGeometry.IsOpenImmersion g] (x : ↥P) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap snd x) ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f ((CategoryTheory.ConcreteCategory.hom fst.base) x))

If P = X ×[Z] Y and Y ⟶ Z is an open immersion, then the stalk map of P ⟶ Y at some x : P is isomorphic to the stalk map of X ⟶ Z at the image of x.

Equations

• One or more equations did not get rendered due to their size.

theorem flat_of_flat_stalkMap {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).Flat) : Flat f

Schemes over a base

We have multiple ways of talking about a scheme over a base.

Varieties

There is no AlgebraicGeometry.Variety and there will most likely never be such a definition.

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

But you are free to create your local definition of variety (downstream of mathlib).

• diagonal_isClosedImmersion : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal s)
• finiteType_of_affine_subset (U : ↑(Spec (CommRingCat.of k)).affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map s.base).obj ↑U) : (CommRingCat.Hom.hom (Scheme.Hom.appLE s (↑U) (↑V) e)).FiniteType

More topics