CatDat

Download

CatDat is built on a SQLite database. You can download a snapshot of it below and inspect the data in your terminal or with any database tool of your choice.

This is intended for advanced users. It is useful if you want to explore the data beyond what is available through the web application.

Example Queries

-- List of tables
.tables

-- Schema of structures table
.schema structures

-- Number of categories
SELECT COUNT(*) FROM categories;

-- 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;

-- 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 of categories without related properties
SELECT p.id FROM properties p
LEFT JOIN related_properties r
ON r.property_id = p.id
WHERE p.type = 'category' AND r.related_property_id IS NULL;

-- Equivalent characterizations
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, 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;