Preservations of limits for bifunctors #
Let G : C₁ ⥤ C₂ ⥤ C a functor. We introduce a class PreservesLimit₂ K₁ K₂ G that encodes
the hypothesis that the curried functor F : C₁ × C₂ ⥤ C preserves limits of the diagram
K₁ × K₂ : J₁ × J₂ ⥤ C₁ × C₂. We give a basic API to extract isomorphisms
$\lim_{(j_1,j_2)} G(K_1(j_1), K_2(j_2)) \simeq G(\lim K_1, \lim K_2)$
out of this typeclass.
def
CategoryTheory.Functor.mapCocone₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cocone K₁)
(c₂ : Limits.Cocone K₂)
:
Limits.Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
Given a bifunctor G : C₁ ⥤ C₂ ⥤ C, diagrams K₁ : J₁ ⥤ C₁ and K₂ : J₂ ⥤ C₂, and cocones
over these diagrams, G.mapCocone₂ c₁ c₂ is the cocone over the diagram J₁ × J₂ ⥤ C obtained
by applying G to both c₁ and c₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapCocone₂_pt
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cocone K₁)
(c₂ : Limits.Cocone K₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapCocone₂_ι_app
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cocone K₁)
(c₂ : Limits.Cocone K₂)
(x✝ : J₁ × J₂)
:
def
CategoryTheory.Functor.mapCone₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cone K₁)
(c₂ : Limits.Cone K₂)
:
Limits.Cone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
Given a bifunctor G : C₁ ⥤ C₂ ⥤ C, diagrams K₁ : J₁ ⥤ C₁ and K₂ : J₂ ⥤ C₂, and cones
over these diagrams, G.mapCone₂ c₁ c₂ is the cone over the diagram J₁ × J₂ ⥤ C obtained
by applying G to both c₁ and c₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapCone₂_π_app
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cone K₁)
(c₂ : Limits.Cone K₂)
(x✝ : J₁ × J₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapCone₂_pt
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(G : Functor C₁ (Functor C₂ C))
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(c₁ : Limits.Cone K₁)
(c₂ : Limits.Cone K₂)
:
class
CategoryTheory.Limits.PreservesColimit₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
:
A functor PreservesColimit₂ K₁ K₂ if whenever c₁ is a colimit cocone and c₂ is a colimit
cocone then G.mapCocone₂ c₁ c₂ is a colimit cocone. This can be thought of as the data of an
isomorphism
$\mathrm{colim}_{(j_1,j_2)} G(K_1(j_1),K_2(j_2)) \simeq G(\mathrm{colim} K_1,\mathrm{colim} K_2)$.
Instances
class
CategoryTheory.Limits.PreservesLimit₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
:
A functor PreservesLimit₂ K₁ K₂ if whenever c₁ is a limit cone and c₂ is a limit
cone then G.mapCone₂ c₁ c₂ is a limit cone. This can be thought of as the data of an
isomorphism $\lim_{(j_1,j_2)} G(K_1(j_1), K_2(j_2)) \simeq G(\lim K_1, \lim K_2)$.
Instances
noncomputable def
CategoryTheory.Limits.isColimitOfPreserves₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
:
IsColimit (G.mapCocone₂ c₁ c₂)
If PreservesColimit₂ K₁ K₂ G, obtain that G.mapCocone₂ c₁ c₂ is a colimit cocone
whenever c₁ c₂ are colimit cocones.
Equations
- CategoryTheory.Limits.isColimitOfPreserves₂ G hc₁ hc₂ = ⋯.some
Instances For
noncomputable def
CategoryTheory.Limits.isLimitOfPreserves₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
:
If PreservesLimit₂ K₁ K₂ G, obtain that G.mapCone₂ c₁ c₂ is a limit cone
whenever c₁ c₂ are limit cones.
Equations
- CategoryTheory.Limits.isLimitOfPreserves₂ G hc₁ hc₂ = ⋯.some
Instances For
instance
CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_7, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[HasColimit K₁]
[HasColimit K₂]
[PreservesColimit₂ K₁ K₂ G]
:
HasColimit (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
instance
CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_7, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[HasLimit K₁]
[HasLimit K₂]
[PreservesLimit₂ K₁ K₂ G]
:
HasLimit (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
noncomputable def
CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
{c₃ : Cocone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsColimit c₃)
:
Given a PreservesColimit₂ instance, extract the isomorphism between
a colimit of uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G) and
(G.obj c₁).obj c₂ where c₁ (resp. c₂) is a colimit of K₁ (resp K₂).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_7, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
{c₃ : Cocone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsColimit c₃)
(j : J₁ × J₂)
:
Characterize the inverse direction of the isomorphism
PreservesColimit₂.isoObjCoconePointsOfIsColimit w.r.t. the canonical maps to the colimit.
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_7, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
{c₃ : Cocone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsColimit c₃)
(j : J₁ × J₂)
{Z : C}
(h : (G.obj c₁.pt).obj c₂.pt ⟶ Z)
:
CategoryStruct.comp (c₃.ι.app j) (CategoryStruct.comp (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv h) = CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2))
(CategoryStruct.comp ((G.obj c₁.pt).map (c₂.ι.app j.2)) h)
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
{c₃ : Cocone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsColimit c₃)
(j : J₁ × J₂)
:
Characterize the forward direction of the isomorphism
PreservesColimit₂.isoObjCoconePointsOfIsColimit w.r.t. the canonical maps to the colimit.
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
{c₁ : Cocone K₁}
(hc₁ : IsColimit c₁)
{c₂ : Cocone K₂}
(hc₂ : IsColimit c₂)
{c₃ : Cocone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsColimit c₃)
(j : J₁ × J₂)
{Z : C}
(h : c₃.pt ⟶ Z)
:
CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2))
(CategoryStruct.comp ((G.obj c₁.pt).map (c₂.ι.app j.2))
(CategoryStruct.comp (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom h)) = CategoryStruct.comp (c₃.ι.app j) h
noncomputable def
CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
[HasColimit K₁]
[HasColimit K₂]
:
Extract the isomorphism between
colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)) and
(G.obj (colim K₁)).obj (colim K₂) from a PreservesColimit₂ instance, provided the relevant
colimits exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
[HasColimit K₁]
[HasColimit K₂]
(j : J₁ × J₂)
:
CategoryStruct.comp (colimit.ι (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
(isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom = CategoryStruct.comp ((G.map (colimit.ι K₁ j.1)).app (K₂.obj j.2)) ((G.obj (colimit K₁)).map (colimit.ι K₂ j.2))
Characterize the forward direction of the isomorphism
PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ w.r.t. the canonical maps to the colimit.
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
[HasColimit K₁]
[HasColimit K₂]
(j : J₁ × J₂)
{Z : C}
(h : (G.obj (colimit K₁)).obj (colimit K₂) ⟶ Z)
:
CategoryStruct.comp (colimit.ι (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
(CategoryStruct.comp (isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom h) = CategoryStruct.comp ((G.map (colimit.ι K₁ j.1)).app (K₂.obj j.2))
(CategoryStruct.comp ((G.obj (colimit K₁)).map (colimit.ι K₂ j.2)) h)
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
[HasColimit K₁]
[HasColimit K₂]
(j : J₁ × J₂)
:
CategoryStruct.comp ((G.map (colimit.ι K₁ j.1)).app (K₂.obj j.2))
(CategoryStruct.comp ((G.obj (colimit K₁)).map (colimit.ι K₂ j.2)) (isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv) = colimit.ι (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j
Characterize the forward direction of the isomorphism
PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ w.r.t. the canonical maps to the colimit.
@[simp]
theorem
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
[HasColimit K₁]
[HasColimit K₂]
(j : J₁ × J₂)
{Z : C}
(h : colimit (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) ⟶ Z)
:
CategoryStruct.comp ((G.map (colimit.ι K₁ j.1)).app (K₂.obj j.2))
(CategoryStruct.comp ((G.obj (colimit K₁)).map (colimit.ι K₂ j.2))
(CategoryStruct.comp (isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv h)) = CategoryStruct.comp (colimit.ι (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j) h
instance
CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_7, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_8, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)]
[∀ (x : C₁), PreservesColimit K₂ (G.obj x)]
:
PreservesColimit₂ K₁ K₂ G
If a bifunctor preserves separately colimits of K₁ in the first variable and colimits
of K₂ in the second variable, then it preserves colimit of the pair K₁, K₂.
theorem
CategoryTheory.Limits.PreservesColimit₂.of_preservesColimit₂_flip
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_10, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesColimit₂ K₁ K₂ G]
:
PreservesColimit₂ K₂ K₁ G.flip
noncomputable def
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
{c₃ : Cone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsLimit c₃)
:
Given a PreservesLimit₂ instance, extract the isomorphism between
a limit of uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G) and
(G.obj c₁).obj c₂ where c₁ (resp. c₂) is a limit of K₁ (resp K₂).
Equations
- CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃ = (CategoryTheory.Limits.isLimitOfPreserves₂ G hc₁ hc₂).conePointUniqueUpToIso hc₃
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
{c₃ : Cone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsLimit c₃)
(j : J₁ × J₂)
:
Characterize the forward direction of the isomorphism
PreservesLimit₂.isoObjConePointsOfIsLimit w.r.t. the canonical maps to the limit.
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
{c₃ : Cone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsLimit c₃)
(j : J₁ × J₂)
{Z : C}
(h : (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).obj j ⟶ Z)
:
CategoryStruct.comp (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom (CategoryStruct.comp (c₃.π.app j) h) = CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt)
(CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2)) h)
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_7, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
{c₃ : Cone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsLimit c₃)
(j : J₁ × J₂)
:
Characterize the inverse direction of the isomorphism
PreservesLimit₂.isoObjConePointsOfIsLimit w.r.t. the canonical maps to the limit.
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_7, u_1} J₁]
[Category.{u_8, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
{c₁ : Cone K₁}
(hc₁ : IsLimit c₁)
{c₂ : Cone K₂}
(hc₂ : IsLimit c₂)
{c₃ : Cone (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
(hc₃ : IsLimit c₃)
(j : J₁ × J₂)
{Z : C}
(h : (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ Z)
:
CategoryStruct.comp (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).inv
(CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt)
(CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2)) h)) = CategoryStruct.comp (c₃.π.app j) h
noncomputable def
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_10, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
[HasLimit K₁]
[HasLimit K₂]
:
Extract the isomorphism between
colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)) and
(G.obj (colim K₁)).obj (colim K₂) from a PreservesLimit₂ instance, provided the relevant
limits exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
[HasLimit K₁]
[HasLimit K₂]
(j : J₁ × J₂)
:
CategoryStruct.comp (isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv
(limit.π (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j) = CategoryStruct.comp ((G.map (limit.π K₁ j.1)).app (limit K₂)) ((G.obj (K₁.obj j.1)).map (limit.π K₂ j.2))
Characterize the inverse direction of the isomorphism
PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ w.r.t. the canonical maps to the limit.
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_9, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_8, u_3} C₁]
[Category.{u_7, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
[HasLimit K₁]
[HasLimit K₂]
(j : J₁ × J₂)
{Z : C}
(h : (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).obj j ⟶ Z)
:
CategoryStruct.comp (isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv
(CategoryStruct.comp (limit.π (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j) h) = CategoryStruct.comp ((G.map (limit.π K₁ j.1)).app (limit K₂))
(CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (limit.π K₂ j.2)) h)
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
[HasLimit K₁]
[HasLimit K₂]
(j : J₁ × J₂)
:
CategoryStruct.comp (isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom
(CategoryStruct.comp ((G.map (limit.π K₁ j.1)).app (limit K₂)) ((G.obj (K₁.obj j.1)).map (limit.π K₂ j.2))) = limit.π (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j
Characterize the forward direction of the isomorphism
PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ w.r.t. the canonical maps to the limit.
@[simp]
theorem
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_9, u_3} C₁]
[Category.{u_10, u_4} C₂]
[Category.{u_6, u_5} C]
(K₁ : Functor J₁ C₁)
(K₂ : Functor J₂ C₂)
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
[HasLimit K₁]
[HasLimit K₂]
(j : J₁ × J₂)
{Z : C}
(h : (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ Z)
:
CategoryStruct.comp (isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom
(CategoryStruct.comp ((G.map (limit.π K₁ j.1)).app (limit K₂))
(CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (limit.π K₂ j.2)) h)) = CategoryStruct.comp (limit.π (Functor.uncurry.obj ((((Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j) h
instance
CategoryTheory.Limits.PreservesLimit₂.of_preservesLimits_in_each_variable
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_6, u_1} J₁]
[Category.{u_10, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_7, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_8, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)]
[∀ (x : C₁), PreservesLimit K₂ (G.obj x)]
:
PreservesLimit₂ K₁ K₂ G
If a bifunctor preserves separately limits of K₁ in the first variable and limits
of K₂ in the second variable, then it preserves colimit of the pair of cones K₁, K₂.
theorem
CategoryTheory.Limits.PreservesLimit₂.of_preservesLimit₂_flip
{J₁ : Type u_1}
{J₂ : Type u_2}
[Category.{u_8, u_1} J₁]
[Category.{u_7, u_2} J₂]
{C₁ : Type u_3}
{C₂ : Type u_4}
{C : Type u_5}
[Category.{u_10, u_3} C₁]
[Category.{u_9, u_4} C₂]
[Category.{u_6, u_5} C]
{K₁ : Functor J₁ C₁}
{K₂ : Functor J₂ C₂}
(G : Functor C₁ (Functor C₂ C))
[PreservesLimit₂ K₁ K₂ G]
:
PreservesLimit₂ K₂ K₁ G.flip