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}
[Category.{v, u} C]
{α : Type v}
(h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g))
(f : α → Functor Cᵒᵖ (Type v))
(hf : ∀ (a : α), IsIndObject (f a))
:
IsIndObject (∏ᶜ f)
theorem
CategoryTheory.Limits.isIndObject_limit_of_discrete
{C : Type u}
[Category.{v, u} C]
{α : Type v}
(h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g))
(F : Functor (Discrete α) (Functor Cᵒᵖ (Type v)))
(hF : ∀ (a : Discrete α), IsIndObject (F.obj a))
:
IsIndObject (limit F)
theorem
CategoryTheory.Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape
{C : Type u}
[Category.{v, u} C]
{α : Type v}
[HasLimitsOfShape (Discrete α) C]
(F : Functor (Discrete α) (Functor Cᵒᵖ (Type v)))
(hF : ∀ (a : Discrete α), IsIndObject (F.obj a))
:
IsIndObject (limit F)