CatDat

Implications of categories

Found 251 implications*

• abelian is equivalent to additive andcokernels andconormal andkernels andnormal
• abelian implies regular
• accessible andcomplete is equivalent to 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 andeffective congruences implies normal
• 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
• Barr-exact is equivalent to effective congruences andregular
• binary copowers andleft cancellative implies thin
• binary coproducts andinhabited implies sifted
• binary powers andcore-thin implies thin
• binary products andcoreflexive equalizers implies equalizers
• binary products andequalizers implies pullbacks
• binary products andpullbacks implies equalizers
• binary products implies binary powers
• biproducts andfiltered colimits andfiltered-colimit-stable monomorphisms andproducts implies CIP
• 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 filtered colimits andfiltered-colimit-stable monomorphisms
• Cauchy complete andessentially finite implies finitely accessible
• Cauchy complete andessentially small implies accessible
• CIP implies coproducts andproducts andzero morphisms
• 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
• cofiltered-limit-stable epimorphisms andcountable coproducts andelementary topos implies trivial
• cokernels andkernels andpreadditive implies quotients of congruences
• 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
• core-thin andgroupoid implies thin
• core-thin implies effective congruences andquotients of congruences
• countable powers andessentially countable implies thin
• countable powers andlocally finite 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
• effective congruences andextensive implies mono-regular
• effective congruences andregular implies quotients of congruences
• elementary topos andlocally essentially small implies well-copowered
• elementary topos is equivalent to cartesian closed andfinitely complete andsubobject classifier
• elementary topos implies coregular
• elementary topos implies disjoint finite coproducts andeffective congruences andepi-regular andfinitely cocomplete
• elementary topos implies locally cartesian closed
• epi-regular andextensive andregular implies co-Malcev andeffective cocongruences
• epi-regular andregular andwell-powered implies well-copowered
• epi-regular andright cancellative implies subobject-trivial
• equalizers andright cancellative implies thin
• equalizers andsubobject-trivial 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 andlocally finite
• 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
• exact filtered colimits implies filtered-colimit-stable monomorphisms
• extensive andfinite products implies distributive
• extensive implies disjoint finite coproducts andstrict initial object
• extensive implies finite coproducts
• filtered colimits andleft cancellative implies filtered-colimit-stable monomorphisms
• filtered colimits andpullbacks andreflexive coequalizers implies sifted colimits
• filtered colimits andsubobject-trivial implies filtered-colimit-stable monomorphisms
• filtered implies sifted
• filtered-colimit-stable monomorphisms implies filtered colimits
• 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
• gaunt is equivalent to core-thin andskeletal
• 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 andexact filtered colimits andinfinitary extensive andlocally presentable
• Grothendieck topos is equivalent to coproducts andelementary topos andgenerating set andlocally essentially small
• groupoid andmulti-terminal object implies thin
• groupoid implies directed limits andleft cancellative andmono-regular andpullbacks andself-dual andwell-powered
• groupoid implies locally cartesian closed
• groupoid implies subobject-trivial
• 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 andstrongly connected andterminal object implies pointed
• kernels andnormal andpreadditive implies effective congruences
• 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 andeffective cocongruences andeffective congruences 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 finite implies locally essentially small
• locally finitely multi-presentable is equivalent to connected limits andfinitely accessible
• locally finitely multi-presentable implies filtered-colimit-stable monomorphisms
• 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 andsubobject classifier implies subobject-trivial
• Malcev implies finitely complete
• mono-regular andpreadditive implies normal
• mono-regular andregular subobject classifier implies subobject classifier
• mono-regular implies balanced
• multi-algebraic implies effective congruences
• 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 core-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 andquotients of congruences andregular implies cokernels
• preadditive implies locally essentially small andzero morphisms
• products implies countable products andpowers
• pullbacks andterminal object implies binary products
• reflexive coequalizers implies quotients of congruences
• 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
• subobject-trivial implies coreflexive equalizers andreflexive coequalizers
• subobject-trivial implies mono-regular
• terminal object andthin implies powers
• terminal object andwide pullbacks implies complete
• terminal object implies filtered
• thin implies binary powers
• thin implies equalizers andgenerating set andleft cancellative andlocally finite 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.