CatDat

List of Implications

The following 169 implications and equivalences are available*.

• abelian is equivalent to   additive and  equalizers and  coequalizers and  mono-regular and  epi-regular

  by definition
• abelian implies   Malcev
• additive is equivalent to   preadditive and  finite products

  by definition
• additive implies   disjoint finite coproducts

  If $f : T \to A + B$ is a morphism that factors through $A$ and $B$, then $p_B f = 0$ and $p_A f = 0$, so $f = 0$.
• additive and  pullbacks and  subobject classifier implies   trivial

  see MSE/4086192
• additive is equivalent to   preadditive and  finite coproducts

  [dualized] by definition
• binary coproducts and  coequalizers implies   pushouts

  [dualized] The pullback of $f : X \to S$ and $g : Y \to S$ is the equalizer of $p_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S$.
• binary coproducts and  pushouts implies   coequalizers

  [dualized] The equalizer of $f,g : X \rightrightarrows Y$ is the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$.
• binary coproducts and  inhabited implies   connected

  [dualized] For any two objects $A,B$ we have the zig-zag $A \to A \times B \to B$.
• binary products and  equalizers implies   pullbacks

  The pullback of $f : X \to S$ and $g : Y \to S$ is the equalizer of $p_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S$.
• binary products and  pullbacks implies   equalizers

  The equalizer of $f,g : X \rightrightarrows Y$ is the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$.
• binary products and  inhabited implies   connected

  For any two objects $A,B$ we have the zig-zag $A \to A \times B \to B$.
• cartesian closed and  finite coproducts implies   distributive

  Each functor $A \times -$ is left adjoint and hence preserves finite coproducts (in fact, all colimits).
• cartesian closed and  coproducts implies   infinitary distributive

  Each functor $A \times -$ is left adjoint and hence preserves coproducts (in fact, all colimits).
• cartesian closed implies   finite products

  by definition
• cartesian closed and  initial object implies   strict initial object

  See the nLab.
• cocomplete implies   finitely cocomplete and  filtered colimits and  wide pushouts and  connected colimits

  [dualized] trivial
• cocomplete is equivalent to   coproducts and  coequalizers

  [dualized] Mac Lane, V.2, Cor. 2
• coequalizers implies   Cauchy complete

  [dualized] If $e : X \to X$ is an idempotent, then the equalizer of $e, \mathrm{id}_X : X \rightrightarrows X$ provides a splitting of $e$.
• coequalizers and  countable coproducts implies   sequential colimits

  [dualized] Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. Namely, the limit of $\cdots \to X_2 \to X_1 \to X_0$ is the equalizer of two suitable endomorphisms of $\prod_{n \geq 0} X_n$.
• cogenerator implies   inhabited

  [dualized] trivial
• complete implies   finitely complete and  filtered limits and  wide pullbacks and  connected limits

  trivial
• complete is equivalent to   products and  equalizers

  Mac Lane, V.2, Cor. 2
• connected implies   inhabited

  by definition
• connected colimits is equivalent to   wide pushouts and  coequalizers

  [dualized] The direction $\Rightarrow$ is trivial. The direction $\Leftarrow$ can be found at the nLab.
• connected limits is equivalent to   wide pullbacks and  equalizers

  The direction $\Rightarrow$ is trivial. The direction $\Leftarrow$ can be found at the nLab.
• coproducts implies   finite coproducts and  countable coproducts

  [dualized] trivial
• countable coproducts implies   finite coproducts

  [dualized] trivial
• countable products implies   finite products

  trivial
• discrete implies   essentially discrete and  locally small and  skeletal

  trivial
• disjoint coproducts is equivalent to   coproducts and  disjoint finite coproducts

  easy
• disjoint finite coproducts implies   finite coproducts

  by definition
• disjoint finite coproducts and  thin implies   trivial

  For every object $A$ the two inclusions $A \rightrightarrows A + A$ must be equal, so their equalizer is $A$, but also $0$ since the coproduct is disjoint. Hence $A = 0$.
