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

      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