CatDat

Properties

Properties from the database

• is locally small
• is essentially small
• is abelian
• has a generator

Deduced properties

• is well-powered

  Since it is essentially small, we deduce that it is well-powered.
• is well-copowered

  Since it is essentially small, we deduce that it is well-copowered.
• is locally essentially small

  Since it is essentially small, we deduce that it is locally essentially small.
• is additive

  Since it is abelian, we deduce that it is additive.
• has equalizers

  Since it is abelian, we deduce that it has equalizers.
• has coequalizers

  Since it is abelian, we deduce that it has coequalizers.
• is mono-regular

  Since it is abelian, we deduce that it is mono-regular.
• is epi-regular

  Since it is abelian, we deduce that it is epi-regular.
• is Malcev

  Since it is abelian, we deduce that it is Malcev.
• is inhabited

  Since it has a generator, we deduce that it is inhabited.
• is balanced

  Since it is mono-regular, we deduce that it is balanced.
• is finitely complete

  Since it is Malcev, we deduce that it is finitely complete.
• is Cauchy complete

  Since it has coequalizers, we deduce that it is Cauchy complete.
• is preadditive

  Since it is additive, we deduce that it is preadditive.
• has finite coproducts

  Since it is additive, we deduce that it has finite coproducts.
• has finite products

  Since it is finitely complete, we deduce that it has finite products.
• has a terminal object

  Since it has finite products, we deduce that it has a terminal object.
• has binary products

  Since it has finite products, we deduce that it has binary products.
• has pullbacks

  Since it has binary products and has equalizers, we deduce that it has pullbacks.
• is connected

  Since it has a terminal object, we deduce that it is connected.
• has zero morphisms

  Since it is preadditive, we deduce that it has zero morphisms.
• has disjoint finite coproducts

  Since it is additive, we deduce that it has disjoint finite coproducts.
• is finitely cocomplete

  Since it has finite coproducts and has coequalizers, we deduce that it is finitely cocomplete.
• has an initial object

  Since it has finite coproducts, we deduce that it has an initial object.
• has binary coproducts

  Since it has finite coproducts, we deduce that it has binary coproducts.
• has pushouts

  Since it has binary coproducts and has coequalizers, we deduce that it has pushouts.
• is pointed

  Since it has zero morphisms and has a terminal object, we deduce that it is pointed.

Non-Properties

Non-Properties from the database

• is not small
• does not have a cogenerator
• is not split abelian
• does not have countable products
• does not have countable coproducts
• is not skeletal

  trivial

Deduced Non-Properties*

• is not complete

  Assume for a contradiction that it is complete. Since it is complete, we deduce that it has products. Since it has products, we deduce that it has countable products. This is a contradiction since we already know that it does not have countable products.
• is not cocomplete

  Assume for a contradiction that it is cocomplete. Since it is cocomplete, we deduce that it has coproducts. Since it has coproducts, we deduce that it has countable coproducts. This is a contradiction since we already know that it does not have countable coproducts.
• is not cartesian closed

  Assume for a contradiction that it is cartesian closed. Since it is pointed and is cartesian closed, we deduce that it is trivial. Since it is trivial, we deduce that it is split abelian. This is a contradiction since we already know that it is not split abelian.
• is not locally finitely presentable

  Assume for a contradiction that it is locally finitely presentable. Since it is locally finitely presentable, we deduce that it is locally presentable. Since it is locally presentable, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• is not locally presentable

  Assume for a contradiction that it is locally presentable. Since it is locally presentable, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• is not locally ℵ₁-presentable

  Assume for a contradiction that it is locally ℵ₁-presentable. Since it is locally ℵ₁-presentable, we deduce that it is locally presentable. This is a contradiction since we already know that it is not locally presentable.
• is not an elementary topos

  Assume for a contradiction that it is an elementary topos. Since it is an elementary topos, we deduce that it is cartesian closed. This is a contradiction since we already know that it is not cartesian closed.
• is not a Grothendieck topos

  Assume for a contradiction that it is a Grothendieck topos. Since it is a Grothendieck topos, we deduce that it is an elementary topos. This is a contradiction since we already know that it is not an elementary topos.
• does not have products

  Assume for a contradiction that it has products. Since it has products and has equalizers, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• does not have coproducts

  Assume for a contradiction that it has coproducts. Since it is essentially small and has coproducts, we deduce that it is thin. Since it is thin and is inhabited, we deduce that it has a cogenerator. This is a contradiction since we already know that it does not have a cogenerator.
• does not have filtered limits

  Assume for a contradiction that it has filtered limits. Since it has finite products and has filtered limits, we deduce that it has products. This is a contradiction since we already know that it does not have products.
• does not have filtered colimits

  Assume for a contradiction that it has filtered colimits. Since it has finite coproducts and has filtered colimits, we deduce that it has coproducts. This is a contradiction since we already know that it does not have coproducts.