• distributive implies   finite products and  finite coproducts

  by definition
• distributive implies   strict initial object

  See the nLab.
• distributive and  exact filtered colimits and  coproducts implies   infinitary distributive

  Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts.
• elementary topos is equivalent to   cartesian closed and  finitely complete and  subobject classifier

  by definition
• elementary topos implies   finitely cocomplete and  disjoint finite coproducts and  epi-regular

  Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.
• elementary topos and  locally essentially small implies   well-copowered

  This follows from Mac Lane & Moerdijk, Theorem IV.7.8 (and Prop. I.3.1).
• epi-regular implies   balanced

  [dualized] Any regular monomorphism that is an epimorphism must be an isomorphism.
• equalizers implies   Cauchy complete

  If $e : X \to X$ is an idempotent, then the equalizer of $e, \mathrm{id}_X : X \rightrightarrows X$ provides a splitting of $e$.
• equalizers and  countable products implies   sequential limits

  Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. Namely, the limit of $\cdots \to X_2 \to X_1 \to X_0$ is the equalizer of two suitable endomorphisms of $\prod_{n \geq 0} X_n$.
• essentially discrete is equivalent to   thin and  groupoid

  trivial
• essentially discrete implies   locally essentially small and  connected limits

  trivial
• essentially discrete and  connected implies   trivial

  trivial
• essentially discrete implies   locally essentially small and  connected colimits

  [dualized] trivial
• essentially finite and  finite products implies   thin

  Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case.
• essentially finite implies   essentially small

  trivial
• essentially finite and  finite coproducts implies   thin

  [dualized] Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case.
• essentially small implies   well-powered and  well-copowered and  locally essentially small

  trivial
• essentially small and  products implies   thin

  Mac Lane, V.2, Prop. 3. The proof works for any category with products.
• essentially small and  thin and  complete implies   cocomplete

  The supremum of a subset in a (small) partial order is the infimum of the set of upper bounds.
• essentially small and  thin and  complete and  infinitary distributive implies   cartesian closed

  This is an application of the adjoint functor theorem. Specifically, if $P$ is a complete lattice in which $\sup_i \inf(t,x_i) = \inf(t, \sup_i y_i)$ always holds, then the functor $\int(t,-)$ is a left adjoint because it preserves all suprema.
• essentially small and  coproducts implies   thin

  [dualized] Mac Lane, V.2, Prop. 3. The proof works for any category with products.
• essentially small and  thin and  cocomplete implies   complete

  [dualized] The supremum of a subset in a (small) partial order is the infimum of the set of upper bounds.
• exact filtered colimits implies   filtered colimits and  finitely complete

  by definition
• filtered colimits implies   sequential colimits

  [dualized] trivial
• filtered limits implies   sequential limits

  trivial
• finitary algebraic implies   locally finitely presentable

  Adamek-Rosicky, Cor. 3.7
• finite implies   small and  essentially finite

  trivial
• finite coproducts is equivalent to   initial object and  binary coproducts

  [dualized] The non-trivial direction follows since finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$.
• finite coproducts and  filtered colimits implies   coproducts

  [dualized] The product $\prod_{i \in I} X_i$ is the filtered limit of the finite partial products $\prod_{i \in E} X_i$ where $E$ ranges over the finite subsets of $I$.
• finite coproducts and  sequential colimits implies   countable coproducts

  [dualized] If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$.
• finite products is equivalent to   terminal object and  binary products

  The non-trivial direction follows since finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$.
• finite products and  filtered limits implies   products

  The product $\prod_{i \in I} X_i$ is the filtered limit of the finite partial products $\prod_{i \in E} X_i$ where $E$ ranges over the finite subsets of $I$.
• finite products and  sequential limits implies   countable products

  If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$.
• finitely cocomplete is equivalent to   finite coproducts and  coequalizers

  [dualized] Mac Lane, V.2, Cor. 1
