# Connected limits #

A connected limit is a limit whose shape is a connected category.

We give examples of connected categories, and prove that the functor given by (X × -) preserves any connected limit. That is, any limit of shape J where J is a connected category is preserved by the functor (X × -).

Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.ProdPreservesConnectedLimits.γ₂_app {C : Type u₂} [] {J : Type v₂} {K : } (X : C) (Y : J) :
= CategoryTheory.Limits.prod.snd
def CategoryTheory.ProdPreservesConnectedLimits.γ₂ {C : Type u₂} [] {J : Type v₂} {K : } (X : C) :
K.comp (CategoryTheory.Limits.prod.functor.obj X) K

(Impl). The obvious natural transformation from (X × K -) to K.

Equations
• = { app := fun (Y : J) => CategoryTheory.Limits.prod.snd, naturality := }
Instances For
@[simp]
theorem CategoryTheory.ProdPreservesConnectedLimits.γ₁_app {C : Type u₂} [] {J : Type v₂} {K : } (X : C) (Y : J) :
= CategoryTheory.Limits.prod.fst
def CategoryTheory.ProdPreservesConnectedLimits.γ₁ {C : Type u₂} [] {J : Type v₂} {K : } (X : C) :
K.comp (CategoryTheory.Limits.prod.functor.obj X) .obj X

(Impl). The obvious natural transformation from (X × K -) to X

Equations
• = { app := fun (Y : J) => CategoryTheory.Limits.prod.fst, naturality := }
Instances For
@[simp]
theorem CategoryTheory.ProdPreservesConnectedLimits.forgetCone_π {C : Type u₂} [] {J : Type v₂} {X : C} {K : } (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) :
@[simp]
theorem CategoryTheory.ProdPreservesConnectedLimits.forgetCone_pt {C : Type u₂} [] {J : Type v₂} {X : C} {K : } (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) :
def CategoryTheory.ProdPreservesConnectedLimits.forgetCone {C : Type u₂} [] {J : Type v₂} {X : C} {K : } (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) :

(Impl). Given a cone for (X × K -), produce a cone for K using the natural transformation γ₂

Equations
Instances For
noncomputable def CategoryTheory.prodPreservesConnectedLimits {C : Type u₂} [] {J : Type v₂} (X : C) :
CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Limits.prod.functor.obj X)

The functor (X × -) preserves any connected limit. Note that this functor does not preserve the two most obvious disconnected limits - that is, (X × -) does not preserve products or terminal object, eg (X ⨯ A) ⨯ (X ⨯ B) is not isomorphic to X ⨯ (A ⨯ B) and X ⨯ 1 is not isomorphic to 1.

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