Colimits of LocallyRingedSpace #

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

We construct the explicit coproducts and coequalizers of LocallyRingedSpace. It then follows that LocallyRingedSpace has all colimits, and forget_to_SheafedSpace preserves them.

We roughly follow the construction given in [DG70]. 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.