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 the u-IPC property and
• if C satisfies the w-IPC property, then D ⥤ C satisfies the w-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, 3.1.10, 3.1.11, 3.1.12.

noncomputable def CategoryTheory.Limits.pointwiseProduct {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) : Functor ((i : α) → I i) C

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.

@[simp]

theorem CategoryTheory.Limits.pointwiseProduct_obj {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) (k : (i : α) → I i) : (pointwiseProduct F).obj k = ∏ᶜ fun (s : α) => (F s).obj (k s)

@[simp]

theorem CategoryTheory.Limits.pointwiseProduct_map {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) {X✝ Y✝ : (i : α) → I i} (f : X✝ ⟶ Y✝) : (pointwiseProduct F).map f = Pi.map fun (s : α) => (F s).map (f s)

noncomputable def CategoryTheory.Limits.coconePointwiseProduct {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] : Cocone (pointwiseProduct F)

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.

@[simp]

theorem CategoryTheory.Limits.coconePointwiseProduct_pt {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] : (coconePointwiseProduct F).pt = ∏ᶜ fun (s : α) => colimit (F s)

@[simp]

theorem CategoryTheory.Limits.coconePointwiseProduct_ι_app {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] (k : (i : α) → I i) : (coconePointwiseProduct F).ι.app k = Pi.map fun (s : α) => colimit.ι (F s) (k s)

noncomputable def CategoryTheory.Limits.colimitPointwiseProductToProductColimit {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] [HasColimitsOfShape ((i : α) → I i) C] : colimit (pointwiseProduct F) ⟶ ∏ᶜ fun (s : α) => colimit (F s)

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

• CategoryTheory.Limits.colimitPointwiseProductToProductColimit F = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.pointwiseProduct F) (CategoryTheory.Limits.coconePointwiseProduct F)

@[simp]

theorem CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] [HasColimitsOfShape ((i : α) → I i) C] (k : (i : α) → I i) (s : α) : CategoryStruct.comp (colimit.ι (pointwiseProduct F) k) (CategoryStruct.comp (colimitPointwiseProductToProductColimit F) (Pi.π (fun (s : α) => colimit (F s)) s)) = CategoryStruct.comp (Pi.π (fun (s : α) => (F s).obj (k s)) s) (colimit.ι (F s) (k s))

@[simp]

theorem CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π_assoc {C : Type u} [Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → Category.{v₁, u₁} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimitsOfShape (I i) C] [HasColimitsOfShape ((i : α) → I i) C] (k : (i : α) → I i) (s : α) {Z : C} (h : colimit (F s) ⟶ Z) : CategoryStruct.comp (colimit.ι (pointwiseProduct F) k) (CategoryStruct.comp (colimitPointwiseProductToProductColimit F) (CategoryStruct.comp (Pi.π (fun (s : α) => colimit (F s)) s) h)) = CategoryStruct.comp (Pi.π (fun (s : α) => (F s).obj (k s)) s) (CategoryStruct.comp (colimit.ι (F s) (k s)) h)

noncomputable def CategoryTheory.Limits.pointwiseProductCompEvaluation {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} {I : α → Type u₂} [(i : α) → Category.{u_1, u₂} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) (Functor D C)) (d : D) : (pointwiseProduct F).comp ((evaluation D C).obj d) ≅ pointwiseProduct fun (s : α) => (F s).comp ((evaluation D C).obj d)

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) ⋯

@[simp]

theorem CategoryTheory.Limits.pointwiseProductCompEvaluation_hom_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} {I : α → Type u₂} [(i : α) → Category.{u_1, u₂} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) (Functor D C)) (d : D) (X : (i : α) → I i) : (pointwiseProductCompEvaluation F d).hom.app X = (piObjIso (fun (s : α) => (F s).obj (X s)) d).hom

@[simp]

theorem CategoryTheory.Limits.pointwiseProductCompEvaluation_inv_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} {I : α → Type u₂} [(i : α) → Category.{u_1, u₂} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) (Functor D C)) (d : D) (X : (i : α) → I i) : (pointwiseProductCompEvaluation F d).inv.app X = (piObjIso (fun (s : α) => (F s).obj (X s)) d).inv

theorem CategoryTheory.Limits.colimitPointwiseProductToProductColimit_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} {I : α → Type u₂} [(i : α) → Category.{u_1, u₂} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) (Functor D C)) [∀ (i : α), HasColimitsOfShape (I i) C] [HasColimitsOfShape ((i : α) → I i) C] (d : D) : (colimitPointwiseProductToProductColimit F).app d = CategoryStruct.comp (colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).hom (CategoryStruct.comp (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom (CategoryStruct.comp (colimitPointwiseProductToProductColimit fun (s : α) => (F s).comp ((evaluation D C).obj d)) (CategoryStruct.comp (Pi.mapIso fun (x : α) => (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom (piObjIso (fun (x : α) => colimit (F x)) d).inv)))

class CategoryTheory.Limits.IsIPC (C : Type u) [Category.{v, u} C] [HasProducts C] [HasFilteredColimitsOfSize.{w, w, v, u} C] : Prop

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.

theorem CategoryTheory.Limits.Types.isIso_colimitPointwiseProductToProductColimit {α : Type u} {I : α → Type u} [(i : α) → SmallCategory (I i)] [∀ (i : α), IsFiltered (I i)] (F : (i : α) → Functor (I i) (Type u)) : IsIso (colimitPointwiseProductToProductColimit F)

instance CategoryTheory.Limits.instIsIPCType : IsIPC (Type u)

instance CategoryTheory.Limits.instIsIPCFunctor {C : Type u} [Category.{v, u} C] [HasProducts C] [HasFilteredColimitsOfSize.{w, w, v, u} C] [IsIPC C] {D : Type u₁} [Category.{v₁, u₁} D] : IsIPC (Functor D C)