• does not have sequential limits

  Assume for a contradiction that it has sequential limits. Since it has finite products and has sequential limits, we deduce that it has countable products. This is a contradiction since we already know that it does not have countable products.
• does not have sequential colimits

  Assume for a contradiction that it has sequential colimits. Since it has finite coproducts and has sequential colimits, we deduce that it has countable coproducts. This is a contradiction since we already know that it does not have countable coproducts.
• does not have connected limits

  Assume for a contradiction that it has connected limits. Since it has connected limits, we deduce that it has wide pullbacks. Since it has wide pullbacks and has a terminal object, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• does not have connected colimits

  Assume for a contradiction that it has connected colimits. Since it has connected colimits, we deduce that it has wide pushouts. Since it has wide pushouts and has an initial object, we deduce that it is cocomplete. This is a contradiction since we already know that it is not cocomplete.
• does not have a strict initial object

  Assume for a contradiction that it has a strict initial object. Since it has a strict initial object and is pointed, we deduce that it is trivial. Since it is trivial, we deduce that it is a Grothendieck topos. This is a contradiction since we already know that it is not a Grothendieck topos.
• does not have a strict terminal object

  Assume for a contradiction that it has a strict terminal object. Since it has a strict terminal object and is pointed, we deduce that it is trivial. Since it is trivial, we deduce that it is a Grothendieck topos. This is a contradiction since we already know that it is not a Grothendieck topos.
• is not self-dual

  Assume for a contradiction that it is self-dual. Since it is self-dual and has a generator, we deduce that it has a cogenerator. This is a contradiction since we already know that it does not have a cogenerator.
• is not a groupoid

  Assume for a contradiction that it is a groupoid. Since it is a groupoid, we deduce that it is self-dual. This is a contradiction since we already know that it is not self-dual.
• is not thin

  Assume for a contradiction that it is thin. Since it is thin, we deduce that it is left cancellative. Since it is left cancellative and has an initial object, we deduce that it has a strict initial object. This is a contradiction since we already know that it does not have a strict initial object.
• is not discrete

  Assume for a contradiction that it is discrete. Since it is discrete, we deduce that it is skeletal. This is a contradiction since we already know that it is not skeletal.
• is not essentially discrete

  Assume for a contradiction that it is essentially discrete. Since it is essentially discrete, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
• is not finitary algebraic

  Assume for a contradiction that it is finitary algebraic. Since it is finitary algebraic, we deduce that it is locally finitely presentable. This is a contradiction since we already know that it is not locally finitely presentable.
• is not finite

  Assume for a contradiction that it is finite. Since it is finite, we deduce that it is small. This is a contradiction since we already know that it is not small.
• is not essentially finite

  Assume for a contradiction that it is essentially finite. Since it is essentially finite and has finite products, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
• is not trivial

  Assume for a contradiction that it is trivial. Since it is trivial, we deduce that it is finitary algebraic. This is a contradiction since we already know that it is not finitary algebraic.
• does not have a subobject classifier

  Assume for a contradiction that it has a subobject classifier. Since it is additive and has pullbacks and has a subobject classifier, we deduce that it is trivial. This is a contradiction since we already know that it is not trivial.
• is not infinitary distributive

  Assume for a contradiction that it is infinitary distributive. Since it is infinitary distributive, we deduce that it has coproducts. This is a contradiction since we already know that it does not have coproducts.
• is not distributive

  Assume for a contradiction that it is distributive. Since it is distributive, we deduce that it has a strict initial object. This is a contradiction since we already know that it does not have a strict initial object.
• does not have exact filtered colimits

  Assume for a contradiction that it has exact filtered colimits. Since it has exact filtered colimits, we deduce that it has filtered colimits. This is a contradiction since we already know that it does not have filtered colimits.
• is not Grothendieck abelian

  Assume for a contradiction that it is Grothendieck abelian. Since it is Grothendieck abelian, we deduce that it has coproducts. This is a contradiction since we already know that it does not have coproducts.
• does not have disjoint coproducts

  Assume for a contradiction that it has disjoint coproducts. Since it has disjoint coproducts, we deduce that it has coproducts. This is a contradiction since we already know that it does not have coproducts.
• is not left cancellative

  Assume for a contradiction that it is left cancellative. Since it is left cancellative and has coequalizers, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
• is not right cancellative

  Assume for a contradiction that it is right cancellative. Since it is right cancellative and has an initial object, we deduce that it has a strict initial object. This is a contradiction since we already know that it does not have a strict initial object.
• does not have wide pullbacks

  Assume for a contradiction that it has wide pullbacks. Since it has wide pullbacks and has equalizers, we deduce that it has connected limits. This is a contradiction since we already know that it does not have connected limits.
• does not have wide pushouts

  Assume for a contradiction that it has wide pushouts. Since it has wide pushouts and has coequalizers, we deduce that it has connected colimits. This is a contradiction since we already know that it does not have connected colimits.

*This also uses the deduced properties.