CatDat

Properties

Properties from the database

• is locally small
• is a Grothendieck topos
• is locally finitely presentable

Deduced properties

• is locally essentially small

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

  Since it is locally finitely presentable, we deduce that it is locally presentable.
• 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 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.
• has a cogenerator

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

  Since it has a generator, we deduce that it is inhabited.
• 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.
• is connected

  Since it has an initial object, we deduce that it is connected.
• has filtered colimits

  Since it has exact filtered colimits, we deduce that it has filtered colimits.
• is finitely complete

  Since it has exact filtered colimits, we deduce that it is finitely complete.
• is well-powered

  Since it is locally presentable, we deduce that it is well-powered.
• is well-copowered

  Since it is locally presentable, we deduce that it is well-copowered.
• is complete

  Since it is locally presentable, we deduce that it is complete.
• is cocomplete

  Since it is locally presentable, we deduce that it is cocomplete.
• 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.
• is finitely cocomplete

  Since it is an elementary topos, we deduce that it is finitely cocomplete.
• 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.
• has finite products

  Since it is cartesian closed, we deduce that it has finite products.
• has a strict initial object

  Since it is cartesian closed and has an initial object, we deduce that it has a strict initial object.
• is mono-regular

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

  Since it is mono-regular, we deduce that it is balanced.
• has wide pushouts

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

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

  Since it is cocomplete, we deduce that it has coequalizers.
• has pushouts

  Since it has binary coproducts and has coequalizers, we deduce that it has pushouts.
• 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.
• has filtered limits

  Since it is complete, we deduce that it has filtered limits.
• has wide pullbacks

  Since it is complete, we deduce that it has wide pullbacks.
• has connected limits

  Since it is complete, we deduce that it has connected limits.
• has products

  Since it is complete, we deduce that it has products.
• has equalizers

  Since it is complete, we deduce that it has equalizers.
• has countable products

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

  Since it has coproducts and has disjoint finite coproducts, we deduce that it has disjoint coproducts.
• has sequential limits

  Since it has equalizers and has countable products, we deduce that it has sequential limits.
• 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.

Non-Properties

Non-Properties from the database

• does not have a strict terminal object
• is not skeletal

  trivial
• is not Malcev

Deduced Non-Properties*

• is not small

  Assume for a contradiction that it is small. Since it is small, we deduce that it is essentially small. Since it is essentially small and has products, we deduce that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
• does not have zero morphisms

  Assume for a contradiction that it has zero morphisms. Since it has zero morphisms and has an initial object, we deduce that it is pointed. 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. Since it is split abelian, we deduce that it is abelian. Since it is abelian, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
• is not preadditive

  Assume for a contradiction that it is preadditive. Since it is preadditive, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
• is not additive

  Assume for a contradiction that it is additive. Since it is additive, we deduce that it is preadditive. This is a contradiction since we already know that it is not preadditive.
• is not abelian

  Assume for a contradiction that it is abelian. Since it is abelian, we deduce that it is additive. This is a contradiction since we already know that it is not additive.
• is not pointed

  Assume for a contradiction that it is pointed. Since it is pointed, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
• is not self-dual

  Assume for a contradiction that it is self-dual. Since it is locally presentable and is self-dual, we deduce that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
• 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 essentially small

  Assume for a contradiction that it is essentially small. Since it is essentially small and has products, we deduce that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
• is not thin

  Assume for a contradiction that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
• 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 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 self-dual. This is a contradiction since we already know that it is not self-dual.
• is not Grothendieck abelian

  Assume for a contradiction that it is Grothendieck abelian. Since it is Grothendieck abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.
• 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 equalizers, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
• is not split abelian

  Assume for a contradiction that it is split abelian. Since it is split abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.

*This also uses the deduced properties.