(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.
- The disjoint union is the coproduct of a family of schemes, and the forgetful functor to
LocallyRingedSpace
andTopCat
preserves them.
TODO #
- Spec preserves finite coproducts.
Spec ℤ
is the terminal object in the category of schemes.
Equations
- One or more equations did not get rendered due to their size.
Spec ℤ
is the terminal object in the category of schemes.
Equations
- One or more equations did not get rendered due to their size.
Equations
The map from the empty scheme.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
(Implementation Detail) The glue data associated to a disjoint union.
Equations
- One or more equations did not get rendered due to their size.
(Implementation Detail) The glue data associated to a disjoint union.
Equations
- AlgebraicGeometry.disjointGlueData f = { toGlueData := CategoryTheory.GlueData.ofGlueData' (AlgebraicGeometry.disjointGlueData' f), f_open := ⋯ }
(Implementation Detail) The cofan in LocallyRingedSpace
associated to a disjoint union.
Equations
- One or more equations did not get rendered due to their size.
(Implementation Detail)
The cofan in LocallyRingedSpace
associated to a disjoint union is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
(Implementation Detail) Coproduct of schemes is isomorphic to the disjoint union.
Equations
- One or more equations did not get rendered due to their size.
The images of each component in the coproduct is disjoint.
The open cover of the coproduct.
Equations
- AlgebraicGeometry.sigmaOpenCover g = { J := σ, obj := g, map := CategoryTheory.Limits.Sigma.ι g, f := fun (x : ↥(∐ g)) => ⋯.choose, covers := ⋯, map_prop := ⋯ }
S
is the disjoint union of Xᵢ
if the Xᵢ
are covering, pairwise disjoint open subschemes
of S
.
(Implementation Detail)
The coproduct of the two schemes is given by indexed coproducts over WalkingPair
.
Equations
- One or more equations did not get rendered due to their size.
The open cover of the coproduct of two schemes.
Equations
- One or more equations did not get rendered due to their size.
If X
and Y
are open disjoint and covering open subschemes of S
,
S
is the disjoint union of X
and Y
.
The map Spec R ⨿ Spec S ⟶ Spec (R × S)
.
This is an isomorphism as witnessed by an IsIso
instance provided below.
Equations
- One or more equations did not get rendered due to their size.
The canonical map ∐ Spec Rᵢ ⟶ Spec (Π Rᵢ)
.
This is an isomorphism when the product is finite.
Equations
- AlgebraicGeometry.sigmaSpec R = CategoryTheory.Limits.Sigma.desc fun (i : ι) => AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i))