The IPC property #
Given a family of categories I i
(i : α
) and a family of functors F i : I i ⥤ C
, we construct
the natural morphism colim_k (∏ᶜ s ↦ (F s).obj (k s)) ⟶ ∏ᶜ s ↦ colim_k (F s).obj (k s)
.
Similarly to the study of finite limits commuting with filtered colimits, we then study sufficient
conditions for this morphism to be an isomorphism. We say that C
satisfies the w
-IPC property if
the morphism is an isomorphism as long as α
is w
-small and I i
is w
-small and filtered for
all i
.
We show that
- the category
Type u
satisfies theu
-IPC property and - if
C
satisfies thew
-IPC property, thenD ⥤ C
satisfies thew
-IPC property.
These results will be used to show that if a category C
has products indexed by α
, then so
does the category of Ind-objects of C
.
References #
- [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], 3.1.10, 3.1.11, 3.1.12.
Given a family of functors I i ⥤ C
for i : α
, we obtain a functor (∀ i, I i) ⥤ C
which
maps k : ∀ i, I i
to ∏ᶜ fun (s : α) => (F s).obj (k s)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusions (F s).obj (k s) ⟶ colimit (F s)
induce a cocone on pointwiseProduct F
with
cone point ∏ᶜ (fun s : α) => colimit (F s)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural morphism colim_k (∏ᶜ s ↦ (F s).obj (k s)) ⟶ ∏ᶜ s ↦ colim_k (F s).obj (k s)
.
We will say that a category has the IPC
property if this morphism is an isomorphism as long
as the indexing categories are filtered.
Equations
Instances For
Evaluating the pointwise product k ↦ ∏ᶜ fun (s : α) => (F s).obj (k s)
at d
is the same as
taking the pointwise product k ↦ ∏ᶜ fun (s : α) => ((F s).obj (k s)).obj d
.
Equations
- CategoryTheory.Limits.pointwiseProductCompEvaluation F d = CategoryTheory.NatIso.ofComponents (fun (k : (i : α) → I i) => CategoryTheory.Limits.piObjIso (fun (s : α) => (F s).obj (k s)) d) ⋯
Instances For
A category C
has the w
-IPC property if the natural morphism
colim_k (∏ᶜ s ↦ (F s).obj (k s)) ⟶ ∏ᶜ s ↦ colim_k (F s).obj (k s)
is an isomorphism for any
family of functors F i : I i ⥤ C
with I i
w
-small and filtered for all i
.
- isIso (α : Type w) (I : α → Type w) [(i : α) → SmallCategory (I i)] [∀ (i : α), IsFiltered (I i)] (F : (i : α) → Functor (I i) C) : IsIso (colimitPointwiseProductToProductColimit F)
colimitPointwiseProductToProductColimit F
is always an isomorphism.