Download

List of tables

.tables

Schema of structures table

.schema structures

Number of categorical structures per type

SELECT type, COUNT(*) AS count
FROM structures
GROUP BY type;

Categories without an nLab link

SELECT id, name
FROM structures
WHERE type = 'category'
AND nlab_link IS NULL;

Structures involving rings

SELECT id, name, type
FROM structures
WHERE name LIKE '%ring%';

Finite categories

SELECT structure_id
FROM property_assignments
WHERE type = 'category'
AND property_id = 'finite'
AND is_satisfied = TRUE;

Categories without a generating set

SELECT structure_id
FROM property_assignments
WHERE type = 'category'
AND property_id = 'generating set'
AND is_satisfied = FALSE;

Abelian categories that are not cocomplete

SELECT a.structure_id
FROM property_assignments a
CROSS JOIN property_assignments b
WHERE a.type = 'category'
AND a.structure_id = b.structure_id
AND a.property_id = 'abelian'
AND a.is_satisfied = TRUE
AND b.property_id = 'cocomplete'
AND b.is_satisfied = FALSE;

Top 20 categories with the most unsatisfied properties

SELECT
    structure_id AS category,
    count(property_id) AS count
FROM property_assignments
WHERE is_satisfied = FALSE
AND type = 'category'
GROUP BY structure_id
ORDER BY count
DESC LIMIT 20;

Categories with unknown regular epimorphisms

SELECT s.id
FROM structures s
WHERE s.type = 'category'
AND NOT EXISTS (
    SELECT 1 FROM special_morphism_assignments a
    WHERE a.category_id = s.id
    AND a.type = 'regular epimorphisms'
);

Number of categories per tag

SELECT
    tag,
    COUNT(structure_id) AS tagged_categories
FROM structure_tag_assignments
WHERE type = 'category'
GROUP BY tag
ORDER BY tagged_categories DESC;

Properties without a dual

SELECT id, type
FROM properties
WHERE dual_property_id IS NULL;

Self-dual properties

SELECT id, type
FROM properties
WHERE id = dual_property_id;

Properties not invariant under equivalences

SELECT id, type
FROM properties
WHERE invariant_under_equivalences = FALSE;

Properties without related properties

SELECT p.id, p.type
FROM properties p
WHERE NOT EXISTS (
   SELECT 1 FROM related_properties r
   WHERE r.property_id = p.id
)
ORDER BY p.type;

Number of non-deduced implications per type

SELECT type, COUNT(*) AS count
FROM implications
WHERE is_deduced = FALSE
GROUP BY type;

Equivalent characterizations for categories

SELECT assumptions, conclusions
FROM implications_view
WHERE type = 'category'
AND is_equivalence = TRUE;

Top 5 implications of categories with the most assumptions

SELECT assumptions, conclusions
FROM implications_view
WHERE type = 'category'
ORDER BY json_array_length(assumptions)
DESC LIMIT 5;

Trivial proofs

SELECT structure_id, type, property_id, is_satisfied, proof
FROM property_assignments
WHERE proof = 'This is trivial.';

Top 10 longest proofs

SELECT structure_id, type, property_id, is_satisfied, length(proof)
FROM property_assignments
ORDER BY length(proof)
DESC LIMIT 10;

Top 10 properties with the most undecided categories

SELECT
    p.id AS property_id,
    COUNT(s.id) AS undecided_categories
FROM properties p
CROSS JOIN structures s
LEFT JOIN property_assignments pa
ON pa.structure_id = s.id
AND pa.property_id = p.id
WHERE p.type = 'category'
AND pa.property_id IS NULL
AND s.type = 'category'
GROUP BY p.id
ORDER BY undecided_categories
DESC LIMIT 10;

Properties which cannot be decided for a given structure

SELECT structure_id, type, property_id, proof
FROM property_assignments
WHERE is_satisfied IS NULL;

Functors with left adjoints

SELECT
    structure_id AS functor,
    associated_structure_id AS left_adjoint
FROM associated_structures
WHERE type = 'functor'
AND label = 'left_adjoint';

Symmetric monoidal categories with their underlying categories

SELECT
    structure_id AS symmetric_monoidal_category,
    associated_structure_id AS category
FROM associated_structures
WHERE type = 'symmetric_monoidal_category'
AND label = 'underlying_category';

Types of epimorphisms

SELECT property_id
FROM property_tag_assignments
WHERE type = 'morphism'
AND tag = 'types of epimorphisms';