Add Redundancy Tests

.github/workflows/test.yaml

@@ -33,3 +33,6 @@ jobs:
               run: |
                   pnpm db:setup:catdat
                   pnpm db:update
+
+            - name: Redundancy check
+              run: pnpm db:redundancies

CONTRIBUTING.md

@@ -110,7 +110,7 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **Reduce Unknowns**: Try to reduce the number of unknown properties of categories, in particular when adding a new category. Use the category detail page to see its unknown properties. Use the [page with missing data](https://catdat.app/missing) to identify categories with unknown properties. The same remarks apply to functors.
 
-- **Atomic Properties**: Only assign properties to a category or functor that cannot be deduced from other properties (satisfied or not). For example, if a category is complete, add the property "complete", but do not add "terminal object". The application infers this property automatically.
+- **Avoid redundant assignments**: Only assign properties (satisfied or not) to a category or functor if they cannot be deduced from other assignments. For example, if a category is complete, record that it is complete, but do not also record that it has a terminal object; the application infers this automatically. Redundant assignments can be identified using the redundancy script described below.
 
 - **No dual categories**: Instead of adding the dual of a category already in the database, consider adding properties to the original category (use the corresponding dual properties).
 
@@ -138,6 +138,26 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **New Combinations**: Add new categories that satisfy combinations of satisfied properties and unsatisfied properties and not yet in the database. For example, you may add a category that is abelian but neither cocomplete nor essentially small (if it is not already present). The [page with missing data](https://catdat.app/missing) lists consistent combinations of the form $p \land \neg q$ that are not yet witnessed by a category in the database. The same remarks apply to functors.
 
+### Redundancy Script
+
+As noted above, avoid redundant property assignments to a category. To detect redundancies, run `pnpm db:redundancies`.
+
+The script reports at most one redundant assignment per category for each of satisfied and unsatisfied properties, even if multiple exist. After removing an assignment, run the script again to ensure that all remaining redundancies are handled.
+
+Removing redundant assignments is not required, but it is recommended, especially for all unsatisfied properties. For satisfied properties, removal depends on context: keep them if the proof is meaningful, otherwise consider removing them if it is purely technical or uninformative.
+
+In particular, it often makes sense to **keep** a redundant assignment of a satisfied property in the following cases:
+
+- The proof for the property is straight forward anyway (e.g. showing that a category is pointed).
+- The proof provides useful insight.
+- The proof constructs objects (especially limits or colimits) that are used later.
+- Removing the assignment would lead to an overly complex deduction generated by _CatDat_.
+- The proof establishes an intermediate result that is used as an assumption in a later argument.
+
+For example, you may first prove that a category has zero morphisms, and then prove that it is normal. Although the database contains the implication "normal => zero morphisms", in practice the latter is used as a prerequisite. Similarly, when proving that a category is extensive, it is often clearer to first show that finite coproducts exist, rather than relying on the implication "extensive => finite coproducts". Also, an explicit description of finite coproducts is useful for deciding other properties involving coproducts.
+
+Every redundant assignment of a satisfied property that is intentionally kept must be explicitly marked to skip the redundancy check. See `N.sql` for an example.
+
 ### Keep Pull Requests Focused
 
 Please keep each pull request limited in scope. Large pull requests are harder to review, more likely to conflict with ongoing changes on the main branch, and more difficult to merge cleanly.

DATABASE.md

@@ -33,6 +33,7 @@ Further tables are:
 - `special_morphisms`
 - `related_category_properties`
 - `category_comments`
+- `category_property_comments`
 - `lemmas` (a flexible variant of implications)
 
 For functors there are similar tables, such as:
@@ -64,11 +65,15 @@ Use `pnpm db:update` to run all the commands in sequence: `pnpm db:seed`,`pnpm d
 
 Use `pnpm db:watch` to run this command automatically every time a file in the subfolder [/databases/catdat/data](/databases/catdat/data) changes. This is useful in particular during development.
 
+## Redundancies
+
+There is another script that intentionally does not run with each update: `pnpm db:redundancies` checks for redundant assignments of properties to categories.
+
 ## Diagram
 
 This is the database schema as of 24.04.2026; changes may occur.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/f315b67e-1bb1-4e93-970a-1e5288dba60e" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/411f9d8a-c28b-4d8f-919c-0ff2aad6a989" />
 
 ## Application Database
 

databases/catdat/data/001_categories/100_related-categories.sql

@@ -43,8 +43,10 @@ VALUES
 ('Delta', 'walking_coreflexive_pair'),
 ('FI', 'B'),
 ('FI', 'FS'),
+('FI', 'FinSet'),
 ('FS', 'B'),
 ('FS', 'FI'),
+('FS', 'FinSet'),
 ('FinAb', 'Ab'),
 ('FinAb', 'Ab_fg'),
 ('FinAb', 'FinGrp'),
@@ -55,6 +57,8 @@ VALUES
 ('FinSet', 'Set'),
 ('FinSet', 'Set_c'),
 ('FinSet', 'Set_f'),
+('FinSet', 'FI'),
+('FinSet', 'FS'),
 ('Fld', 'CRing'),
 ('FreeAb', 'Ab'),
 ('FreeAb', 'TorsFreeAb'),

databases/catdat/data/003_category-property-assignments/Ab_fg.sql

@@ -53,18 +53,6 @@ VALUES
 	FALSE,
 	'The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split.'
 ),
-(
-	'Ab_fg',
-	'countable powers',
-	FALSE,
-	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \IZ \times P$. Tensoring with $\IQ$ yields an isomorphism of finite-dimensional vector spaces $P_{\IQ} \cong \IQ \times P_{\IQ}$, which is impossible: the dimension $d$ of $P_{\IQ}$ (i.e. the rank of $P$) would satisfy $d = 1+d$.'
-),
-(
-	'Ab_fg',
-	'countable copowers',
-	FALSE,
-	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \IZ \oplus P$. Tensoring with $\IQ$ yields an isomorphism of finite-dimensional vector spaces $C_{\IQ} \cong \IQ \oplus C_{\IQ}$, which is impossible: the dimension $d$ of $C_{\IQ}$ (i.e. the rank of $C$) would satisfy $d = 1+d$.'
-),
 (
 	'Ab_fg',
 	'skeletal',

databases/catdat/data/003_category-property-assignments/BN.sql

@@ -35,12 +35,6 @@ VALUES
 	TRUE,
 	'The unique object is a generator for trivial reasons.'
 ),
-(
-	'BN',
-	'pullbacks',
-	TRUE,
-	'For natural numbers $n,m$ we need to find a universal pair $p,q$ of natural numbers satisfying $n + p = m + q$. We may assume w.l.o.g. $n \leq m$. Then take $p = m-n$, $q = 0$.'
-),
 (
 	'BN',
 	'left cancellative',
@@ -59,18 +53,6 @@ VALUES
 	TRUE,
 	'The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, <a href="/category-implication/sequential_implies_lcc">hence</a> cartesian closed.'
 ),
-(
-	'BN',
-	'essentially finite',
-	FALSE,
-	'This is trivial.'
-),
-(
-	'BN',
-	'thin',
-	FALSE,
-	'This is trivial.'
-),
 (
 	'BN',
 	'sequential limits',

databases/catdat/data/003_category-property-assignments/BOn.sql

@@ -47,12 +47,6 @@ VALUES
 	TRUE,
 	'This is because $0$ is the only ordinal number with an additive inverse.'
 ),
-(
-	'BOn',
-	'pullbacks',
-	TRUE,
-	'If $\alpha,\beta$ are ordinals, w.l.o.g. $\alpha \leq \beta$, choose $\delta$ with $\beta = \alpha + \delta$. Then the pair $\delta,0$ is a pullback of $\alpha,\beta$: We have $\alpha + \delta = \beta + 0$, and if $\epsilon_1,\,\epsilon_2$ is a pair of ordinals with $\alpha + \epsilon_1 = \beta + \epsilon_2$, we may cancel $\alpha$ to get $\epsilon_1 = \delta + \epsilon_2$, so that the pair factors as $\delta + \epsilon_2,\, 0 + \epsilon_2$.'
-),
 (
 	'BOn',
 	'cofiltered limits',
@@ -77,30 +71,12 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'BOn',
-	'terminal object',
-	FALSE,
-	'This is trivial.'
-),
-(
-	'BOn',
-	'right cancellative',
-	FALSE,
-	'Since $1 + \omega = 0 + \omega$, the ordinal $\omega$ is not an epimorphism. In fact, the epimorphisms are exactly the finite ordinals (see below).'
-),
 (
 	'BOn',
 	'balanced',
 	FALSE,
 	'Every finite ordinal is both a mono- and an epimorphism (see below), but only $0$ is an isomorphism.'
 ),
-(
-	'BOn',
-	'binary powers',
-	FALSE,
-	'Assume that the unique object has a product with itself. This amounts to a pair of ordinals $\pi_1,\pi_2$ such that for every pair of ordinals $\alpha_1,\alpha_2$ there is a unique ordinal $\tau$ with $\pi_i + \tau = \alpha_i$ for $i = 1,2$. Applying this to $\alpha_i = 0$ we get $\pi_i = 0$. Now we get a contradiction for any distinct $\alpha_1,\alpha_2$.'
-),
 (
 	'BOn',
 	'well-powered',

databases/catdat/data/003_category-property-assignments/Ban.sql

@@ -94,4 +94,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ <i>and</i> $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Ban'
+AND property_id IN ('pointed');

databases/catdat/data/003_category-property-assignments/CAlg(R).sql

@@ -88,4 +88,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see <a href="https://math.stackexchange.com/questions/2391187" target="_blank">MSE/2391187</a>.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CAlg(R)'
+AND property_id IN ('strict terminal object');

databases/catdat/data/003_category-property-assignments/CMon.sql

@@ -29,12 +29,6 @@ VALUES
 	TRUE,
 	'This follows from the explicit construction of coproducts and products.'
 ),
-(
-	'CMon',
-	'preadditive',
-	FALSE,
-	'In categories with finite products and finite coproducts, the preadditive structure <a href="/lemma/preadditive_structure_unique">is unique</a> if it exists. In the case of $\CMon$, this is just the pointwise addition of maps. This is indeed an enrichment of $\CMon$ over itself, but not over $\Ab$, since for example $\Hom(\IN,\IN) \cong \IN$ (with respect to addition) is not a group.'
-),
 (
 	'CMon',
 	'balanced',
@@ -88,4 +82,10 @@ VALUES
 	'CSP',
 	FALSE,
 	'First of all, epimorphisms in $\CMon$ are preserved and reflected by the forgetful functor to $\Mon$ (see below). Furthermore, if $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see <a href="https://mathoverflow.net/questions/510431/" target="_blank">MO/510431</a>). This implies that in $\CMon$ the canonical homomorphism $\bigoplus_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CMon'
+AND property_id IN ('pointed');

databases/catdat/data/003_category-property-assignments/CRing.sql

@@ -89,3 +89,9 @@ VALUES
 	FALSE,
 	'For a prime $p$ consider the sequence of projections $\cdots \to \IZ/p^2 \to \IZ/p$ and the constant sequence $\cdots \to \IZ \to \IZ$. The surjective homomorphisms $\IZ \to \IZ/p^n$ induce the homomorphism $\IZ \to \IZ_p$ in the limit, where $\IZ_p$ is the ring of $p$-adic integers. It is not surjective since $\IZ_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use <a href="https://stacks.math.columbia.edu/tag/04W0" target="_blank">SP/04W0</a> to conclude that it is no epimorphism in $\CRing$.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CRing'
+AND property_id IN ('strict terminal object');

databases/catdat/data/003_category-property-assignments/Delta.sql

@@ -99,18 +99,6 @@ VALUES
     FALSE,
     'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ have a common left inverse, the unique map $s^0 : [1] \to [0]$, but are not equalized by any morphism.'
 ),
-(
-	'Delta',
-	'binary powers',
-	FALSE,
-	'The <a href="/category/FinOrd">proof for $\FinOrd$</a> also works for $\FinSet \setminus \{\varnothing\}$: The forgetful functor to $\Set$ is representable, hence preserves all limits. Thus, if the power $\{0 < 1\} \times \{0 < 1\}$ exists in $\FinOrd \setminus \{\varnothing\}$, we may assume its underlying set is the cartesian product and the projection morphisms are the usual projection maps. Moreover, these maps are order-preserving. Since the result must be a total order, we have $(0,1) \leq (1,0)$ or $(1,0) \leq (0,1)$. In the first case, apply $p_2$ to get $1 \leq 0$, a contradiction. In the second case, use $p_1$ to get a contradiction.'
-),
-(
-	'Delta',
-	'binary copowers',
-	FALSE,
-	'The <a href="/category/FinOrd">proof for $\FinOrd$</a> also works for $\FinSet \setminus \{\varnothing\}$: Assume that the copower $1+1$, i.e. the coproduct of two terminal objects exists, denoted $\{x\}$ and $\{y\}$. If $x \leq y$ holds in the coproduct, then the universal property would imply this relation for all pairs of elements in any non-empty finite order, which is absurd. Otherwise, $y \leq x$ holds in the coproduct, which yields the same contradiction.'
-),
 (
     'Delta',
     'sequential colimits',
@@ -123,12 +111,6 @@ VALUES
     FALSE,
     'We can just copy the <a href="/category/FinOrd">proof for $\FinOrd$</a> to show that the sequence of truncations $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has no limit.'
 ),
-(
-    'Delta',
-    'essentially finite',
-    FALSE,
-    'The set $\IN$ is not finite.'
-),
 (
     'Delta',
     'pushouts',

databases/catdat/data/003_category-property-assignments/FI.sql

@@ -11,12 +11,6 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\FI \to \Set$ and $\Set$ is locally small.'
 ),
-(
-	'FI',
-	'initial object',
-	TRUE,
-	'Take the empty set.'
-),
 (
 	'FI',
 	'left cancellative',
@@ -89,12 +83,6 @@ VALUES
 	FALSE,
 	'Let $X_n := \{1,\dotsc,n\}$. Assume the sequence of inclusion maps $X_n \hookrightarrow X_{n+1}$ has a colimit $(f_n : X_n \to X)$ in this category. But $f_n$ must be an injective map, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.'
 ),
-(
-	'FI',
-	'essentially finite',
-	FALSE,
-	'This is trivial.'
-),
 (
 	'FI',
 	'skeletal',

databases/catdat/data/003_category-property-assignments/FS.sql

@@ -83,12 +83,6 @@ VALUES
 	FALSE,
 	'The connected component of non-empty sets has a terminal object, $1$, and it suffices to prove that it has no products. Let $X$ be a finite set with more than $1$ element. Assume that the product $P$ of $X$ with itself exists. The diagonal $X \to P$ is a split monomorphism, hence injective, but also surjective, i.e. an isomorphism. In other words, the two projections $P \rightrightarrows X$ are equal. The universal property of $P$ now implies that every two morphisms $Y \rightrightarrows X$ are equal, which is absurd.'
 ),
-(
-	'FS',
-	'essentially finite',
-	FALSE,
-	'This is trivial.'
-),
 (
 	'FS',
 	'skeletal',

databases/catdat/data/003_category-property-assignments/FinAb.sql

@@ -53,12 +53,6 @@ VALUES
 	FALSE,
 	'The sequence $0 \to \IZ/2 \to \IZ/4 \to \IZ/2 \to 0$ does not split.'
 ),
-(
-	'FinAb',
-	'countable powers',
-	FALSE,
-	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \IZ/2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.'
-),
 (
 	'FinAb',
 	'skeletal',

databases/catdat/data/003_category-property-assignments/FinGrp.sql

@@ -23,12 +23,6 @@ VALUES
 	TRUE,
 	'The underlying set of a finite structure can be chosen to be a subset of $\IN$.'
 ),
-(
-	'FinGrp',
-	'epi-regular',
-	TRUE,
-	'This holds since every epimorphism is surjective (see below), and a surjective homomorphism $A \to B$ is the coequalizer of its kernel pair $A \times_B A \rightrightarrows A$.'
-),
 (
 	'FinGrp',
 	'mono-regular',
@@ -107,12 +101,6 @@ VALUES
 	FALSE,
 	'If $A,B$ are finite groups whose orders are coprime, then we know that $\Hom(A,B)$ is trivial. But a generator would admit a non-trivial homomorphism to any other non-trivial finite group.'
 ),
-(
-	'FinGrp',
-	'countable powers',
-	FALSE,
-	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong C_2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.'
-),
 (
 	'FinGrp',
 	'sequential colimits',
@@ -125,3 +113,9 @@ VALUES
 	FALSE,
 	'This is trivial.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'FinGrp'
+AND property_id IN ('pointed');