Colimits of LocallyRingedSpace #
We construct the explicit coproducts and coequalizers of LocallyRingedSpace.
It then follows that LocallyRingedSpace has all colimits, and
forgetToSheafedSpace preserves them.
Equations
- ⋯ = ⋯
The explicit coproduct for F : discrete ι ⥤ LocallyRingedSpace.
Equations
- AlgebraicGeometry.LocallyRingedSpace.coproduct F = { toSheafedSpace := CategoryTheory.Limits.colimit (F.comp AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace), isLocalRing := ⋯ }
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
- ⋯ = ⋯
Alias of AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom.
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
- One or more equations did not get rendered due to their size.
Instances For
Alias of AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom.
The coequalizer of two locally ringed space in the category of sheafed spaces is a locally ringed space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The explicit coequalizer cofork of locally ringed spaces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- ⋯ = ⋯