CatDat

Implications of categories

Found 224 implications*

• abelian is equivalent to additive andcokernels andconormal andkernels andnormal
• abelian implies regular
• accessible andcomplete implies locally presentable
• accessible andpushouts implies well-copowered
• accessible implies Cauchy complete
• accessible implies generating set
• accessible implies locally essentially small
• accessible implies well-powered
• 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 copowers andleft cancellative implies thin
• binary coproducts andinhabited implies sifted
• binary products andcoreflexive equalizers implies equalizers
• binary products andequalizers implies pullbacks
• binary products andone-way implies thin
• binary products andpullbacks implies equalizers
• binary products implies binary powers
• biproducts andfiltered colimits implies cartesian filtered colimits
• biproducts andfinitely complete implies unital
• biproducts implies finite coproducts andfinite products andzero morphisms
• cartesian closed andcopowers implies powers
• cartesian closed andcoproducts implies infinitary distributive
• cartesian closed andcountable copowers implies countable powers
• cartesian closed andcountable coproducts implies countably distributive
• cartesian closed andfiltered colimits implies cartesian filtered colimits
• cartesian closed andfinite coproducts implies distributive
• cartesian closed andinitial object implies strict initial object
• cartesian closed andstrict terminal object implies thin
• cartesian closed implies finite products
• cartesian filtered colimits andcoproducts anddistributive implies infinitary distributive
• cartesian filtered colimits andcountable coproducts anddistributive implies countably distributive
• cartesian filtered colimits andthin implies exact filtered colimits
• cartesian filtered colimits implies filtered colimits andfinite products
• Cauchy complete andessentially finite implies finitely accessible
• Cauchy complete andessentially small implies accessible
• cocomplete andextensive andlocally cartesian closed implies infinitary extensive
• coequalizers andfinitely complete andlocally cartesian closed implies regular
• coequalizers andsemi-strongly connected implies filtered
• cofiltered limits andextensive andterminal object implies cocartesian cofiltered limits
• cofiltered limits andfinite powers implies powers
• cofiltered limits andfinite products implies products
• complete andessentially small andinfinitary distributive andthin implies cartesian closed
• complete andessentially small andthin implies cocomplete
• complete implies connected limits andfinitely complete
• complete is equivalent to equalizers andproducts
• complete implies multi-complete
• connected colimits implies sifted colimits
• connected limits is equivalent to equalizers andwide pullbacks
• connected andessentially discrete implies trivial
• connected andgroupoid implies strongly connected
• connected andmulti-terminal object is equivalent to terminal object
• connected implies inhabited
• coproducts andgenerating set andzero morphisms implies generator
• countable powers andessentially countable implies thin
• countable powers implies finite powers
• countable products andequalizers implies sequential limits
• countable products andessentially countable andthin implies products
• countable products implies countable powers andfinite products
• countable implies essentially countable
• countably distributive implies countable coproducts andfinite products
• countably distributive implies distributive
• countably distributive implies natural numbers object
• direct implies one-way andskeletal
• direct implies sequential limits
• directed colimits is equivalent to filtered colimits
• directed limits implies sequential limits
• discrete implies direct andessentially 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 andthin implies codistributive
• 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 andright cancellative implies thin
• equalizers andzero morphisms implies kernels
• equalizers implies Cauchy complete
• equalizers implies coreflexive equalizers
• essentially countable andthin implies ℵ₁-accessible
• essentially countable implies essentially small
• essentially discrete implies connected limits andlocally essentially small
• essentially discrete is equivalent to groupoid andthin
• essentially finite andfinite powers implies thin
• essentially finite andfinite products andthin implies products
• essentially finite andpullbacks implies wide pullbacks
• essentially finite implies essentially countable
• essentially small andpowers implies thin
• essentially small implies generating set andlocally essentially small andwell-copowered andwell-powered
• exact filtered colimits implies cartesian filtered colimits
• exact filtered colimits implies filtered colimits andfinitely complete
• extensive andfinite products implies distributive
• extensive implies disjoint finite coproducts andstrict initial object
• extensive implies finite coproducts
• filtered colimits andpullbacks andreflexive coequalizers implies sifted colimits
• filtered implies sifted
• finitary algebraic andpointed implies disjoint products
• finitary algebraic implies generator
• finitary algebraic implies locally strongly finitely presentable
• finitary algebraic implies well-copowered
• finite coproducts andmulti-complete implies complete
• finite coproducts andpreadditive implies finite products
• finite powers andsequential limits implies countable powers
• finite powers implies binary powers andterminal object
• finite products andinfinitary extensive implies infinitary distributive
• finite products andsequential limits implies countable products
• finite products andstrongly connected implies disjoint finite products
• finite products andthin implies natural numbers object
• finite products is equivalent to binary products andterminal object
• finite products implies finite powers
• finite andone-way andskeletal implies direct
• finite implies countable andessentially finite
• finitely accessible implies filtered colimits
• finitely accessible implies ℵ₁-accessible
• finitely cocomplete implies filtered
• 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
• generalized variety implies sifted colimits
• generalized variety implies ℵ₁-accessible
• 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 andinfinitary extensive andlocally presentable
• Grothendieck topos is equivalent to coproducts andelementary topos andgenerating set andlocally essentially small
• groupoid andmulti-terminal object implies thin
• groupoid andone-way implies thin
• 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 countably distributive
• infinitary extensive implies coproducts
• infinitary extensive implies extensive
• inhabited andthin andzero morphisms implies trivial
• 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
• initial object andstrongly connected andterminal object implies pointed
• kernels andpreadditive implies equalizers
• kernels implies zero morphisms
• left cancellative andsifted implies thin
• left cancellative andzero morphisms implies thin
• left cancellative implies Cauchy complete
• left cancellative implies coreflexive equalizers andreflexive coequalizers
• locally cartesian closed andterminal object implies cartesian closed
• locally cartesian closed implies pullbacks
• locally copresentable andlocally presentable implies essentially small
• locally essentially small andsubobject classifier implies well-powered
• locally finitely multi-presentable is equivalent to connected limits andfinitely accessible
• locally finitely multi-presentable is equivalent to finitely accessible andmulti-cocomplete
• locally finitely presentable is equivalent to cocomplete andfinitely accessible
• locally finitely presentable implies exact filtered colimits
• locally finitely presentable implies locally ℵ₁-presentable
• locally multi-presentable is equivalent to accessible andconnected limits
• locally multi-presentable is equivalent to accessible andmulti-cocomplete
• locally poly-presentable is equivalent to accessible andwide pullbacks
• locally presentable is equivalent to accessible andcocomplete
• locally small implies locally essentially small
• locally strongly finitely presentable is equivalent to cocomplete andgeneralized variety
• locally strongly finitely presentable implies locally finitely presentable
• locally strongly finitely presentable implies multi-algebraic
• locally strongly finitely presentable implies regular
• locally ℵ₁-presentable is equivalent to cocomplete andℵ₁-accessible
• locally ℵ₁-presentable implies locally presentable
• Malcev andpointed implies unital
• Malcev implies finitely complete
• mono-regular andpreadditive implies normal
• mono-regular andregular subobject classifier implies subobject classifier
• mono-regular implies balanced
• multi-algebraic is equivalent to generalized variety andmulti-cocomplete
• multi-algebraic implies locally finitely multi-presentable
• multi-complete implies multi-terminal object
• natural numbers object andpointed implies trivial
• natural numbers object andstrict terminal object implies one-way
• natural numbers object implies finite products
• normal implies mono-regular
• normal implies zero morphisms
• one-way andzero morphisms implies thin
• one-way implies reflexive coequalizers
• pointed andstrict initial object implies trivial
• pointed andsubobject classifier implies normal
• pointed is equivalent to initial object andzero morphisms
• powers implies countable powers
• preadditive implies locally essentially small andzero morphisms
• products implies countable products andfinite products andpowers
• pullbacks andterminal object implies binary products
• regular subobject classifier andstrict terminal object implies thin
• regular subobject classifier implies finitely complete
• regular implies finitely complete
• semi-strongly connected andthin implies locally cartesian closed
• semi-strongly connected implies connected
• sequential colimits implies Cauchy complete
• sifted colimits implies filtered colimits andreflexive coequalizers
• sifted implies connected
• small implies essentially small andlocally small
• split abelian implies abelian
• strict initial object implies initial object
• strongly connected andthin implies trivial
• strongly connected implies semi-strongly connected
• subobject classifier implies finitely complete andmono-regular
• subobject classifier implies regular subobject classifier
• terminal object andthin implies powers
• terminal object andwide pullbacks implies complete
• terminal object implies filtered
• thin implies binary powers
• thin implies equalizers andleft cancellative
• thin implies generating set andlocally essentially small andone-way
• 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
• ℵ₁-accessible implies accessible

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

Implications can be combined to yield longer, non-obvious deductions that are not explicitly listed above. For example, the listed implications imply that every inhabited groupoid with binary products is trivial.

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.