Connected limits

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

We show that constant functors from a connected category have a limit and a colimit. From this we deduce that a cocone c over a connected diagram is a colimit cocone if and only if colimMap c.ι is an isomorphism (where c.ι : F ⟶ const c.pt is the natural transformation that defines the cocone).

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

def CategoryTheory.Limits.constCone (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : Cone ((Functor.const J).obj X)

The obvious cone of a constant functor.

Equations

• CategoryTheory.Limits.constCone J X = { pt := X, π := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const J).obj X) }

@[simp]

theorem CategoryTheory.Limits.constCone_pt (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : (constCone J X).pt = X

@[simp]

theorem CategoryTheory.Limits.constCone_π (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : (constCone J X).π = CategoryStruct.id ((Functor.const J).obj X)

def CategoryTheory.Limits.constCocone (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : Cocone ((Functor.const J).obj X)

The obvious cocone of a constant functor.

Equations

• CategoryTheory.Limits.constCocone J X = { pt := X, ι := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const J).obj X) }

@[simp]

theorem CategoryTheory.Limits.constCocone_ι (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : (constCocone J X).ι = CategoryStruct.id ((Functor.const J).obj X)

@[simp]

theorem CategoryTheory.Limits.constCocone_pt (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) : (constCocone J X).pt = X

def CategoryTheory.Limits.isLimitConstCone (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) [IsConnected J] : IsLimit (constCone J X)

When J is a connected category, the limit of a constant functor J ⥤ C with value X : C identifies to X.

Equations

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

def CategoryTheory.Limits.isColimitConstCocone (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) [IsConnected J] : IsColimit (constCocone J X)

When J is a connected category, the colimit of a constant functor J ⥤ C with value X : C identifies to X.

Equations

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

instance CategoryTheory.Limits.hasLimit_const_of_isConnected (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) [IsConnected J] : HasLimit ((Functor.const J).obj X)

instance CategoryTheory.Limits.hasColimit_const_of_isConnected (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) [IsConnected J] : HasColimit ((Functor.const J).obj X)

def CategoryTheory.Limits.Cone.isLimitOfIsIsoLimMapπ {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasLimit F] (c : Cone F) [IsIso (limMap c.π)] : IsLimit c

If J is connected, F : J ⥤ C and c is a cone on F, then to check that c is a limit it is sufficient to check that limMap c.π is an isomorphism. The converse is also true, see Cone.isLimit_iff_isIso_limMap_π.

Equations

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

theorem CategoryTheory.Limits.IsLimit.isIso_limMap_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasLimit F] {c : Cone F} (hc : IsLimit c) : IsIso (limMap c.π)

theorem CategoryTheory.Limits.Cone.isLimit_iff_isIso_limMap_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasLimit F] (c : Cone F) : Nonempty (IsLimit c) ↔ IsIso (limMap c.π)

def CategoryTheory.Limits.Cocone.isColimitOfIsIsoColimMapι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasColimit F] (c : Cocone F) [IsIso (colimMap c.ι)] : IsColimit c

If J is connected, F : J ⥤ C and C is a cocone on F, then to check that c is a colimit it is sufficient to check that colimMap c.ι is an isomorphism. The converse is also true, see Cocone.isColimit_iff_isIso_colimMap_ι.

Equations

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

theorem CategoryTheory.Limits.IsColimit.isIso_colimMap_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) : IsIso (colimMap c.ι)

theorem CategoryTheory.Limits.Cocone.isColimit_iff_isIso_colimMap_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [IsConnected J] {F : Functor J C} [HasColimit F] (c : Cocone F) : Nonempty (IsColimit c) ↔ IsIso (colimMap c.ι)

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

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

instance CategoryTheory.parallelPairInhabited : Inhabited Limits.WalkingParallelPair

Equations

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

instance CategoryTheory.parallel_pair_connected : IsConnected Limits.WalkingParallelPair

def CategoryTheory.ProdPreservesConnectedLimits.γ₂ {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {K : Functor J C} (X : C) : K.comp (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₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {K : Functor J C} (X : C) (x✝ : J) : (γ₂ X).app x✝ = Limits.prod.snd

def CategoryTheory.ProdPreservesConnectedLimits.γ₁ {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {K : Functor J C} (X : C) : K.comp (Limits.prod.functor.obj X) ⟶ (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₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {K : Functor J C} (X : C) (x✝ : J) : (γ₁ X).app x✝ = Limits.prod.fst

def CategoryTheory.ProdPreservesConnectedLimits.forgetCone {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {X : C} {K : Functor J C} (s : Limits.Cone (K.comp (Limits.prod.functor.obj X))) : 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₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] {X : C} {K : Functor J C} (s : Limits.Cone (K.comp (Limits.prod.functor.obj X))) : (forgetCone s).pt = s.pt

@[simp]

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

theorem CategoryTheory.prod_preservesConnectedLimits {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasBinaryProducts C] {J : Type v₂} [SmallCategory J] [IsConnected J] (X : C) : Limits.PreservesLimitsOfShape J (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.