CatDat

Properties

Properties from the database

• is trivial
• is finite

Deduced properties

• is small

  Since it is finite, we deduce that it is small.
• is essentially finite

  Since it is finite, we deduce that it is essentially finite.
• is essentially small

  Since it is essentially finite, we deduce that it is essentially small.
• is finitary algebraic

  Since it is trivial, we deduce that it is finitary algebraic.
• is a Grothendieck topos

  Since it is trivial, we deduce that it is a Grothendieck topos.
• is split abelian

  Since it is trivial, we deduce that it is split abelian.
• is self-dual

  Since it is trivial, we deduce that it is self-dual.
• is essentially discrete

  Since it is trivial, we deduce that it is essentially discrete.
• is locally finitely presentable

  Since it is finitary algebraic, we deduce that it is locally finitely presentable.
• is an elementary topos

  Since it is a Grothendieck topos, we deduce that it is an elementary topos.
• has coproducts

  Since it is a Grothendieck topos, we deduce that it has coproducts.
• has a generator

  Since it is a Grothendieck topos, we deduce that it has a generator.
• is locally essentially small

  Since it is a Grothendieck topos, we deduce that it is locally essentially small.
• is locally presentable

  Since it is a Grothendieck topos, we deduce that it is locally presentable.
• has a cogenerator

  Since it is a Grothendieck topos, we deduce that it has a cogenerator.
• is abelian

  Since it is split abelian, we deduce that it is abelian.
• 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 finitely complete

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

  Since it is essentially small and has coproducts, we deduce that it is thin.
• has connected colimits

  Since it is essentially discrete, we deduce that it has connected colimits.
• has coequalizers

  Since it is thin, we deduce that it has coequalizers.
• is right cancellative

  Since it is thin, we deduce that it is right cancellative.
• is cocomplete

  Since it has coproducts and has coequalizers, we deduce that it is cocomplete.
• has finite coproducts

  Since it has coproducts, we deduce that it has finite coproducts.
• has countable coproducts

  Since it has coproducts, we deduce that it has countable coproducts.
• 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 connected

  Since it has an initial object, we deduce that it is connected.
• has wide pushouts

  Since it has connected colimits, we deduce that it has wide pushouts.
• has filtered colimits

  Since it has wide pushouts, we deduce that it has filtered colimits.
• is Cauchy complete

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

  Since it has coequalizers and has countable coproducts, we deduce that it has sequential colimits.
• is complete

  Since it is essentially small and is thin and is cocomplete, we deduce that it is complete.
• is finitely cocomplete

  Since it is self-dual and is finitely complete, we deduce that it is finitely cocomplete.
• has a terminal object

  Since it is self-dual and has an initial object, we deduce that it has a terminal object.
• has products

  Since it is self-dual and has coproducts, we deduce that it has products.
• has finite products

  Since it is self-dual and has finite coproducts, we deduce that it has finite products.
• has binary products

  Since it is self-dual and has binary coproducts, we deduce that it has binary products.
• has countable products

  Since it is self-dual and has countable coproducts, we deduce that it has countable products.
• has equalizers

  Since it is self-dual and has coequalizers, we deduce that it has equalizers.
• has filtered limits

  Since it is self-dual and has filtered colimits, we deduce that it has filtered limits.
• has sequential limits

  Since it is self-dual and has sequential colimits, we deduce that it has sequential limits.
• has connected limits

  Since it is self-dual and has connected colimits, we deduce that it has connected limits.
• has pullbacks

  Since it is self-dual and has pushouts, we deduce that it has pullbacks.
• is left cancellative

  Since it is self-dual and is right cancellative, we deduce that it is left cancellative.
• has wide pullbacks

  Since it is self-dual and has wide pushouts, we deduce that it has wide pullbacks.
• is locally small

  Since it is small, we deduce that it is locally small.
• 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 a groupoid

  Since it is essentially discrete, we deduce that it is a groupoid.
• has a strict initial object

  Since it is left cancellative and has an initial object, we deduce that it has a strict initial object.
• has exact filtered colimits

  Since it is locally finitely presentable, we deduce that it has exact filtered colimits.
• is locally ℵ₁-presentable

  Since it is locally finitely presentable, we deduce that it is locally ℵ₁-presentable.
• is cartesian closed

  Since it is an elementary topos, we deduce that it is cartesian closed.
• has a subobject classifier

  Since it is an elementary topos, we deduce that it has a subobject classifier.
• has disjoint finite coproducts

  Since it is an elementary topos, we deduce that it has disjoint finite coproducts.
• is epi-regular

  Since it is an elementary topos, we deduce that it is epi-regular.
• is mono-regular

  Since it has a subobject classifier, we deduce that it is mono-regular.
• is additive

  Since it is abelian, we deduce that it is additive.
• is Grothendieck abelian

  Since it is abelian and has coproducts and has a generator and has exact filtered colimits, we deduce that it is Grothendieck abelian.
• is balanced

  Since it is mono-regular, we deduce that it is balanced.
• has a strict terminal object

  Since it is right cancellative and has a terminal object, we deduce that it has a strict terminal object.
• is preadditive

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

  Since it has coproducts and has disjoint finite coproducts, we deduce that it has disjoint coproducts.
• is distributive

  Since it is cartesian closed and has finite coproducts, we deduce that it is distributive.
• is infinitary distributive

  Since it is cartesian closed and has coproducts, we deduce that it is infinitary distributive.
• has zero morphisms

  Since it is preadditive, we deduce that it has zero morphisms.
• 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 skeletal

  The two objects are isomorphic, but different.

Deduced Non-Properties*

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

*This also uses the deduced properties.