(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).

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.

Equations

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

noncomputable instance AlgebraicGeometry.instHasTerminalSchemeInstCategoryScheme : CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasTerminalSchemeInstCategoryScheme = ⋯

noncomputable instance AlgebraicGeometry.instIsAffineTerminalSchemeInstCategorySchemeInstHasTerminalSchemeInstCategoryScheme : AlgebraicGeometry.IsAffine (⊤_ AlgebraicGeometry.Scheme)

Equations

• AlgebraicGeometry.instIsAffineTerminalSchemeInstCategorySchemeInstHasTerminalSchemeInstCategoryScheme = ⋯

noncomputable instance AlgebraicGeometry.instHasFiniteLimitsSchemeInstCategoryScheme : CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasFiniteLimitsSchemeInstCategoryScheme = ⋯

noncomputable def AlgebraicGeometry.Scheme.emptyTo (X : AlgebraicGeometry.Scheme) : ∅ ⟶ X

The map from the empty scheme.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : ↑↑∅.toPresheafedSpace) : (AlgebraicGeometry.Scheme.emptyTo X).val.base x = PEmpty.elim x

@[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)

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

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

noncomputable instance AlgebraicGeometry.Scheme.hom_unique_of_empty_source (X : AlgebraicGeometry.Scheme) : Unique (∅ ⟶ X)

Equations

• AlgebraicGeometry.Scheme.hom_unique_of_empty_source X = { toInhabited := { default := AlgebraicGeometry.Scheme.emptyTo X }, uniq := ⋯ }

noncomputable def AlgebraicGeometry.emptyIsInitial : CategoryTheory.Limits.IsInitial ∅

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

Equations

• AlgebraicGeometry.emptyIsInitial = CategoryTheory.Limits.IsInitial.ofUnique ∅

@[simp]

theorem AlgebraicGeometry.emptyIsInitial_to : CategoryTheory.Limits.IsInitial.to AlgebraicGeometry.emptyIsInitial = AlgebraicGeometry.Scheme.emptyTo

noncomputable instance AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceEmpty : IsEmpty ↑↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace

Equations

• AlgebraicGeometry.instIsEmptyαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceEmpty = ⋯

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

Equations

• AlgebraicGeometry.spec_punit_isEmpty = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

A scheme is initial if its underlying space is empty .

Equations

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

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.

Equations

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

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

Equations

• ⋯ = ⋯

noncomputable instance AlgebraicGeometry.instHasInitialSchemeInstCategoryScheme : CategoryTheory.Limits.HasInitial AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasInitialSchemeInstCategoryScheme = ⋯

noncomputable instance AlgebraicGeometry.initial_isEmpty : IsEmpty ↑↑(⊥_ AlgebraicGeometry.Scheme).toPresheafedSpace

Equations

• AlgebraicGeometry.initial_isEmpty = ⋯

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

noncomputable instance AlgebraicGeometry.instHasStrictInitialObjectsSchemeInstCategoryScheme : CategoryTheory.Limits.HasStrictInitialObjects AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.instHasStrictInitialObjectsSchemeInstCategoryScheme = ⋯