Documentation

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

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

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 #

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.
Instances For
    @[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] :

    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
      @[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
      Instances For
        @[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 : α) :
        @[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) :
        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.{w, 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
        Instances For
          @[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.{w, 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.{w, 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

          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.

          Instances
            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)) :