# Documentation

Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits

# 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 AlgebraicGeometry.SheafedSpace.isColimit_exists_rep {C : Type u} {J : Type v} {c : } (hc : ) (x : c.pt.toPresheafedSpace) :
i y, (c.app i).base y = x
theorem AlgebraicGeometry.SheafedSpace.colimit_exists_rep {C : Type u} {J : Type v} (x : ().toPresheafedSpace) :
i y, ().base y = x

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.

noncomputable def AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen (f : X Y) (g : X Y) (U : TopologicalSpace.Opens (CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace) (s : ↑((CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace.presheaf.obj ())) :

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

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage (f : X Y) (g : X Y) (U : TopologicalSpace.Opens (CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace) (s : ↑((CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace.presheaf.obj ())) :
(CategoryTheory.Limits.coequalizer.π f.val g.val).base ⁻¹' ((CategoryTheory.Limits.coequalizer.π f.val g.val).base '' ().carrier) = ().carrier
theorem AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open (f : X Y) (g : X Y) (U : TopologicalSpace.Opens (CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace) (s : ↑((CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace.presheaf.obj ())) :
IsOpen ((CategoryTheory.Limits.coequalizer.π f.val g.val).base '' ().carrier)

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

Instances For
noncomputable def AlgebraicGeometry.LocallyRingedSpace.coequalizerCofork (f : X Y) (g : X Y) :

The explicit coequalizer cofork of locally ringed spaces.

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.isLocalRingHom_stalkMap_congr (f : X Y) (g : X Y) (H : f = g) (x : X.toPresheafedSpace) :

The cofork constructed in coequalizer_cofork is indeed a colimit cocone.

Instances For