• finitely complete is equivalent to   finite products and  equalizers

  Mac Lane, V.2, Cor. 1
• generator implies   inhabited

  trivial
• Grothendieck abelian is equivalent to   abelian and  coproducts and  generator and  exact filtered colimits

  by definition
• Grothendieck abelian implies   locally presentable

  See Deriving Auslander's formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10.
• Grothendieck abelian implies   cogenerator

  Kashiwara-Schapira, Thm. 9.6.3
• Grothendieck abelian and  self-dual implies   trivial

  This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116.
• Grothendieck topos is equivalent to   elementary topos and  coproducts and  generator and  locally essentially small

  Mac Lane & Moerdijk, Appendix, Prop. 4.4
• Grothendieck topos implies   locally presentable and  cogenerator

  For "locally presentable" see Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3. For "cogenerator" see the nLab.
• groupoid implies   self-dual and  mono-regular and  pullbacks and  filtered limits and  left cancellative and  well-powered

  easy
• groupoid and  equalizers implies   thin

  The equalizer of any parallel pair $f,g$ must be an isomorphism, so $f=g$.
• groupoid and  binary products and  inhabited implies   trivial

  Let $\mathcal{C}$ be an inhabited groupoid with binary products. Then it is connected, so we may assume $\mathcal{C}=BG$ for a group $G$ with unique object $*$. But then $* \times * = *$, so there are $p,q \in G$ such that $G \to G \times G$, $x \mapsto (px,qx)$ is bijective. From here it is an easy exercise to deduce $G=1$.
• groupoid and  initial object implies   trivial

  easy
• groupoid implies   self-dual and  epi-regular and  pushouts and  filtered colimits and  right cancellative and  well-copowered

  [dualized] easy
• groupoid and  coequalizers implies   thin

  [dualized] The equalizer of any parallel pair $f,g$ must be an isomorphism, so $f=g$.
• groupoid and  binary coproducts and  inhabited implies   trivial

  [dualized] Let $\mathcal{C}$ be an inhabited groupoid with binary products. Then it is connected, so we may assume $\mathcal{C}=BG$ for a group $G$ with unique object $*$. But then $* \times * = *$, so there are $p,q \in G$ such that $G \to G \times G$, $x \mapsto (px,qx)$ is bijective. From here it is an easy exercise to deduce $G=1$.
• groupoid and  terminal object implies   trivial

  [dualized] easy
• infinitary distributive implies   finite products and  coproducts

  by definition
• infinitary distributive implies   distributive

  trivial
• initial object implies   connected

  [dualized] If $1$ denotes the terminal object, then for any two objects $A,B$ we have the zig-zag $A \to 1 \leftarrow B$.
• left cancellative and  coequalizers implies   thin

  If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.
• left cancellative and  initial object implies   strict initial object

  It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \mathrm{id}_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.
• left cancellative implies   Cauchy complete

  Any idempotent monomorphism must be the identity and therefore splits.
• left cancellative and  right cancellative and  balanced implies   groupoid

  trivial
• left cancellative and  terminal object implies   strict terminal object

  [dualized] Let $f : A \to 0$ be a morphism. Let $g : 0 \to A$ be the unique morphism. It is an epimorphism by assumption. Also, $f \circ g = \mathrm{id}_0$ since $0$ is initial. But then $g$ is a split monomorphism and an epimorphism, hence an isomorphism.
• locally finitely presentable implies   locally presentable

  Locally finitely presentable categories are by definition the locally $\aleph_0$-presentable categories.
• locally finitely presentable implies   exact filtered colimits

  Special case of Adamek-Rosicky, Prop. 1.59 with $\lambda = \aleph_0$.
• locally finitely presentable implies   locally ℵ₁-presentable

  trivial
• locally presentable implies   locally essentially small and  well-powered and  well-copowered and  complete and  cocomplete and  generator

  For the non-trivial conclusions see Adamek-Rosicky, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.
