(Co)Limits of Schemes #

We construct various limits and colimits in the category of schemes.

The existence of fibred products was shown in Mathlib/AlgebraicGeometry/Pullbacks.lean.
Spec ℤ is the terminal object.
The preceding two results imply that Scheme has all finite limits.
The empty scheme is the (strict) initial object.

Todo #

Coproducts exists (and the forgetful functors preserve them).

source

noncomputable def AlgebraicGeometry.specZIsTerminal :

CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of ℤ)))

Spec ℤ is the terminal object in the category of schemes.

Instances For

source

instance AlgebraicGeometry.instHasTerminalSchemeInstCategoryScheme :

CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme

source

instance AlgebraicGeometry.instIsAffineTerminalSchemeInstCategorySchemeInstHasTerminalSchemeInstCategoryScheme :

AlgebraicGeometry.IsAffine (⊤_ AlgebraicGeometry.Scheme)

source

instance AlgebraicGeometry.instHasFiniteLimitsSchemeInstCategoryScheme :

CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme

source

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : ↑↑∅.toPresheafedSpace) :

↑(AlgebraicGeometry.Scheme.emptyTo X).val.base x = PEmpty.elim x

source

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_val_c_app (X : AlgebraicGeometry.Scheme) (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) :

(AlgebraicGeometry.Scheme.emptyTo X).val.c.app U = CategoryTheory.Limits.IsTerminal.from CommRingCat.punitIsTerminal (X.presheaf.obj U)

source

def AlgebraicGeometry.Scheme.emptyTo (X : AlgebraicGeometry.Scheme) :

∅ ⟶ X

The map from the empty scheme.

Instances For

source

theorem AlgebraicGeometry.Scheme.empty_ext {X : AlgebraicGeometry.Scheme} (f : ∅ ⟶ X) (g : ∅ ⟶ X) :

f = g

source

theorem AlgebraicGeometry.Scheme.eq_emptyTo {X : AlgebraicGeometry.Scheme} (f : ∅ ⟶ X) :

f = AlgebraicGeometry.Scheme.emptyTo X

source

instance AlgebraicGeometry.Scheme.hom_unique_of_empty_source (X : AlgebraicGeometry.Scheme) :

Unique (∅ ⟶ X)

source

def AlgebraicGeometry.emptyIsInitial :

CategoryTheory.Limits.IsInitial ∅

The empty scheme is the initial object in the category of schemes.

Instances For

source

@[simp]

theorem AlgebraicGeometry.emptyIsInitial_to :

CategoryTheory.Limits.IsInitial.to AlgebraicGeometry.emptyIsInitial = AlgebraicGeometry.Scheme.emptyTo

source

instance AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceEmpty :

IsEmpty ↑↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace

source

instance AlgebraicGeometry.spec_punit_isEmpty :

IsEmpty ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of PUnit.{u_1 + 1} ))).toPresheafedSpace

source

instance AlgebraicGeometry.isOpenImmersion_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑X.toPresheafedSpace] :

AlgebraicGeometry.IsOpenImmersion f

source

instance AlgebraicGeometry.isIso_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↑↑Y.toPresheafedSpace] :

CategoryTheory.IsIso f

source

noncomputable def AlgebraicGeometry.isInitialOfIsEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty ↑↑X.toPresheafedSpace] :

CategoryTheory.Limits.IsInitial X

A scheme is initial if its underlying space is empty .

Instances For

source

noncomputable def AlgebraicGeometry.specPunitIsInitial :

CategoryTheory.Limits.IsInitial (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (CommRingCat.of PUnit.{u_1 + 1} )))

Spec 0 is the initial object in the category of schemes.

Instances For

source

instance AlgebraicGeometry.isAffine_of_isEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty ↑↑X.toPresheafedSpace] :

AlgebraicGeometry.IsAffine X

source

instance AlgebraicGeometry.instHasInitialSchemeInstCategoryScheme :

CategoryTheory.Limits.HasInitial AlgebraicGeometry.Scheme

source

instance AlgebraicGeometry.initial_isEmpty :

IsEmpty ↑↑(⊥_ AlgebraicGeometry.Scheme).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace

source

theorem AlgebraicGeometry.bot_isAffineOpen (X : AlgebraicGeometry.Scheme) :

AlgebraicGeometry.IsAffineOpen ⊥

source

instance AlgebraicGeometry.instHasStrictInitialObjectsSchemeInstCategoryScheme :

CategoryTheory.Limits.HasStrictInitialObjects AlgebraicGeometry.Scheme