CatDat

List of implications

Found 141 implications*

• abelian is equivalent to additive andcoequalizers andepi-regular andequalizers andmono-regular
• abelian implies regular
• additive andfinitely complete implies Malcev
• additive andregular subobject classifier implies trivial
• additive implies biproducts
• additive is equivalent to finite products andpreadditive
• balanced andleft cancellative andright cancellative implies groupoid
• binary coproducts andleft cancellative implies thin
• binary products andequalizers implies pullbacks
• binary products andgroupoid andinhabited implies trivial
• binary products andinhabited implies connected
• binary products andpullbacks implies equalizers
• biproducts andfinitely complete andpointed implies unital
• biproducts implies disjoint finite coproducts
• biproducts implies finite coproducts andfinite products andzero morphisms
• cartesian closed andcoproducts implies infinitary distributive
• cartesian closed andfinite coproducts implies distributive
• cartesian closed andinitial object implies strict initial object
• cartesian closed andpointed implies trivial
• cartesian closed implies finite products
• cocomplete andextensive andlocally cartesian closed implies infinitary extensive
• coequalizers andfinitely complete andlocally cartesian closed implies regular
• coequalizers andleft cancellative implies thin
• cofiltered limits andfinite products implies products
• complete andessentially small andinfinitary distributive andthin implies cartesian closed
• complete andessentially small andthin implies cocomplete
• complete implies cofiltered limits andconnected limits andfinitely complete andwide pullbacks
• complete is equivalent to equalizers andproducts
• connected limits is equivalent to equalizers andwide pullbacks
• connected andessentially discrete implies trivial
• connected andgroupoid implies strongly connected
• connected implies inhabited
• coproducts anddistributive andexact filtered colimits implies infinitary distributive
• coproducts andgenerating set andzero morphisms implies generator
• countable products andequalizers implies sequential limits
• countable products implies finite products
• directed colimits is equivalent to filtered colimits
• directed limits implies sequential limits
• discrete implies essentially discrete andlocally small andskeletal
• disjoint coproducts is equivalent to coproducts anddisjoint finite coproducts
• disjoint finite coproducts andlocally cartesian closed implies extensive
• disjoint finite coproducts andstrict terminal object implies thin
• disjoint finite coproducts andthin implies trivial
• disjoint finite coproducts implies finite coproducts
• distributive implies finite coproducts andfinite products
• distributive implies strict initial object
• elementary topos andlocally essentially small implies well-copowered
• elementary topos is equivalent to cartesian closed andfinitely complete andsubobject classifier
• elementary topos implies co-Malcev
• elementary topos implies coregular
• elementary topos implies disjoint finite coproducts andepi-regular andfinitely cocomplete
• elementary topos implies locally cartesian closed
• equalizers andgroupoid implies thin
• equalizers implies Cauchy complete
• essentially discrete implies connected limits andlocally essentially small
• essentially discrete is equivalent to groupoid andthin
• essentially finite andfinite products implies products andthin
• essentially finite andpullbacks implies wide pullbacks
• essentially finite implies essentially small
• essentially small andproducts implies thin
• essentially small implies generating set
• essentially small implies locally essentially small andwell-copowered andwell-powered
• exact filtered colimits implies filtered colimits andfinitely complete
• extensive andfinite products implies distributive
• extensive implies disjoint finite coproducts
• extensive implies finite coproducts
• extensive implies strict initial object
• finitary algebraic andpointed implies disjoint products
• finitary algebraic implies generator
• finitary algebraic implies locally strongly finitely presentable
• finitary algebraic implies well-copowered
• finite coproducts andpreadditive implies finite products
• finite products andinfinitary extensive implies infinitary distributive
• finite products andsequential limits implies countable products
• finite products is equivalent to binary products andterminal object
• finite implies essentially finite andsmall
• finitely complete andright cancellative implies regular subobject classifier
• finitely complete andthin implies Malcev
• finitely complete andthin implies regular
• finitely complete is equivalent to equalizers andfinite products
• generator implies generating set andinhabited
• Grothendieck abelian andself-dual implies trivial
• Grothendieck abelian is equivalent to abelian andcoproducts andexact filtered colimits andgenerator
• Grothendieck abelian implies cogenerator
• Grothendieck abelian implies locally presentable
• Grothendieck topos implies cogenerator andlocally presentable
• Grothendieck topos is equivalent to coproducts andelementary topos andgenerating set andlocally essentially small
• Grothendieck topos implies infinitary extensive
• groupoid andinhabited andzero morphisms implies trivial
• groupoid andinitial object implies trivial
• groupoid implies directed limits andleft cancellative andmono-regular andpullbacks andself-dual andwell-powered
• groupoid implies locally cartesian closed
• infinitary distributive implies coproducts andfinite products
• infinitary distributive implies distributive
• infinitary extensive implies coproducts
• infinitary extensive implies extensive
• inhabited andthin implies generator
• inhabited andzero morphisms implies strongly connected
• initial object andleft cancellative implies strict initial object
• initial object andright cancellative implies strict initial object
• left cancellative andzero morphisms implies thin
• left cancellative implies Cauchy complete
• lextensive is equivalent to extensive andfinitely complete
• locally cartesian closed andterminal object implies cartesian closed
• locally cartesian closed implies pullbacks
• locally essentially small andsubobject 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 andself-dual implies thin
• locally presentable implies cocomplete andcomplete andgenerating set andlocally essentially small andwell-copowered andwell-powered
• locally small implies locally essentially small
• locally strongly finitely presentable implies locally finitely presentable
• locally strongly finitely presentable implies regular
• locally ℵ₁-presentable implies locally presentable
• Malcev andpointed implies unital
• Malcev implies finitely complete
• mono-regular andregular subobject classifier implies subobject classifier
• mono-regular implies balanced
• pointed andstrict initial object implies trivial
• pointed is equivalent to initial object andzero morphisms
• preadditive implies locally essentially small andzero morphisms
• products implies countable products andfinite products
• pullbacks andterminal object implies binary products
• regular subobject classifier andstrict terminal object implies thin
• regular subobject classifier implies finitely complete
• regular implies finitely complete
• small implies essentially small andlocally small
• split abelian implies abelian
• strict initial object implies initial object
• strongly connected andthin implies locally cartesian closed
• strongly connected implies connected
• subobject classifier andthin implies trivial
• subobject classifier implies finitely complete andmono-regular
• subobject classifier implies regular subobject classifier
• terminal object andwide pullbacks implies complete
• terminal object implies connected
• thin implies equalizers andleft cancellative
• trivial implies essentially discrete andessentially finite andfinitary algebraic andGrothendieck topos andself-dual andsplit abelian
• unital implies finitely complete andpointed
• wide pullbacks is equivalent to cofiltered limits andpullbacks

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