CatDat

List of Implications

The following 93 implications and equivalences are available*.

• abelian is equivalent to   additive and  coequalizers and  epi-regular and  equalizers and  mono-regular
• additive and  finitely complete implies   Malcev
• additive and  pullbacks and  subobject classifier implies   trivial
• additive implies   disjoint finite coproducts
• additive is equivalent to   finite products and  preadditive
• balanced and  left cancellative and  right cancellative implies   groupoid
• binary products and  equalizers implies   pullbacks
• binary products and  groupoid and  inhabited implies   trivial
• binary products and  inhabited implies   connected
• binary products and  pullbacks implies   equalizers
• cartesian closed and  coproducts implies   infinitary distributive
• cartesian closed and  finite coproducts implies   distributive
• cartesian closed and  initial object implies   strict initial object
• cartesian closed and  pointed implies   trivial
• cartesian closed implies   finite products
• coequalizers and  left cancellative implies   thin
• complete and  essentially small and  infinitary distributive and  thin implies   cartesian closed
• complete and  essentially small and  thin implies   cocomplete
• complete implies   connected limits and  filtered limits and  finitely complete and  wide pullbacks
• complete is equivalent to   equalizers and  products
• connected limits is equivalent to   equalizers and  wide pullbacks
• connected and  essentially discrete implies   trivial
• connected implies   inhabited
• coproducts and  distributive and  exact filtered colimits implies   infinitary distributive
• countable products and  equalizers implies   sequential limits
• countable products implies   finite products
• discrete implies   essentially discrete and  locally small and  skeletal
• disjoint coproducts is equivalent to   coproducts and  disjoint finite coproducts
• disjoint finite coproducts and  thin implies   trivial
• disjoint finite coproducts implies   finite coproducts
• distributive implies   finite coproducts and  finite products
• distributive implies   strict initial object
• elementary topos and  locally essentially small implies   well-copowered
• elementary topos is equivalent to   cartesian closed and  finitely complete and  subobject classifier
• elementary topos implies   disjoint finite coproducts and  epi-regular and  finitely cocomplete
• equalizers and  groupoid implies   thin
• equalizers implies   Cauchy complete
• essentially discrete implies   connected limits and  locally essentially small
• essentially discrete is equivalent to   groupoid and  thin
• essentially finite and  finite products implies   thin
• essentially finite implies   essentially small
• essentially small and  products implies   thin
• essentially small implies   locally essentially small and  well-copowered and  well-powered
• exact filtered colimits implies   filtered colimits and  finitely complete
• filtered limits and  finite products implies   products
• filtered limits implies   sequential limits
• finitary algebraic implies   locally finitely presentable
• finite coproducts and  preadditive implies   finite products
• finite products and  sequential limits implies   countable products
• finite products is equivalent to   binary products and  terminal object
• finite implies   essentially finite and  small
• finitely complete and  thin implies   Malcev
• finitely complete is equivalent to   equalizers and  finite products
• generator implies   inhabited
• Grothendieck abelian and  self-dual implies   trivial
• Grothendieck abelian is equivalent to   abelian and  coproducts and  exact filtered colimits and  generator
• Grothendieck abelian implies   cogenerator
• Grothendieck abelian implies   locally presentable
• Grothendieck topos implies   cogenerator and  locally presentable
• Grothendieck topos is equivalent to   coproducts and  elementary topos and  generator and  locally essentially small
• groupoid and  initial object implies   trivial
• groupoid implies   filtered limits and  left cancellative and  mono-regular and  pullbacks and  self-dual and  well-powered
• infinitary distributive implies   coproducts and  finite products
• infinitary distributive implies   distributive
• inhabited and  thin implies   generator
• inhabited and  zero morphisms implies   connected
• initial object and  left cancellative implies   strict initial object
• initial object and  right cancellative implies   strict initial object
• left cancellative implies   Cauchy complete
• locally essentially small and  subobject classifier implies   well-powered
• locally finitely presentable implies   exact filtered colimits
• locally finitely presentable implies   locally presentable
• locally finitely presentable implies   locally ℵ₁-presentable
• locally presentable and  self-dual implies   thin
• locally presentable implies   cocomplete and  complete and  generator and  locally essentially small and  well-copowered and  well-powered
• locally small implies   locally essentially small
• locally ℵ₁-presentable implies   locally presentable
• Malcev implies   finitely complete
• mono-regular implies   balanced
• pointed and  strict initial object implies   trivial
• pointed is equivalent to   initial object and  zero morphisms
• preadditive implies   locally essentially small and  zero morphisms
• products implies   countable products and  finite products
• pullbacks and  terminal object implies   binary products
• small implies   essentially small and  locally small
• split abelian implies   abelian
• strict initial object implies   initial object
• subobject classifier implies   finitely complete and  mono-regular
• terminal object and  wide pullbacks implies   complete
• terminal object implies   connected
• thin implies   equalizers and  left cancellative
• trivial implies   essentially discrete and  essentially finite and  finitary algebraic and  Grothendieck topos and  self-dual and  split abelian
• wide pullbacks is equivalent to   filtered limits and  pullbacks

*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.

Moreover, implications are automatically dualized when the corresponding dual properties exist. For example, the statement that finitely complete categories with filtered limits are complete automatically implies that finitely cocomplete categories with filtered colimits are cocomplete. Similarly, if a category is self-dual and, for example, complete, it is automatically inferred to be cocomplete as well.