Ind-objects are closed under filtered colimits #
We show that if F : I ⥤ Cᵒᵖ ⥤ Type v is a functor such that I is small and filtered and
F.obj i is an ind-object for all i, then colimit F is also an ind-object.
Our proof is a slight variant of the proof given in Kashiwara-Schapira.
References #
- M. Kashiwara, P. Schapira, Categories and Sheaves, Theorem 6.1.8
We start by stating the key interchange property exists_nonempty_limit_obj_of_isColimit. It
consists of pulling out a colimit out of a hom functor and interchanging a filtered colimit with
a finite limit.
noncomputable def
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.compYonedaColimitIsoColimitCompYoneda
{C : Type u}
[Category.{v, u} C]
{I : Type v}
[SmallCategory I]
(F : Functor I (Functor Cᵒᵖ (Type v)))
{J : Type v}
[SmallCategory J]
(G : Functor J (CostructuredArrow yoneda (colimit F)))
{K : Type v}
[SmallCategory K]
(H : Functor K (Over (colimit F)))
:
(implementation) Pulling out a colimit out of a hom functor is one half of the key lemma. Note
that all of the heavy lifting actually happens in CostructuredArrow.toOverCompYonedaColimit
and yonedaYonedaColimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit
{C : Type u}
[Category.{v, u} C]
{I : Type v}
[SmallCategory I]
(F : Functor I (Functor Cᵒᵖ (Type v)))
{J : Type v}
[SmallCategory J]
[FinCategory J]
(G : Functor J (CostructuredArrow yoneda (colimit F)))
{K : Type v}
[SmallCategory K]
(H : Functor K (Over (colimit F)))
[IsFiltered K]
(h : Nonempty (limit ((G.op.comp (CostructuredArrow.toOver yoneda (colimit F)).op).comp (yoneda.obj (colimit H)))))
:
theorem
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit
{C : Type u}
[Category.{v, u} C]
{I : Type v}
[SmallCategory I]
(F : Functor I (Functor Cᵒᵖ (Type v)))
{J : Type v}
[SmallCategory J]
[FinCategory J]
(G : Functor J (CostructuredArrow yoneda (colimit F)))
{K : Type v}
[SmallCategory K]
(H : Functor K (Over (colimit F)))
[IsFiltered K]
{c : Cocone H}
(hc : IsColimit c)
(T : Over (colimit F))
(hT : c.pt ≅ T)
(h : Nonempty (limit ((G.op.comp (CostructuredArrow.toOver yoneda (colimit F)).op).comp (yoneda.obj T))))
:
theorem
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.isFiltered
{C : Type u}
[Category.{v, u} C]
{I : Type v}
[SmallCategory I]
(F : Functor I (Functor Cᵒᵖ (Type v)))
[IsFiltered I]
(hF : ∀ (i : I), IsIndObject (F.obj i))
:
theorem
CategoryTheory.Limits.isIndObject_colimit
{C : Type u}
[Category.{v, u} C]
(I : Type v)
[SmallCategory I]
[IsFiltered I]
(F : Functor I (Functor Cᵒᵖ (Type v)))
(hF : ∀ (i : I), IsIndObject (F.obj i))
:
IsIndObject (colimit F)