The IPC property

Given a family of categories I i (i : α) and a family of functors F i : I i ⥤ C, we consider the diagram pointwiseProduct F : Π i, I i ⥤ C defined by (Xᵢ)ᵢ ↦ ∏ᶜ Xᵢ. Given a cocone cᵢ on Fᵢ for each i, there is a natural cocone on pointwiseProduct F with point ∏ᶜ cᵢ.

Similarly to the study of finite limits commuting with filtered colimits, we then study sufficient conditions for this cocone to be colimiting if all the cᵢ are colimiting. 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.

Main definitions

• CategoryTheory.Limits.IsIPCOfShape: C satisfies w-IPC of shape α if w-sized filtered colimits commute products of shape α, i.e. if the joint cocone from above is colimiting if the components are.
• CategoryTheory.Limits.IsIPC: C satisfies the w-IPC property if it satisfies w-IPC for every α : Type w.

Main results

• The category Type u satisfies the u-IPC property (available by inferInstance).
• If C satisfies the w-IPC property, then D ⥤ C satisfies the w-IPC property (available by inferInstance).

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.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.pointwiseProduct {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α 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

• CategoryTheory.Limits.pointwiseProduct F = (CategoryTheory.Functor.pi F).comp (CategoryTheory.Limits.Pi.functor α)

noncomputable def CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) {β : Type u_3} (f : β ≃ α) [HasProductsOfShape β C] : (Pi.equivalenceOfEquiv I f).inverse.comp (pointwiseProduct fun (i : β) => F (f i)) ≅ pointwiseProduct F

pointwiseProduct is invariant under re-indexing.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_inv_app {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) {β : Type u_3} (f : β ≃ α) [HasProductsOfShape β C] (X : (i : α) → I i) : (equivalenceOfEquivCompPointwiseProduct F f).inv.app X = map' ⇑f fun (j : β) => CategoryStruct.id ((F (f j)).obj (X (f j)))

@[simp]

theorem CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_hom_app {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) {β : Type u_3} (f : β ≃ α) [HasProductsOfShape β C] (X : (i : α) → I i) : (equivalenceOfEquivCompPointwiseProduct F f).hom.app X = map' ⇑f.symm fun (k : α) => eqToHom ⋯

noncomputable def CategoryTheory.Limits.coconePointwiseProduct {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] {F : (i : α) → Functor (I i) C} (c : (i : α) → Cocone (F i)) : 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 u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] {F : (i : α) → Functor (I i) C} (c : (i : α) → Cocone (F i)) : (coconePointwiseProduct c).pt = ∏ᶜ fun (i : α) => (c i).pt

@[simp]

theorem CategoryTheory.Limits.coconePointwiseProduct_ι {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] {F : (i : α) → Functor (I i) C} (c : (i : α) → Cocone (F i)) : (coconePointwiseProduct c).ι = CategoryStruct.comp (Functor.whiskerRight (NatTrans.pi fun (i : α) => (c i).ι) (Pi.functor α)) (Pi.constCompPiIsoConst fun (i : α) => (c i).pt).hom

noncomputable def CategoryTheory.Limits.coconePointwiseProductIso {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) {c c' : (i : α) → Cocone (F i)} (e : (i : α) → c i ≅ c' i) : coconePointwiseProduct c ≅ coconePointwiseProduct c'

coconePointwiseProduct is invariant under isomorphisms of cocones.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.colimitPointwiseProductToProductColimit {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimit (F i)] [HasColimit ((Functor.pi F).comp (Pi.functor α))] : 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). A category has the IPC property of shape α if this morphism is an isomorphism as long as the indexing categories are filtered.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimit (F i)] [HasColimit (pointwiseProduct F)] (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.π ((Functor.pi F).obj k) s) (colimit.ι (F s) (k s))

@[simp]

theorem CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π_assoc {C : Type u} [Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → Category.{v_1, u_2} (I i)] [HasProductsOfShape α C] (F : (i : α) → Functor (I i) C) [∀ (i : α), HasColimit (F i)] [HasColimit (pointwiseProduct F)] (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.π ((Functor.pi F).obj k) s) (CategoryStruct.comp (colimit.ι (F s) (k s)) h)

