Ind-objects are closed under products #
We show that if C admits products indexed by α, then IsIndObject is closed under taking
products in Cᵒᵖ ⥤ Type v indexed by α. This will imply that the functor Ind C ⥤ Cᵒᵖ ⥤ Type v
creates products indexed by α and that the functor C ⥤ Ind C preserves them.
References #
- [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Prop. 6.1.16(ii)
theorem
CategoryTheory.Limits.isIndObject_pi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type v}
(h : ∀ (g : α → C), CategoryTheory.Limits.IsIndObject (∏ᶜ CategoryTheory.yoneda.obj ∘ g))
(f : α → CategoryTheory.Functor Cᵒᵖ (Type v))
(hf : ∀ (a : α), CategoryTheory.Limits.IsIndObject (f a))
:
theorem
CategoryTheory.Limits.isIndObject_limit_of_discrete
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type v}
(h : ∀ (g : α → C), CategoryTheory.Limits.IsIndObject (∏ᶜ CategoryTheory.yoneda.obj ∘ g))
(F : CategoryTheory.Functor (CategoryTheory.Discrete α) (CategoryTheory.Functor Cᵒᵖ (Type v)))
(hF : ∀ (a : CategoryTheory.Discrete α), CategoryTheory.Limits.IsIndObject (F.obj a))
:
theorem
CategoryTheory.Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type v}
[CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
(F : CategoryTheory.Functor (CategoryTheory.Discrete α) (CategoryTheory.Functor Cᵒᵖ (Type v)))
(hF : ∀ (a : CategoryTheory.Discrete α), CategoryTheory.Limits.IsIndObject (F.obj a))
: