# Colimits of LocallyRingedSpace #

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

theorem AlgebraicGeometry.SheafedSpace.isColimit_exists_rep {C : Type u} {J : Type v} {c : } (hc : ) (x : c.pt.toPresheafedSpace) :
∃ (i : J) (y : (F.obj i).toPresheafedSpace), (c.app i).base y = x
theorem AlgebraicGeometry.SheafedSpace.colimit_exists_rep {C : Type u} {J : Type v} (x : .toPresheafedSpace) :
∃ (i : J) (y : (F.obj i).toPresheafedSpace), .base y = x
instance AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseπ {C : Type u} (f : X Y) (g : X Y) :
Equations
• =

The explicit coproduct for F : discrete ι ⥤ LocallyRingedSpace.

Equations
• = { toSheafedSpace := , localRing := }
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.

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.

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).presheaf.obj (Opposite.op U))) :

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

Equations
• One or more equations did not get rendered due to their size.
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).presheaf.obj (Opposite.op U))) :
(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).presheaf.obj (Opposite.op U))) :
IsOpen ((CategoryTheory.Limits.coequalizer.π f.val g.val).base '' .carrier)
Equations
• =

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

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

The explicit coequalizer cofork of locally ringed spaces.

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.