(Co)Limits of Schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

The existence of fibred products was shown in algebraic_geometry/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 algebraic_geometry.Spec_Z_is_terminal :

category_theory.limits.is_terminal (algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of ℤ)))

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

Equations

algebraic_geometry.Spec_Z_is_terminal = category_theory.limits.is_terminal.is_terminal_obj algebraic_geometry.Scheme.Spec (opposite.op (CommRing.of ℤ)) (category_theory.limits.terminal_op_of_initial CommRing.Z_is_initial)

source

@[protected, instance]

def algebraic_geometry.Scheme.category_theory.limits.has_terminal :

category_theory.limits.has_terminal algebraic_geometry.Scheme

source

@[protected, instance]

def algebraic_geometry.category_theory.limits.terminal.is_affine :

algebraic_geometry.is_affine (⊤_ algebraic_geometry.Scheme)

source

@[protected, instance]

def algebraic_geometry.Scheme.category_theory.limits.has_finite_limits :

category_theory.limits.has_finite_limits algebraic_geometry.Scheme

source

@[simp]

theorem algebraic_geometry.Scheme.empty_to_val_base_apply (X : algebraic_geometry.Scheme) (x : ↥↑(∅.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)) :

⇑(X.empty_to.val.base) x = pempty.elim x

source

def algebraic_geometry.Scheme.empty_to (X : algebraic_geometry.Scheme) :

∅ ⟶ X

The map from the empty scheme.

Equations

X.empty_to = {val := {base := {to_fun := λ (x : ↥↑(∅.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), pempty.elim x, continuous_to_fun := _}, c := {app := λ (U : (topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ), CommRing.punit_is_terminal.from (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj U), naturality' := _}}, prop := _}

source

@[ext]

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

f = g

source

theorem algebraic_geometry.Scheme.eq_empty_to {X : algebraic_geometry.Scheme} (f : ∅ ⟶ X) :

f = X.empty_to

source

@[protected, instance]

def algebraic_geometry.quiver.hom.unique (X : algebraic_geometry.Scheme) :

unique (∅ ⟶ X)

Equations

algebraic_geometry.quiver.hom.unique X = {to_inhabited := {default := X.empty_to}, uniq := _}

source

def algebraic_geometry.empty_is_initial :

category_theory.limits.is_initial ∅

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

Equations

algebraic_geometry.empty_is_initial = category_theory.limits.is_initial.of_unique ∅

source

@[simp]

theorem algebraic_geometry.empty_is_initial_to :

algebraic_geometry.empty_is_initial.to = algebraic_geometry.Scheme.empty_to

source

@[protected, instance]

def algebraic_geometry.carrier.is_empty :

is_empty ↥(algebraic_geometry.Scheme.empty.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

source

@[protected, instance]

def algebraic_geometry.Spec_punit_is_empty :

is_empty ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of punit))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

source

@[protected, instance]

def algebraic_geometry.is_open_immersion_of_is_empty {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [is_empty ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

algebraic_geometry.is_open_immersion f

source

@[protected, instance]

def algebraic_geometry.is_iso_of_is_empty {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [is_empty ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

category_theory.is_iso f

source

noncomputable def algebraic_geometry.is_initial_of_is_empty {X : algebraic_geometry.Scheme} [is_empty ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

category_theory.limits.is_initial X

A scheme is initial if its underlying space is empty .

Equations

algebraic_geometry.is_initial_of_is_empty = algebraic_geometry.empty_is_initial.of_iso (category_theory.as_iso (algebraic_geometry.empty_is_initial.to X))

source

noncomputable def algebraic_geometry.Spec_punit_is_initial :

category_theory.limits.is_initial (algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of punit)))

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

Equations

algebraic_geometry.Spec_punit_is_initial = algebraic_geometry.empty_is_initial.of_iso (category_theory.as_iso (algebraic_geometry.empty_is_initial.to (algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of punit)))))

source

@[protected, instance]

def algebraic_geometry.is_affine_of_is_empty {X : algebraic_geometry.Scheme} [is_empty ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

algebraic_geometry.is_affine X

source

@[protected, instance]

def algebraic_geometry.Scheme.category_theory.limits.has_initial :

category_theory.limits.has_initial algebraic_geometry.Scheme

source

@[protected, instance]

def algebraic_geometry.initial_is_empty :

is_empty ↥((⊥_ algebraic_geometry.Scheme).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

source

theorem algebraic_geometry.bot_is_affine_open (X : algebraic_geometry.Scheme) :

algebraic_geometry.is_affine_open ⊥

source

@[protected, instance]

def algebraic_geometry.Scheme.category_theory.limits.has_strict_initial_objects :

category_theory.limits.has_strict_initial_objects algebraic_geometry.Scheme