|
39 | 39 | .tables |
40 | 40 | </pre> |
41 | 41 |
|
42 | | -<pre>-- Schema of categories table |
43 | | -.schema categories |
| 42 | +<pre>-- Schema of structures table |
| 43 | +.schema structures |
44 | 44 | </pre> |
45 | 45 |
|
46 | 46 | <pre>-- Number of categories |
47 | 47 | SELECT COUNT(*) FROM categories; |
48 | 48 | </pre> |
49 | 49 |
|
50 | 50 | <pre>-- Categories without an nLab link |
51 | | -SELECT id, name FROM categories WHERE nlab_link IS NULL; |
| 51 | +SELECT id, name FROM structures |
| 52 | +WHERE type = 'category' AND nlab_link IS NULL; |
52 | 53 | </pre> |
53 | 54 |
|
54 | | -<pre>-- Categories involving rings |
55 | | -SELECT id, name FROM categories WHERE name LIKE '%ring%'; |
| 55 | +<pre>-- Structures involving rings |
| 56 | +SELECT id, name, type FROM structures WHERE name LIKE '%ring%'; |
56 | 57 | </pre> |
57 | 58 |
|
58 | 59 | <pre>-- Finite categories |
59 | | -SELECT category_id FROM category_property_assignments |
60 | | -WHERE property_id = 'finite' AND is_satisfied = TRUE; |
| 60 | +SELECT structure_id FROM property_assignments |
| 61 | +WHERE type = 'category' AND property_id = 'finite' |
| 62 | +AND is_satisfied = TRUE; |
61 | 63 | </pre> |
62 | 64 |
|
63 | 65 | <pre>-- Categories without a generating set |
64 | | -SELECT category_id FROM category_property_assignments |
65 | | -WHERE property_id = 'generating set' AND is_satisfied = FALSE; |
| 66 | +SELECT structure_id FROM property_assignments |
| 67 | +WHERE type = 'category' AND property_id = 'generating set' |
| 68 | +AND is_satisfied = FALSE; |
66 | 69 | </pre> |
67 | 70 |
|
68 | 71 | <pre>-- Abelian categories that are not cocomplete |
69 | | -SELECT a.category_id |
70 | | -FROM category_property_assignments a |
71 | | -CROSS JOIN category_property_assignments b |
72 | | -WHERE a.category_id = b.category_id |
| 72 | +SELECT a.structure_id |
| 73 | +FROM property_assignments a |
| 74 | +CROSS JOIN property_assignments b |
| 75 | +WHERE a.type = 'category' |
| 76 | +AND a.structure_id = b.structure_id |
73 | 77 | AND a.property_id = 'abelian' AND a.is_satisfied = TRUE |
74 | 78 | AND b.property_id = 'cocomplete' AND b.is_satisfied = FALSE; |
75 | 79 | </pre> |
76 | 80 |
|
77 | 81 | <pre>-- Number of categories per tag |
78 | | -SELECT tag, count(category_id) AS tagged_categories |
79 | | -FROM category_tag_assignments |
| 82 | +SELECT tag, count(structure_id) AS tagged_categories |
| 83 | +FROM structure_tag_assignments |
| 84 | +WHERE type = 'category' |
80 | 85 | GROUP BY tag |
81 | 86 | ORDER BY tagged_categories DESC; |
82 | 87 | </pre> |
83 | 88 |
|
84 | 89 | <pre>-- Properties without a dual |
85 | | -SELECT id FROM category_properties WHERE dual_property_id IS NULL; |
| 90 | +SELECT id, type FROM properties WHERE dual_property_id IS NULL; |
86 | 91 | </pre> |
87 | 92 |
|
88 | 93 | <pre>-- Self-dual properties |
89 | | -SELECT id FROM category_properties WHERE id = dual_property_id; |
| 94 | +SELECT id, type FROM properties WHERE id = dual_property_id; |
90 | 95 | </pre> |
91 | 96 |
|
92 | 97 | <pre>-- Properties not invariant under equivalences |
93 | | -SELECT id FROM category_properties WHERE invariant_under_equivalences = FALSE; |
| 98 | +SELECT id, type FROM properties WHERE invariant_under_equivalences = FALSE; |
94 | 99 | </pre> |
95 | 100 |
|
96 | | -<pre>-- Properties without related properties |
97 | | -SELECT p.id FROM category_properties p |
98 | | -LEFT JOIN related_category_properties r |
| 101 | +<pre>-- Properties of categories without related properties |
| 102 | +SELECT p.id FROM properties p |
| 103 | +LEFT JOIN related_properties r |
99 | 104 | ON r.property_id = p.id |
100 | | -WHERE r.related_property_id IS NULL; |
| 105 | +WHERE p.type = 'category' AND r.related_property_id IS NULL; |
101 | 106 | </pre> |
102 | 107 |
|
103 | | -<pre>-- Equivalences |
104 | | -SELECT assumptions, conclusions FROM category_implications_view |
105 | | -WHERE is_equivalence = TRUE; |
| 108 | +<pre>-- Equivalent characterizations |
| 109 | +SELECT assumptions, conclusions FROM implications_view |
| 110 | +WHERE type = 'category' AND is_equivalence = TRUE; |
106 | 111 | </pre> |
107 | 112 |
|
108 | | -<pre>-- Top 5 implications with the most assumptions |
109 | | -SELECT assumptions, conclusions FROM category_implications_view |
| 113 | +<pre>-- Top 5 implications of categories with the most assumptions |
| 114 | +SELECT assumptions, conclusions FROM implications_view |
| 115 | +WHERE type = 'category' |
110 | 116 | ORDER BY json_array_length(assumptions) DESC LIMIT 5; |
111 | 117 | </pre> |
112 | 118 |
|
113 | 119 | <pre>-- Trivial proofs |
114 | | -SELECT category_id, property_id, is_satisfied, proof |
115 | | -FROM category_property_assignments |
| 120 | +SELECT structure_id, type, property_id, is_satisfied, proof |
| 121 | +FROM property_assignments |
116 | 122 | WHERE proof = 'This is trivial.'; |
117 | 123 | </pre> |
118 | 124 |
|
119 | 125 | <pre>-- Top 10 longest proofs |
120 | | -SELECT category_id, property_id, is_satisfied, proof |
121 | | -FROM category_property_assignments |
| 126 | +SELECT structure_id, type, property_id, is_satisfied, proof |
| 127 | +FROM property_assignments |
122 | 128 | ORDER BY length(proof) DESC LIMIT 10; |
123 | 129 | </pre> |
124 | 130 |
|
125 | 131 | <pre>-- Top 10 properties with the most undecided categories |
126 | | -SELECT p.id AS property_id, COUNT(c.id) AS undecided_categories |
127 | | -FROM category_properties p |
128 | | -CROSS JOIN categories c |
129 | | -LEFT JOIN category_property_assignments pa |
130 | | -ON pa.category_id = c.id AND pa.property_id = p.id |
131 | | -WHERE pa.property_id IS NULL |
| 132 | +SELECT p.id AS property_id, COUNT(s.id) AS undecided_categories |
| 133 | +FROM properties p |
| 134 | +CROSS JOIN structures s |
| 135 | +LEFT JOIN property_assignments pa |
| 136 | +ON pa.structure_id = s.id AND pa.property_id = p.id |
| 137 | +WHERE p.type = 'category' AND pa.property_id IS NULL |
| 138 | +AND s.type = 'category' |
132 | 139 | GROUP BY p.id |
133 | 140 | ORDER BY undecided_categories DESC LIMIT 10; |
134 | 141 | </pre> |
135 | 142 |
|
136 | | -<pre>-- Properties which cannot be decided for a given category |
137 | | -SELECT category_id, property_id, proof |
138 | | -FROM category_property_assignments |
| 143 | +<pre>-- Properties which cannot be decided for a given structure |
| 144 | +SELECT structure_id, type, property_id, proof |
| 145 | +FROM property_assignments |
139 | 146 | WHERE is_satisfied IS NULL; |
140 | 147 | </pre> |
141 | 148 |
|
|
0 commit comments