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 × -).

instance CategoryTheory.widePullbackShape_connected (J : Type v₁) : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)

Equations

• ⋯ = ⋯

instance CategoryTheory.widePushoutShape_connected (J : Type v₁) : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePushoutShape J)

Equations

• ⋯ = ⋯

instance CategoryTheory.parallelPairInhabited : Inhabited CategoryTheory.Limits.WalkingParallelPair

Equations

• CategoryTheory.parallelPairInhabited = { default := CategoryTheory.Limits.WalkingParallelPair.one }

instance CategoryTheory.parallel_pair_connected : CategoryTheory.IsConnected CategoryTheory.Limits.WalkingParallelPair

Equations

• CategoryTheory.parallel_pair_connected = ⋯

def CategoryTheory.ProdPreservesConnectedLimits.γ₂ {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ K

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

Equations

• CategoryTheory.ProdPreservesConnectedLimits.γ₂ X = { app := fun (x : J) => CategoryTheory.Limits.prod.snd, naturality := ⋯ }

@[simp]

theorem CategoryTheory.ProdPreservesConnectedLimits.γ₂_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : ∀ (x : J), (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X).app x = CategoryTheory.Limits.prod.snd

def CategoryTheory.ProdPreservesConnectedLimits.γ₁ {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ (CategoryTheory.Functor.const J).obj X

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

Equations

• CategoryTheory.ProdPreservesConnectedLimits.γ₁ X = { app := fun (x : J) => CategoryTheory.Limits.prod.fst, naturality := ⋯ }

@[simp]

theorem CategoryTheory.ProdPreservesConnectedLimits.γ₁_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : ∀ (x : J), (CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app x = CategoryTheory.Limits.prod.fst

def CategoryTheory.ProdPreservesConnectedLimits.forgetCone {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : CategoryTheory.Limits.Cone K

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

Equations

• CategoryTheory.ProdPreservesConnectedLimits.forgetCone s = { pt := s.pt, π := CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X) }

@[simp]

theorem CategoryTheory.ProdPreservesConnectedLimits.forgetCone_pt {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).pt = s.pt

@[simp]

theorem CategoryTheory.ProdPreservesConnectedLimits.forgetCone_π {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).π = CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X)

noncomputable def CategoryTheory.prodPreservesConnectedLimits {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] [CategoryTheory.IsConnected J] (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.