Documentation

Mathlib.CategoryTheory.Limits.Connected

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

source
instance CategoryTheory.widePullbackShape_connected (J : Type v₁) :
CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)
Equations
source
instance CategoryTheory.widePushoutShape_connected (J : Type v₁) :
CategoryTheory.IsConnected (CategoryTheory.Limits.WidePushoutShape J)
Equations
source
instance CategoryTheory.parallelPairInhabited :
Inhabited CategoryTheory.Limits.WalkingParallelPair
Equations
source
instance CategoryTheory.parallel_pair_connected :
CategoryTheory.IsConnected CategoryTheory.Limits.WalkingParallelPair
Equations
source
@[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) (Y : J) :
(CategoryTheory.ProdPreservesConnectedLimits.γ₂ X).app Y = CategoryTheory.Limits.prod.snd
source
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) :
CategoryTheory.Functor.comp K (CategoryTheory.Limits.prod.functor.toPrefunctor.obj X) ⟶ K

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

Equations
Instances For
    source
    @[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) (Y : J) :
    (CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app Y = CategoryTheory.Limits.prod.fst
    source
    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) :
    CategoryTheory.Functor.comp K (CategoryTheory.Limits.prod.functor.toPrefunctor.obj X) ⟶ (CategoryTheory.Functor.const J).toPrefunctor.obj X

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

    Equations
    Instances For
      source
      @[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 (CategoryTheory.Functor.comp K (CategoryTheory.Limits.prod.functor.toPrefunctor.obj X))) :
      (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).π = CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X)
      source
      @[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 (CategoryTheory.Functor.comp K (CategoryTheory.Limits.prod.functor.toPrefunctor.obj X))) :
      (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).pt = s.pt
      source
      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 (CategoryTheory.Functor.comp K (CategoryTheory.Limits.prod.functor.toPrefunctor.obj X))) :
      CategoryTheory.Limits.Cone K

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

      Equations
      Instances For
        source
        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.toPrefunctor.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
        Instances For