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.

source

theorem AlgebraicGeometry.SheafedSpace.isColimit_exists_rep {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {J : Type v} [CategoryTheory.Category.{v, v} J] (F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C)) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (x : ↑↑c.pt.toPresheafedSpace) :

∃ (i : J) (y : ↑↑(F.obj i).toPresheafedSpace), (c.ι.app i).base y = x

source

theorem AlgebraicGeometry.SheafedSpace.colimit_exists_rep {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {J : Type v} [CategoryTheory.Category.{v, v} J] (F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C)) (x : ↑↑(CategoryTheory.Limits.colimit F).toPresheafedSpace) :

∃ (i : J) (y : ↑↑(F.obj i).toPresheafedSpace), (CategoryTheory.Limits.colimit.ι F i).base y = x

source

instance AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {X : AlgebraicGeometry.SheafedSpace C} {Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) (g : X ⟶ Y) :

CategoryTheory.Epi (CategoryTheory.Limits.coequalizer.π f g).base

Equations

⋯ = ⋯

source

noncomputable def AlgebraicGeometry.LocallyRingedSpace.coproduct {ι : Type u} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace) :

AlgebraicGeometry.LocallyRingedSpace

The explicit coproduct for F : discrete ι ⥤ LocallyRingedSpace.

Equations

AlgebraicGeometry.LocallyRingedSpace.coproduct F = { toSheafedSpace := CategoryTheory.Limits.colimit (F.comp AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace), localRing := ⋯ }

Instances For

source

noncomputable def AlgebraicGeometry.LocallyRingedSpace.coproductCofan {ι : Type u} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace) :

CategoryTheory.Limits.Cocone F

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def AlgebraicGeometry.LocallyRingedSpace.coproductCofanIsColimit {ι : Type u} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace) :

CategoryTheory.Limits.IsColimit (AlgebraicGeometry.LocallyRingedSpace.coproductCofan F)

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

source

instance AlgebraicGeometry.LocallyRingedSpace.instHasCoproducts :

CategoryTheory.Limits.HasCoproducts AlgebraicGeometry.LocallyRingedSpace

Equations

⋯ = ⋯

source

noncomputable instance AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace (J : Type u) :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

Equations

One or more equations did not get rendered due to their size.

source

instance AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalRingHom {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace) :

IsLocalRingHom ((CategoryTheory.Limits.coequalizer.π f.val g.val).c.app (Opposite.op U))

Equations

⋯ = ⋯

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.

source