Category implications

Found 269 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 andthin implies locally cartesian closed
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 countable andlocally finite implies ℵ₁-accessible
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 andcountable coproducts implies ℵ₁-filtered
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 products implies products
cofiltered-limit-stable epimorphisms andcountable coproducts andelementary topos implies trivial
cogenerating set anddisjoint coproducts implies cogenerator
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 copowers andℵ₁-filtered colimits implies copowers
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 andℵ₁-cofiltered limits 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 andℵ₁-filtered implies terminal object
essentially countable implies essentially small
essentially discrete implies connected limits andlocally essentially small
essentially discrete is equivalent to groupoid andthin
essentially finite andfiltered andthin implies terminal object
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 andgroupoid implies finitely accessible andgeneralized variety
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 andfinite copowers implies copowers
filtered colimits andleft cancellative implies filtered-colimit-stable monomorphisms
filtered colimits andleft cancellative implies sifted colimits
filtered colimits andpullbacks andreflexive coequalizers implies sifted colimits
filtered colimits andsubobject-trivial implies filtered-colimit-stable monomorphisms
filtered colimits implies ℵ₁-filtered colimits
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 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 andleft cancellative implies generalized variety
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 andmulti-complete implies complete
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 ℵ₂-small powers
preadditive andquotients of congruences andregular implies cokernels
preadditive implies locally essentially small andzero morphisms
pretopos is equivalent to Barr-exact andextensive
products implies powers
products implies ℵ₂-small products
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
terminal object implies ℵ₁-filtered
thin implies binary powers
thin implies equalizers andgenerating set andleft cancellative andlocally finite andone-way
trivial implies Grothendieck topos andessentially discrete andessentially finite andfinitary algebraic andself-dual andsplit abelian
unital implies finitely complete andpointed
wide pullbacks is equivalent to cofiltered limits andpullbacks
ℵ₁-accessible implies accessible andℵ₁-filtered colimits
ℵ₁-filtered colimits implies Cauchy complete
ℵ₁-filtered implies filtered
ℵ₂-small powers implies countable powers
ℵ₂-small products implies countable products andℵ₂-small powers

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

For results that do not quite fit the implication model, content pages are used instead.