• locally presentable and  self-dual implies   thin

  This follows from Adamek-Rosicky, Thm. 1.64.
• locally small implies   locally essentially small

  trivial
• locally ℵ₁-presentable implies   locally presentable

  trivial
• Malcev implies   finitely complete

  by definition
• mono-regular implies   balanced

  Any regular monomorphism that is an epimorphism must be an isomorphism.
• pointed is equivalent to   zero morphisms and  initial object

  easy
• pointed and  cartesian closed implies   trivial

  We have $X \cong X \times 1 \cong X \times 0 \cong 0$ for every object $X$.
• pointed is equivalent to   zero morphisms and  terminal object

  [dualized] easy
• preadditive implies   locally essentially small and  zero morphisms

  trivial
• preadditive and  finite coproducts implies   finite products

  Mac Lane, VIII.2., Theorem 2
• preadditive and  finite products implies   finite coproducts

  [dualized] Mac Lane, VIII.2., Theorem 2
• products implies   finite products and  countable products

  trivial
• pullbacks and  terminal object implies   binary products

  If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.
• pushouts and  initial object implies   binary coproducts

  [dualized] If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.
• right cancellative and  initial object implies   strict initial object

  Let $f : A \to 0$ be a morphism. Let $g : 0 \to A$ be the unique morphism. It is an epimorphism by assumption. Also, $f \circ g = \mathrm{id}_0$ since $0$ is initial. But then $g$ is a split monomorphism and an epimorphism, hence an isomorphism.
• right cancellative and  equalizers implies   thin

  [dualized] If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.
• right cancellative and  terminal object implies   strict terminal object

  [dualized] It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \mathrm{id}_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.
• right cancellative implies   Cauchy complete

  [dualized] Any idempotent monomorphism must be the identity and therefore splits.
• self-dual and  complete implies   cocomplete

  trivial by self-duality
• self-dual and  cocomplete implies   complete

  trivial by self-duality
• self-dual and  finitely complete implies   finitely cocomplete

  trivial by self-duality
• self-dual and  finitely cocomplete implies   finitely complete

  trivial by self-duality
• self-dual and  well-powered implies   well-copowered

  trivial by self-duality
• self-dual and  well-copowered implies   well-powered

  trivial by self-duality
• self-dual and  initial object implies   terminal object

  trivial by self-duality
• self-dual and  terminal object implies   initial object

  trivial by self-duality
• self-dual and  products implies   coproducts

  trivial by self-duality
• self-dual and  coproducts implies   products

  trivial by self-duality
• self-dual and  finite products implies   finite coproducts

  trivial by self-duality
• self-dual and  finite coproducts implies   finite products

  trivial by self-duality
• self-dual and  binary products implies   binary coproducts

  trivial by self-duality
• self-dual and  binary coproducts implies   binary products

  trivial by self-duality
• self-dual and  countable products implies   countable coproducts

  trivial by self-duality
• self-dual and  countable coproducts implies   countable products

  trivial by self-duality
• self-dual and  equalizers implies   coequalizers

  trivial by self-duality
• self-dual and  coequalizers implies   equalizers

  trivial by self-duality
• self-dual and  filtered limits implies   filtered colimits

  trivial by self-duality
• self-dual and  filtered colimits implies   filtered limits

  trivial by self-duality
• self-dual and  sequential limits implies   sequential colimits

  trivial by self-duality
• self-dual and  sequential colimits implies   sequential limits

  trivial by self-duality
• self-dual and  connected limits implies   connected colimits

  trivial by self-duality
• self-dual and  connected colimits implies   connected limits

  trivial by self-duality
• self-dual and  strict initial object implies   strict terminal object

  trivial by self-duality
• self-dual and  strict terminal object implies   strict initial object

  trivial by self-duality
• self-dual and  pullbacks implies   pushouts

  trivial by self-duality
