PresheafedSpace C has colimits. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 u'}
[category_theory.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 u'}
[category_theory.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.componentwise_diagram_obj
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
[category_theory.limits.has_colimit F]
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier))
(j : Jᵒᵖ) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.componentwise_diagram_map
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
[category_theory.limits.has_colimit F]
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier))
(j k : Jᵒᵖ)
(f : j ⟶ k) :
(algebraic_geometry.PresheafedSpace.componentwise_diagram F U).map f = (F.map f.unop).c.app (opposite.op ((topological_space.opens.map (category_theory.limits.colimit.ι F (opposite.unop j)).base).obj U)) ≫ (F.obj (opposite.unop k)).presheaf.map (category_theory.eq_to_hom _)
noncomputable
def
algebraic_geometry.PresheafedSpace.componentwise_diagram
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
[category_theory.limits.has_colimit F]
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier)) :
Given a diagram of PresheafedSpace Cs, its colimit is computed by pushing the sheaves onto
the colimit of the underlying spaces, and taking componentwise limit.
This is the componentwise diagram for an open set U of the colimit of the underlying spaces.
Equations
- algebraic_geometry.PresheafedSpace.componentwise_diagram F U = {obj := λ (j : Jᵒᵖ), (F.obj (opposite.unop j)).presheaf.obj (opposite.op ((topological_space.opens.map (category_theory.limits.colimit.ι F (opposite.unop j)).base).obj U)), map := λ (j k : Jᵒᵖ) (f : j ⟶ k), (F.map f.unop).c.app (opposite.op ((topological_space.opens.map (category_theory.limits.colimit.ι F (opposite.unop j)).base).obj U)) ≫ (F.obj (opposite.unop k)).presheaf.map (category_theory.eq_to_hom _), map_id' := _, map_comp' := _}
@[simp]
theorem
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_obj
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit_map
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
(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
noncomputable
def
algebraic_geometry.PresheafedSpace.pushforward_diagram_to_colimit
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
(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' := _}
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxiliary definition for PresheafedSpace.has_colimits.
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_carrier
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_presheaf
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_X
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit_cocone
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxiliary 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 u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_ι_app_base
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(j : J) :
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(s : category_theory.limits.cocone F)
(U : (topological_space.opens ↥(s.X.carrier))ᵒᵖ) :
Auxiliary 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 u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ 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
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(s : category_theory.limits.cocone F) :
Auxiliary definition for PresheafedSpace.colimit_cocone_is_colimit.
Equations
- algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc F s = {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' := _}}
theorem
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_fac
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(s : category_theory.limits.cocone F)
(j : J) :
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C) :
Auxiliary definition for PresheafedSpace.has_colimits.
Equations
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.category_theory.limits.has_colimits_of_shape
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C] :
@[protected, instance]
noncomputable
def
algebraic_geometry.PresheafedSpace.forget.category_theory.limits.preserves_colimits_of_shape
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C] :
Equations
- algebraic_geometry.PresheafedSpace.forget.category_theory.limits.preserves_colimits_of_shape = {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) _))}
@[protected, 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.
@[protected, instance]
noncomputable
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.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) _))}}
noncomputable
def
algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
[category_theory.limits.has_colimit F]
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier)) :
The components of the colimit of a diagram of PresheafedSpace C is obtained
via taking componentwise limits.
Equations
- algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit F U = (algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso (category_theory.limits.colimit.iso_colimit_cocone {cocone := algebraic_geometry.PresheafedSpace.colimit_cocone F, is_colimit := algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit F}).symm).app (opposite.op U) ≪≫ 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.iso_colimit_cocone {cocone := algebraic_geometry.PresheafedSpace.colimit_cocone F, is_colimit := algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit F}).symm.hom.base).op.obj (opposite.op U)) ≪≫ category_theory.limits.lim.map_iso (category_theory.nat_iso.of_components (λ (X : Jᵒᵖ), category_theory.functor.map_iso (F.obj (opposite.unop X)).presheaf (category_theory.eq_to_iso _)) _)
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier))
(j : J) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit_hom_π
{J : Type u'}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J Top]
[∀ (X : Top), category_theory.limits.has_limits_of_shape Jᵒᵖ (Top.presheaf C X)]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C]
(F : J ⥤ algebraic_geometry.PresheafedSpace C)
(U : topological_space.opens ↥((category_theory.limits.colimit F).carrier))
(j : J) :