Combinations script

[ScriptRaccoon]

When adding a new category (or a new functor, etc.) to the database, it is useful to see which combinations of properties are witnessed by the new structure but have not been witnessed before. Although the /missing page lists all consistent combinations that are not yet witnessed, it is cumbersome to manually check which combinations disappear after adding a new structure.

Therefore, this PR adds a new command-line script that lists all combinations of properties of the form $p \land \neg q$ that are witnessed by a given structure (or its dual), but by no other structure of the same type.

Of course, the results may change when other structures are added in the future. For example, currently the Stone-Cech-compactification functor is the only functor in the database that is a reflector but does not preserve binary products, but there are other examples too.

This script has been developed while working on #340, which adds a category witnessing many new combinations. The idea came already while working on #305 and #306, which added several functors to witness all consistent functor property combinations.

Usage

pnpm db:combinations <structure-id> <structure-type>

Examples

The category of groups

pnpm db:combinations Grp category

prints:

Unique witnessed combinations for category with ID "Grp":
- conormal ∧ ¬cogenerating set
- conormal ∧ ¬extremal cogenerating set

The dual category of topological spaces

In this case, the ID needs to be written in quotes.

pnpm db:combinations 'Top_*' category

prints:

Unique witnessed combinations for category with ID "Top_*":
- counital ∧ ¬ℵ₁-accessible
- CIP ∧ ¬extremal generating set
- CIP ∧ ¬extremal generator

The functor Q x - on topological spaces

pnpm db:combinations rational_product functor

prints:

Unique witnessed combinations for functor with ID "rational_product":
- preserves epimorphisms ∧ ¬preserves regular epimorphisms

The Stone-Cech-compactification functor

pnpm db:combinations stone-cech-compactification functor

prints:

Unique witnessed combinations for functor with ID "stone-cech-compactification":
- reflector ∧ ¬preserves binary products
- reflector ∧ ¬preserves finite products

The category of non-empty sets

This example shows that "weird" categories tend to witness many combinations.

pnpm db:combinations Setne category

prints:

Unique witnessed combinations for category with ID "Setne":
- products ∧ ¬cofiltered
- products ∧ ¬ℵ₁-cofiltered
- cartesian closed ∧ ¬cofiltered
- cartesian closed ∧ ¬coquotients of cocongruences
- cartesian closed ∧ ¬coreflexive equalizers
- cartesian closed ∧ ¬equalizers
- cartesian closed ∧ ¬finitely complete
- cartesian closed ∧ ¬pullbacks
- cartesian closed ∧ ¬ℵ₁-cofiltered limits
- mono-regular ∧ ¬coquotients of cocongruences
- mono-regular ∧ ¬effective cocongruences
- epi-regular ∧ ¬coquotients of cocongruences
- epi-regular ∧ ¬effective cocongruences
- finitely accessible ∧ ¬coquotients of cocongruences
- finitely accessible ∧ ¬ℵ₁-cofiltered limits
- generalized variety ∧ ¬coquotients of cocongruences
- generalized variety ∧ ¬ℵ₁-cofiltered limits
- parametrized natural numbers object ∧ ¬cofiltered
- parametrized natural numbers object ∧ ¬coquotients of cocongruences
- parametrized natural numbers object ∧ ¬countable copowers
- parametrized natural numbers object ∧ ¬countable coproducts
- parametrized natural numbers object ∧ ¬distributive
- parametrized natural numbers object ∧ ¬finite copowers
- parametrized natural numbers object ∧ ¬finite coproducts
- parametrized natural numbers object ∧ ¬initial object
- parametrized natural numbers object ∧ ¬multi-initial object
- parametrized natural numbers object ∧ ¬strict initial object
- parametrized natural numbers object ∧ ¬ℵ₁-cofiltered
- multi-complete ∧ ¬coquotients of cocongruences
- multi-complete ∧ ¬coreflexive equalizers
- multi-complete ∧ ¬ℵ₁-cofiltered limits
- natural numbers object ∧ ¬cofiltered
- natural numbers object ∧ ¬coquotients of cocongruences
- natural numbers object ∧ ¬initial object
- natural numbers object ∧ ¬multi-initial object
- natural numbers object ∧ ¬ℵ₁-cofiltered
- filtered-colimit-stable monomorphisms ∧ ¬coquotients of cocongruences
- filtered-colimit-stable monomorphisms ∧ ¬ℵ₁-cofiltered limits
- ℵ₁-accessible ∧ ¬coquotients of cocongruences
- ℵ₁-accessible ∧ ¬ℵ₁-cofiltered limits
- filtered colimits ∧ ¬coquotients of cocongruences
- filtered colimits ∧ ¬ℵ₁-cofiltered limits
- sifted colimits ∧ ¬coquotients of cocongruences
- sifted colimits ∧ ¬ℵ₁-cofiltered limits
- balanced ∧ ¬coquotients of cocongruences
- balanced ∧ ¬effective cocongruences
- ℵ₂-small products ∧ ¬cofiltered
- ℵ₂-small products ∧ ¬ℵ₁-cofiltered
- ℵ₁-filtered colimits ∧ ¬coquotients of cocongruences
- ℵ₁-filtered colimits ∧ ¬ℵ₁-cofiltered limits
- cartesian filtered colimits ∧ ¬cofiltered
- cartesian filtered colimits ∧ ¬coquotients of cocongruences
- cartesian filtered colimits ∧ ¬coreflexive equalizers
- cartesian filtered colimits ∧ ¬equalizers
- cartesian filtered colimits ∧ ¬finitely complete
- cartesian filtered colimits ∧ ¬pullbacks
- cartesian filtered colimits ∧ ¬ℵ₁-cofiltered limits
- directed colimits ∧ ¬coquotients of cocongruences
- directed colimits ∧ ¬ℵ₁-cofiltered limits
- countable products ∧ ¬cofiltered
- countable products ∧ ¬ℵ₁-cofiltered
- disjoint products ∧ ¬cofiltered
- disjoint products ∧ ¬finite copowers
- disjoint products ∧ ¬finite coproducts
- disjoint products ∧ ¬initial object
- disjoint products ∧ ¬multi-initial object
- disjoint products ∧ ¬ℵ₁-cofiltered
- wide pushouts ∧ ¬coquotients of cocongruences
- wide pushouts ∧ ¬coreflexive equalizers
- wide pushouts ∧ ¬ℵ₁-cofiltered limits
- connected colimits ∧ ¬coquotients of cocongruences
- connected colimits ∧ ¬coreflexive equalizers
- connected colimits ∧ ¬ℵ₁-cofiltered limits

