PresheafedSpace C has colimits. #
If C has limits, then the category PresheafedSpace C has colimits,
and the forgetful functor to TopCat 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
AlgebraicGeometry.PresheafedSpace.map_id_c_app
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(j : J)
(U : TopologicalSpace.Opens ↑↑(F.toPrefunctor.obj j))
:
(F.toPrefunctor.map (CategoryTheory.CategoryStruct.id j)).c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp
((TopCat.Presheaf.Pushforward.id (F.toPrefunctor.obj j).presheaf).inv.app (Opposite.op U))
((TopCat.Presheaf.pushforwardEq
(_ :
CategoryTheory.CategoryStruct.id ↑(F.toPrefunctor.obj j) = (F.toPrefunctor.map (CategoryTheory.CategoryStruct.id j)).base)
(F.toPrefunctor.obj j).presheaf).hom.app
(Opposite.op U))
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.map_comp_c_app
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
{j₁ : J}
{j₂ : J}
{j₃ : J}
(f : j₁ ⟶ j₂)
(g : j₂ ⟶ j₃)
(U : TopologicalSpace.Opens ↑↑(F.toPrefunctor.obj j₃))
:
(F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g)).c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).c.app (Opposite.op U))
(CategoryTheory.CategoryStruct.comp
((TopCat.Presheaf.pushforwardMap (F.toPrefunctor.map g).base (F.toPrefunctor.map f).c).app (Opposite.op U))
(CategoryTheory.CategoryStruct.comp
((TopCat.Presheaf.Pushforward.comp (F.toPrefunctor.obj j₁).presheaf (F.toPrefunctor.map f).base
(F.toPrefunctor.map g).base).inv.app
(Opposite.op U))
((TopCat.Presheaf.pushforwardEq
(_ :
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f).base (F.toPrefunctor.map g).base = (F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g)).base)
(F.toPrefunctor.obj j₁).presheaf).hom.app
(Opposite.op U))))
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
[CategoryTheory.Limits.HasColimit F]
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
(j : Jᵒᵖ)
:
(AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).toPrefunctor.obj j = (F.toPrefunctor.obj j.unop).presheaf.toPrefunctor.obj
(Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j.unop).base).toPrefunctor.obj U))
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
[CategoryTheory.Limits.HasColimit F]
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
{j : Jᵒᵖ}
{k : Jᵒᵖ}
(f : j ⟶ k)
:
(AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp
((F.toPrefunctor.map f.unop).c.app
(Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j.unop).base).toPrefunctor.obj U)))
((F.toPrefunctor.obj k.unop).presheaf.toPrefunctor.map
(CategoryTheory.eqToHom
(_ :
(TopologicalSpace.Opens.map (F.toPrefunctor.map f.unop).base).op.toPrefunctor.obj
(Opposite.op
((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j.unop).base).toPrefunctor.obj U)) = Opposite.op
((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F k.unop).base).toPrefunctor.obj U))))
def
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
[CategoryTheory.Limits.HasColimit F]
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(j : J)
:
(AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).toPrefunctor.obj j = Opposite.op
(CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)) j _* (F.toPrefunctor.obj j).presheaf)
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
{j : J}
{j' : J}
(f : j ⟶ j')
:
(AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).toPrefunctor.map f = (CategoryTheory.CategoryStruct.comp
(TopCat.Presheaf.pushforwardMap
(CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C))
j')
(F.toPrefunctor.map f).c)
(CategoryTheory.CategoryStruct.comp
(TopCat.Presheaf.Pushforward.comp (F.toPrefunctor.obj j).presheaf
((CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)).toPrefunctor.map f)
(CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)) j')).inv
(TopCat.Presheaf.pushforwardEq
(_ :
CategoryTheory.CategoryStruct.comp
((CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)).toPrefunctor.map f)
(CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)) j') = CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C)) j)
(F.toPrefunctor.obj j).presheaf).hom)).op
def
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
(F : CategoryTheory.Functor J (AlgebraicGeometry.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
- One or more equations did not get rendered due to their size.
Instances For
def
AlgebraicGeometry.PresheafedSpace.colimit
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
Auxiliary definition for AlgebraicGeometry.PresheafedSpace.instHasColimits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimit_carrier
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimit_presheaf
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(j : J)
:
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_base
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(j : J)
:
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimitCocone_pt
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
def
AlgebraicGeometry.PresheafedSpace.colimitCocone
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
Auxiliary definition for AlgebraicGeometry.PresheafedSpace.instHasColimits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(s : CategoryTheory.Limits.Cocone F)
(U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ)
:
s.pt.presheaf.toPrefunctor.obj U ⟶ (CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C))
((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s) _* CategoryTheory.Limits.limit
(AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp).toPrefunctor.obj
U
Auxiliary definition for AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(s : CategoryTheory.Limits.Cocone F)
{U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ}
{V : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ}
(i : U ⟶ V)
:
CategoryTheory.CategoryStruct.comp (s.pt.presheaf.toPrefunctor.map i)
(AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s V) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U)
((CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp F (AlgebraicGeometry.PresheafedSpace.forget C))
((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s) _* (AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt.presheaf).toPrefunctor.map
i)
def
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(s : CategoryTheory.Limits.Cocone F)
:
Auxiliary definition for AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_fac
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(s : CategoryTheory.Limits.Cocone F)
(j : J)
:
def
AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
:
Auxiliary definition for AlgebraicGeometry.PresheafedSpace.instHasColimits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShapePresheafedSpaceCategoryOfPresheafedSpaces
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
:
Equations
instance
AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapePresheafedSpaceCategoryOfPresheafedSpacesTopCatInstTopCatLargeCategoryForget
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
:
Equations
- AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapePresheafedSpaceCategoryOfPresheafedSpacesTopCatInstTopCatLargeCategoryForget = CategoryTheory.Limits.PreservesColimitsOfShape.mk
instance
AlgebraicGeometry.PresheafedSpace.instHasColimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
:
When C has limits, the category of presheaved spaces with values in C itself has colimits.
Equations
- One or more equations did not get rendered due to their size.
instance
AlgebraicGeometry.PresheafedSpace.forgetPreservesColimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
:
The underlying topological space of a colimit of presheaved spaces is the colimit of the underlying topological spaces.
Equations
- AlgebraicGeometry.PresheafedSpace.forgetPreservesColimits = CategoryTheory.Limits.PreservesColimitsOfSize.mk
def
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
[CategoryTheory.Limits.HasColimit F]
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
:
(CategoryTheory.Limits.colimit F).presheaf.toPrefunctor.obj (Opposite.op U) ≅ CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U)
The components of the colimit of a diagram of PresheafedSpace C is obtained
via taking componentwise limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
(j : J)
:
@[simp]
theorem
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimitsOfShape J TopCat]
[∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
(F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
(U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F))
(j : J)
: