(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
Spec ℤ is the terminal object.
- The preceding two results imply that
Scheme has all finite limits.
- The empty scheme is the (strict) initial object.
- Coproducts exists (and the forgetful functors preserve them).
Spec ℤ is the terminal object in the category of schemes.
The map from the empty scheme.
The empty scheme is the initial object in the category of schemes.
A scheme is initial if its underlying space is empty .
Spec 0 is the initial object in the category of schemes.