# mathlibdocumentation

algebraic_geometry.presheafed_space.has_colimits

# PresheafedSpace C has colimits.

If C has limits, then the category PresheafedSpace C has colimits, and the forgetful functor to Top preserves these colimits.

When restricted to a diagram where the underlying continuous maps are open embeddings, this says that we can glue presheaved spaces.

Given a diagram F : J ⥤ PresheafedSpace C, we first build the colimit of the underlying topological spaces, as colimit (F ⋙ PresheafedSpace.forget C). Call that colimit space X.

Our strategy is to push each of the presheaves F.obj j forward along the continuous map colimit.ι (F ⋙ PresheafedSpace.forget C) j to X. Since pushforward is functorial, we obtain a diagram J ⥤ (presheaf C X)ᵒᵖ of presheaves on a single space X. (Note that the arrows now point the other direction, because this is the way PresheafedSpace C is set up.)

The limit of this diagram then constitutes the colimit presheaf.

@[simp]
theorem algebraic_geometry.PresheafedSpace.map_id_c_app {J : Type v} {C : Type u} (F : J ) (j : J) (U : topological_space.opens ((F.obj j).carrier)) :

@[simp]
theorem algebraic_geometry.PresheafedSpace.map_comp_c_app {J : Type v} {C : Type u} (F : J ) {j₁ j₂ j₃ : J} (f : j₁ j₂) (g : j₂ j₃) (U : topological_space.opens ((F.obj j₃).carrier)) :
(F.map (f g)).c.app (opposite.op U) = (F.map g).c.app (opposite.op U) (F.map f).c).app (opposite.op U) (F.map f).base (F.map g).base).inv.app (opposite.op U) (F.obj j₁).presheaf).hom.app (opposite.op U)

@[simp]
theorem algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_obj {J : Type v} {C : Type u} (F : J ) (j : J) :

@[simp]
theorem algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_map {J : Type v} {C : Type u} (F : J ) (j j' : J) (f : j j') :

Given a diagram of presheafed spaces, we can push all the presheaves forward to the colimit X of the underlying topological spaces, obtaining a diagram in (presheaf C X)ᵒᵖ.

Equations
@[simp]

@[simp]

def algebraic_geometry.PresheafedSpace.colimit {J : Type v} {C : Type u} (F : J ) :

Auxilliary definition for PresheafedSpace.has_colimits.

Equations
@[simp]

def algebraic_geometry.PresheafedSpace.colimit_cocone {J : Type v} {C : Type u} (F : J ) :

Auxilliary definition for PresheafedSpace.has_colimits.

Equations
@[simp]

@[simp]
theorem algebraic_geometry.PresheafedSpace.colimit_cocone_ι_app_base {J : Type v} {C : Type u} (F : J ) (j : J) :

Auxilliary definition for PresheafedSpace.colimit_cocone_is_colimit.

Equations

Auxilliary definition for PresheafedSpace.has_colimits.

Equations
@[instance]

When C has limits, the category of presheaved spaces with values in C itself has colimits.

@[instance]

The underlying topological space of a colimit of presheaved spaces is the colimit of the underlying topological spaces.

Equations