mathlib3 documentation

category_theory.limits.connected

Connected limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
def category_theory.wide_pullback_shape_connected (J : Type v₁) :
category_theory.is_connected (category_theory.limits.wide_pullback_shape J)
source
@[protected, instance]
def category_theory.wide_pushout_shape_connected (J : Type v₁) :
category_theory.is_connected (category_theory.limits.wide_pushout_shape J)
source
@[protected, instance]
def category_theory.parallel_pair_inhabited  :
inhabited category_theory.limits.walking_parallel_pair
Equations
source
@[protected, instance]
def category_theory.parallel_pair_connected  :
category_theory.is_connected category_theory.limits.walking_parallel_pair
source
noncomputable def category_theory.prod_preserves_connected_limits.γ₂ {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {K : J ⥤ C} (X : C) :
K ⋙ category_theory.limits.prod.functor.obj X ⟶ K

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

Equations
source
@[simp]
theorem category_theory.prod_preserves_connected_limits.γ₂_app {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {K : J ⥤ C} (X : C) (Y : J) :
(category_theory.prod_preserves_connected_limits.γ₂ X).app Y = category_theory.limits.prod.snd
source
noncomputable def category_theory.prod_preserves_connected_limits.γ₁ {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {K : J ⥤ C} (X : C) :
K ⋙ category_theory.limits.prod.functor.obj X ⟶ (category_theory.functor.const J).obj X

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

Equations
source
@[simp]
theorem category_theory.prod_preserves_connected_limits.γ₁_app {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {K : J ⥤ C} (X : C) (Y : J) :
(category_theory.prod_preserves_connected_limits.γ₁ X).app Y = category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.prod_preserves_connected_limits.forget_cone_X {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {X : C} {K : J ⥤ C} (s : category_theory.limits.cone (K ⋙ category_theory.limits.prod.functor.obj X)) :
(category_theory.prod_preserves_connected_limits.forget_cone s).X = s.X
source
@[simp]
theorem category_theory.prod_preserves_connected_limits.forget_cone_π {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {X : C} {K : J ⥤ C} (s : category_theory.limits.cone (K ⋙ category_theory.limits.prod.functor.obj X)) :
(category_theory.prod_preserves_connected_limits.forget_cone s).π = s.π ≫ category_theory.prod_preserves_connected_limits.γ₂ X
source
noncomputable def category_theory.prod_preserves_connected_limits.forget_cone {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] {X : C} {K : J ⥤ C} (s : category_theory.limits.cone (K ⋙ category_theory.limits.prod.functor.obj X)) :
category_theory.limits.cone K

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

Equations
source
noncomputable def category_theory.prod_preserves_connected_limits {C : Type u₂} [category_theory.category C] [category_theory.limits.has_binary_products C] {J : Type v₂} [category_theory.small_category J] [category_theory.is_connected J] (X : C) :
category_theory.limits.preserves_limits_of_shape J (category_theory.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