noncomputable def CategoryTheory.Limits.pointwiseProductCompEvaluation {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → Category.{u_5, u_4} (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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.pointwiseProductCompEvaluation_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → Category.{u_5, u_4} (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 ((Functor.pi F).obj X) d).hom

@[simp]

theorem CategoryTheory.Limits.pointwiseProductCompEvaluation_inv_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → Category.{u_5, u_4} (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 ((Functor.pi F).obj X) d).inv

noncomputable def CategoryTheory.Limits.evaluationCoconePointwiseProductIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → Category.{u_5, u_4} (I i)] [HasLimitsOfShape (Discrete α) C] (F : (i : α) → Functor (I i) (Functor D C)) (X : D) (c : (i : α) → Cocone (F i)) : ((evaluation D C).obj X).mapCocone (coconePointwiseProduct c) ≅ (Cocone.precompose (pointwiseProductCompEvaluation F X).hom).obj (coconePointwiseProduct fun (i : α) => ((evaluation D C).obj X).mapCocone (c i))

In a functor category, coconePointwiseProduct commutes with evaluation.

Equations

• CategoryTheory.Limits.evaluationCoconePointwiseProductIso F X c = CategoryTheory.Limits.Cocone.ext (CategoryTheory.Limits.piObjIso (fun (i : α) => (c i).pt) X) ⋯

theorem CategoryTheory.Limits.colimitPointwiseProductToProductColimit_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → Category.{u_5, u_4} (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.IsIPCOfShape (ι : Type u_3) (C : Type u_4) [Category.{v_2, u_4} C] [HasProductsOfShape ι C] : Prop

A category C has the w-IPC property for shape ι if w-sized filtered colimits commute with products of shape ι.

• nonempty_isColimit ⦃J : ι → Type w⦄ [(i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] ⦃F : (i : ι) → Functor (J i) C⦄ ⦃c : (i : ι) → Cocone (F i)⦄ : ∀ (a : (i : ι) → IsColimit (c i)), Nonempty (IsColimit (coconePointwiseProduct c))

instance CategoryTheory.Limits.instIsIsoColimitPointwiseProductToProductColimitOfIsIPCOfShapeOfIsFiltered {C : Type u_1} [Category.{v_1, u_1} C] {ι : Type u_2} [HasProductsOfShape ι C] [IsIPCOfShape.{w, u_2, v_1, u_1} ι C] {J : ι → Type w} [(i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → Functor (J i) C) [∀ (i : ι), HasColimit (F i)] [HasColimit (pointwiseProduct F)] : IsIso (colimitPointwiseProductToProductColimit F)

theorem CategoryTheory.Limits.IsIPCOfShape.of_forall_exists {C : Type u_1} [Category.{v_1, u_1} C] {ι : Type u_2} [HasProductsOfShape ι C] (H : ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → Functor (J i) C) [∀ (i : ι), HasColimit (F i)], ∃ (c : (i : ι) → Cocone (F i)) (x : (i : ι) → IsColimit (c i)), Nonempty (IsColimit (coconePointwiseProduct c))) : IsIPCOfShape.{w, u_2, v_1, u_1} ι C

theorem CategoryTheory.Limits.IsIPCOfShape.of_isIso {C : Type u_1} [Category.{v_1, u_1} C] {ι : Type u_2} [HasProductsOfShape ι C] (H : ∀ (J : ι → Type w) [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → Functor (J i) C) [inst_2 : ∀ (i : ι), HasColimit (F i)], ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)) : IsIPCOfShape.{w, u_2, v_1, u_1} ι C

theorem CategoryTheory.Limits.IsIPCOfShape.of_equiv {C : Type u_1} [Category.{v_1, u_1} C] {ι : Type u_2} [HasProductsOfShape ι C] {ι' : Type u_3} [HasProductsOfShape ι' C] [IsIPCOfShape.{w, u_2, v_1, u_1} ι C] (e : ι ≃ ι') : IsIPCOfShape.{w, u_3, v_1, u_1} ι' C

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

A category C has the w-IPC property it satisfies the IPC-property for every ι : Type w.

• isIPCOfShape (ι : Type w) : IsIPCOfShape.{w, w, v_1, u_1} ι C

instance CategoryTheory.Limits.instIsIPCOfShapeOfIsIPCOfSmall {C : Type u_1} [Category.{v_1, u_1} C] [HasProducts C] [HasFilteredColimitsOfSize.{w, w, v_1, u_1} C] [IsIPC C] (ι : Type u_3) [Small.{w, u_3} ι] [HasProductsOfShape ι C] : IsIPCOfShape.{w, u_3, v_1, u_1} ι C

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.instIsIPCOfShapeFunctorOfHasFilteredColimitsOfSize {C : Type u} [Category.{v, u} C] (ι : Type u_1) [HasProductsOfShape ι C] [IsIPCOfShape.{w, u_1, v, u} ι C] [HasFilteredColimitsOfSize.{w, w, v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] : IsIPCOfShape.{w, u_1, max u₁ v, max (max (max u u₁) v) v₁} ι (Functor D C)

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)