The delooping of the ordinals

This is another example that shows that "weird" categories tend to witness many combinations.

pnpm db:combinations BOn category

prints:

Unique witnessed combinations for category with ID "BOn":
- cogenerating set ∧ ¬concretizable
- cogenerating set ∧ ¬locally essentially small
- cogenerator ∧ ¬concretizable
- cogenerator ∧ ¬locally essentially small
- core-connected ∧ ¬concretizable
- core-connected ∧ ¬essentially small
- core-connected ∧ ¬locally essentially small
- core-connected ∧ ¬locally small
- core-connected ∧ ¬regular-subobject-trivial
- core-connected ∧ ¬self-dual
- core-connected ∧ ¬small
- core-connected ∧ ¬well-powered
- core-thin ∧ ¬concretizable
- core-thin ∧ ¬locally essentially small
- core-thin ∧ ¬locally small
- extremal cogenerating set ∧ ¬concretizable
- extremal cogenerating set ∧ ¬locally essentially small
- extremal cogenerating set ∧ ¬well-powered
- extremal cogenerator ∧ ¬concretizable
- extremal cogenerator ∧ ¬locally essentially small
- extremal cogenerator ∧ ¬well-powered
- extremal generating set ∧ ¬concretizable
- extremal generating set ∧ ¬locally essentially small
- extremal generating set ∧ ¬well-powered
- extremal generator ∧ ¬concretizable
- extremal generator ∧ ¬locally essentially small
- extremal generator ∧ ¬well-powered
- gaunt ∧ ¬concretizable
- gaunt ∧ ¬locally essentially small
- gaunt ∧ ¬locally small
- generating set ∧ ¬concretizable
- generating set ∧ ¬locally essentially small
- generator ∧ ¬concretizable
- generator ∧ ¬locally essentially small
- left cancellative ∧ ¬concretizable
- left cancellative ∧ ¬locally essentially small
- left cancellative ∧ ¬locally small
- locally cartesian closed ∧ ¬concretizable
- locally cartesian closed ∧ ¬locally essentially small
- regular-quotient-trivial ∧ ¬concretizable
- regular-quotient-trivial ∧ ¬locally essentially small
- regular-quotient-trivial ∧ ¬locally small
- semi-strongly connected ∧ ¬concretizable
- semi-strongly connected ∧ ¬locally essentially small
- semi-strongly connected ∧ ¬locally small
- skeletal ∧ ¬concretizable
- skeletal ∧ ¬locally essentially small
- skeletal ∧ ¬locally small
- strongly connected ∧ ¬concretizable
- strongly connected ∧ ¬locally essentially small
- strongly connected ∧ ¬locally small
- strongly connected ∧ ¬well-powered
- well-copowered ∧ ¬concretizable
- well-copowered ∧ ¬locally essentially small

The category of topological spaces

Actually, most structures have no unique combinations. In this case, None is printed.

Unique witnessed combinations for category with ID "Top":
None