# mathlibdocumentation

algebraic_geometry.locally_ringed_space.has_colimits

# 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.

theorem algebraic_geometry.SheafedSpace.is_colimit_exists_rep {C : Type u} {J : Type v} (F : J ) (x : (c.X)) :
∃ (i : J) (y : (F.obj i)), ((c.ι.app i).base) y = x
theorem algebraic_geometry.SheafedSpace.colimit_exists_rep {C : Type u} {J : Type v} (F : J ) (x : ) :
∃ (i : J) (y : (F.obj i)), y = x
@[protected, instance]

The explicit coproduct for F : discrete ι ⥤ LocallyRingedSpace.

Equations
noncomputable def algebraic_geometry.LocallyRingedSpace.coproduct_cofan {ι : Type u}  :

The explicit coproduct cofan for F : discrete ι ⥤ LocallyRingedSpace.

Equations

The explicit coproduct cofan constructed in coproduct_cofan is indeed a colimit.

Equations
@[protected, instance]

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.

(Implementation). The basic open set of the section π꙳ s.

Equations
@[protected, instance]

The coequalizer of two locally ringed space in the category of sheafed spaces is a locally ringed space.

Equations

The explicit coequalizer cofork of locally ringed spaces.

Equations

The cofork constructed in coequalizer_cofork is indeed a colimit cocone.

Equations
@[protected, instance]