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}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J)
(U : topological_space.opens ↥((F.obj j).carrier)) :
(F.map (𝟙 j)).c.app (opposite.op U) = (Top.presheaf.pushforward.id (F.obj j).presheaf).inv.app (opposite.op U) ≫ (Top.presheaf.pushforward_eq _ (F.obj j).presheaf).hom.app (opposite.op U)
@[simp]
theorem
algebraic_geometry.PresheafedSpace.map_comp_c_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
{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) ≫ (Top.presheaf.pushforward_map (F.map g).base (F.map f).c).app (opposite.op U) ≫ (Top.presheaf.pushforward.comp (F.obj j₁).presheaf (F.map f).base (F.map g).base).inv.app (opposite.op U) ≫ (Top.presheaf.pushforward_eq _ (F.obj j₁).presheaf).hom.app (opposite.op U)
@[simp]
theorem
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_obj
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j j' : J)
(f : j ⟶ j') :
(algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit F).map f = (Top.presheaf.pushforward_map (category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j') (F.map f).c ≫ (Top.presheaf.pushforward.comp (F.obj j).presheaf ((F ⋙ algebraic_geometry.PresheafedSpace.forget C).map f) (category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j')).inv ≫ (Top.presheaf.pushforward_eq _ (F.obj j).presheaf).hom).op
def
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
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
- algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit F = {obj := λ (j : J), opposite.op (category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j _* (F.obj j).presheaf), map := λ (j j' : J) (f : j ⟶ j'), (Top.presheaf.pushforward_map (category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j') (F.map f).c ≫ (Top.presheaf.pushforward.comp (F.obj j).presheaf ((F ⋙ algebraic_geometry.PresheafedSpace.forget C).map f) (category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j')).inv ≫ (Top.presheaf.pushforward_eq _ (F.obj j).presheaf).hom).op, map_id' := _, map_comp' := _}
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_presheaf
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_carrier
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
def
algebraic_geometry.PresheafedSpace.colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxilliary definition for PresheafedSpace.has_colimits.
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
def
algebraic_geometry.PresheafedSpace.colimit_cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxilliary definition for PresheafedSpace.has_colimits.
Equations
- algebraic_geometry.PresheafedSpace.colimit_cocone F = {X := algebraic_geometry.PresheafedSpace.colimit F, ι := {app := λ (j : J), {base := category_theory.limits.colimit.ι (F ⋙ algebraic_geometry.PresheafedSpace.forget C) j, c := category_theory.limits.limit.π (algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit F).left_op (opposite.op j)}, naturality' := _}}
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_ι_app_c
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_ι_app_base
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
def
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(s : category_theory.limits.cocone F)
(U : (topological_space.opens ↥(s.X.carrier))ᵒᵖ) :
Auxilliary definition for PresheafedSpace.colimit_cocone_is_colimit.
Equations
- algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app F s U = category_theory.limits.limit.lift ((algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit F).left_op ⋙ (category_theory.evaluation (topological_space.opens ↥(category_theory.limits.colimit (F ⋙ algebraic_geometry.PresheafedSpace.forget C)))ᵒᵖ C).obj ((topological_space.opens.map (category_theory.limits.colimit.desc (F ⋙ algebraic_geometry.PresheafedSpace.forget C) ((algebraic_geometry.PresheafedSpace.forget C).map_cocone s))).op.obj U)) {X := s.X.presheaf.obj U, π := {app := λ (j : Jᵒᵖ), (s.ι.app (opposite.unop j)).c.app U ≫ (F.obj (opposite.unop j)).presheaf.map (category_theory.eq_to_hom _), naturality' := _}} ≫ (category_theory.limits.limit_obj_iso_limit_comp_evaluation (algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit F).left_op ((topological_space.opens.map (category_theory.limits.colimit.desc (F ⋙ algebraic_geometry.PresheafedSpace.forget C) ((algebraic_geometry.PresheafedSpace.forget C).map_cocone s))).op.obj U)).inv
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_naturality
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(s : category_theory.limits.cocone F)
{U V : (topological_space.opens ↥(s.X.carrier))ᵒᵖ}
(i : U ⟶ V) :
s.X.presheaf.map i ≫ algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app F s V = algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app F s U ≫ (category_theory.limits.colimit.desc (F ⋙ algebraic_geometry.PresheafedSpace.forget C) ((algebraic_geometry.PresheafedSpace.forget C).map_cocone s) _* (algebraic_geometry.PresheafedSpace.colimit_cocone F).X.presheaf).map i
def
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxilliary definition for PresheafedSpace.has_colimits.
Equations
- algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit F = {desc := λ (s : category_theory.limits.cocone F), {base := category_theory.limits.colimit.desc (F ⋙ algebraic_geometry.PresheafedSpace.forget C) ((algebraic_geometry.PresheafedSpace.forget C).map_cocone s), c := {app := λ (U : (topological_space.opens ↥(s.X.carrier))ᵒᵖ), algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app F s U, naturality' := _}}, fac' := _, uniq' := _}
@[instance]
def
algebraic_geometry.PresheafedSpace.category_theory.limits.has_colimits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C] :
When C has limits, the category of presheaved spaces with values in C itself has colimits.
@[instance]
def
algebraic_geometry.PresheafedSpace.forget_preserves_colimits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C] :
The underlying topological space of a colimit of presheaved spaces is the colimit of the underlying topological spaces.
Equations
- algebraic_geometry.PresheafedSpace.forget_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_colimit := λ (F : J ⥤ algebraic_geometry.PresheafedSpace C), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit F) ((category_theory.limits.colimit.is_colimit (F ⋙ algebraic_geometry.PresheafedSpace.forget C)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl (category_theory.limits.colimit.cocone (F ⋙ algebraic_geometry.PresheafedSpace.forget C)).X) _))}}