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
- category_theory.parallel_pair_connected = category_theory.connected.of_induct category_theory.parallel_pair_connected._proof_1
(Impl). The obvious natural transformation from (X × K -) to K.
Equations
- category_theory.prod_preserves_connected_limits.γ₂ X = {app := λ (Y : J), category_theory.limits.prod.snd, naturality' := _}
(Impl). The obvious natural transformation from (X × K -) to X
Equations
- category_theory.prod_preserves_connected_limits.γ₁ X = {app := λ (Y : J), category_theory.limits.prod.fst, naturality' := _}
(Impl). Given a cone for (X × K -), produce a cone for K using the natural transformation γ₂
Equations
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
- category_theory.prod_preserves_connected_limits X = {preserves_limit := λ (K : J ⥤ C), {preserves := λ (c : category_theory.limits.cone K) (l : category_theory.limits.is_limit c), {lift := λ (s : category_theory.limits.cone (K ⋙ category_theory.limits.prod_functor.obj X)), category_theory.limits.prod.lift (s.π.app (inhabited.default J) ≫ category_theory.limits.prod.fst) (l.lift (category_theory.prod_preserves_connected_limits.forget_cone s)), fac' := _, uniq' := _}}}