• self-dual and  pushouts implies   pullbacks

  trivial by self-duality
• self-dual and  generator implies   cogenerator

  trivial by self-duality
• self-dual and  cogenerator implies   generator

  trivial by self-duality
• self-dual and  left cancellative implies   right cancellative

  trivial by self-duality
• self-dual and  right cancellative implies   left cancellative

  trivial by self-duality
• self-dual and  wide pullbacks implies   wide pushouts

  trivial by self-duality
• self-dual and  wide pushouts implies   wide pullbacks

  trivial by self-duality
• self-dual and  mono-regular implies   epi-regular

  trivial by self-duality
• self-dual and  epi-regular implies   mono-regular

  trivial by self-duality
• small implies   locally small and  essentially small

  trivial
• split abelian implies   abelian

  by definition
• strict initial object implies   initial object

  by definition
• strict initial object and  pointed implies   trivial

  If $0$ is the zero object, then for every object $A$ the unique morphism $A \to 0$ is an isomorphism by assumption.
• strict terminal object implies   terminal object

  [dualized] by definition
• strict terminal object and  pointed implies   trivial

  [dualized] If $0$ is the zero object, then for every object $A$ the unique morphism $A \to 0$ is an isomorphism by assumption.
• subobject classifier and  locally essentially small implies   well-powered

  Mac Lane & Moerdijk, Prop. I.3.1
• subobject classifier implies   finitely complete and  mono-regular

  The first part holds by convention, and the second part: any monomorphism $U \to X$ is the equalizer of $$\chi_U,\chi_X : X \to \Omega$.
• terminal object implies   connected

  If $1$ denotes the terminal object, then for any two objects $A,B$ we have the zig-zag $A \to 1 \leftarrow B$.
• thin implies   equalizers and  left cancellative

  Any two parallel morphisms are equal, so their equalizer is the identity, and every morphism is a monomorphism as well.
• thin and  inhabited implies   generator

  Any object will be a generator for trivial reasons.
• thin and  finitely complete implies   Malcev

  In a thin category, every subobject of $X^2 = X$ containing $X$ is already $X$.
• thin implies   coequalizers and  right cancellative

  [dualized] Any two parallel morphisms are equal, so their equalizer is the identity, and every morphism is a monomorphism as well.
• thin and  inhabited implies   cogenerator

  [dualized] Any object will be a generator for trivial reasons.
• trivial implies   finitary algebraic and  Grothendieck topos and  split abelian and  self-dual and  essentially discrete and  essentially finite

  trivial
• wide pullbacks and  terminal object implies   complete

  See the nLab.
• wide pullbacks is equivalent to   pullbacks and  filtered limits

  To prove $\Leftarrow$, a wide pullback can be constructed as a filtered limit of finite pullbacks, and finite pullbacks can be reduced to binary products (the empty-indexed pullback always exists). Conversely, assume that wide pullbacks exist in $\mathcal{C}$. For every object $A$ then the slice category $\mathcal{C} / A$ has wide pullbacks and a terminal object, hence is complete. Since a filtered limit can be finally reduced to such a slice, we are done.
• wide pushouts and  initial object implies   cocomplete

  [dualized] See the nLab.
• wide pushouts is equivalent to   pushouts and  filtered colimits

  [dualized] To prove $\Leftarrow$, a wide pullback can be constructed as a filtered limit of finite pullbacks, and finite pullbacks can be reduced to binary products (the empty-indexed pullback always exists). Conversely, assume that wide pullbacks exist in $\mathcal{C}$. For every object $A$ then the slice category $\mathcal{C} / A$ has wide pullbacks and a terminal object, hence is complete. Since a filtered limit can be finally reduced to such a slice, we are done.
• zero morphisms and  inhabited implies   connected

  trivial

*Deductions from these implications are automatically incorporated into each category whenever applicable. For instance, if a category is identified as complete, the property of having a terminal object is automatically inferred and added.

Use this link to hide the dualizations.