Colimits of LocallyRingedSpace #
We construct the explicit coproducts and coequalizers of LocallyRingedSpace.
It then follows that LocallyRingedSpace has all colimits, and
forget_to_SheafedSpace preserves them.
The explicit coproduct for F : discrete ι ⥤ LocallyRingedSpace.
Instances For
The explicit coproduct cofan for F : discrete ι ⥤ LocallyRingedSpace.
Instances For
The explicit coproduct cofan constructed in coproduct_cofan is indeed a colimit.
Instances For
We roughly follow the construction given in [MR0302656]. Given a pair f, g : X ⟶ Y of morphisms
of locally ringed spaces, we want to show that the stalk map of
π = coequalizer.π f g (as sheafed space homs) is a local ring hom. It then follows that
coequalizer f g is indeed a locally ringed space, and coequalizer.π f g is a morphism of
locally ringed space.
Given a germ ⟨U, s⟩ of x : coequalizer f g such that π꙳ x : Y is invertible, we ought to show
that ⟨U, s⟩ is invertible. That is, there exists an open set U' ⊆ U containing x such that the
restriction of s onto U' is invertible. This U' is given by π '' V, where V is the
basic open set of π⋆x.
Since f ⁻¹' V = Y.basic_open (f ≫ π)꙳ x = Y.basic_open (g ≫ π)꙳ x = g ⁻¹' V, we have
π ⁻¹' (π '' V) = V (as the underlying set map is merely the set-theoretic coequalizer).
This shows that π '' V is indeed open, and s is invertible on π '' V as the components of π꙳
are local ring homs.
(Implementation). The basic open set of the section π꙳ s.
Instances For
The coequalizer of two locally ringed space in the category of sheafed spaces is a locally ringed space.
Instances For
The explicit coequalizer cofork of locally ringed spaces.
Instances For
The cofork constructed in coequalizer_cofork is indeed a colimit cocone.