Check for redundant implications

CLAUDE.md

@@ -42,7 +42,7 @@ Database (all scripts run with `tsx` and are type-checked by `pnpm check` via th
 - `pnpm db:setup`: delete `database/catdat.db` and recreate it from the SQL schema files. It also stores a hash of the schema in `database/schema/schema.json`. Required after any schema change; `db:seed` aborts if the schema hash is outdated.
 - `pnpm db:seed`: clear all data and insert the entries parsed from the YAML files (validated with `valibot` schemas in `database/scripts/utils/seed.schemas.ts`).
 - `pnpm db:deduce`: for each structure type, dualize implications and deduce satisfied and unsatisfied properties (for categories also special objects and morphisms). Deduced rows are marked with `is_deduced`, and those inherited from a parent structure additionally with `is_inherited`.
-- `pnpm db:test`: check data quality: properties and their duals are mutual, categories and their duals are mutual, `1`, `id_Set`, and `1_tensor` have no unsatisfied properties (positivity), all properties are decided for the structures listed in `database/scripts/decided-structures/`, the properties of selected structures exactly match their JSON files in `expected-data/`, adjoint functors are recorded on both sides with matching domains and codomains, links in proofs point to existing entries, all entries of the history file exist, and no property assignment can be deduced from others or inherited from the parent structure (except those marked with `check_redundancy: false`). The redundancy test runs last and lists all redundancies, at most one per structure and kind (satisfied or unsatisfied).
+- `pnpm db:test`: check data quality: properties and their duals are mutual, categories and their duals are mutual, `1`, `id_Set`, and `1_tensor` have no unsatisfied properties (positivity), all properties are decided for the structures listed in `database/scripts/decided-structures/`, the properties of selected structures exactly match their JSON files in `expected-data/`, adjoint functors are recorded on both sides with matching domains and codomains, links in proofs point to existing entries, all entries of the history file exist, no implication follows from the others (not even one conclusion or one direction of an equivalence), and no property assignment can be deduced from others or inherited from the parent structure (both except those marked with `check_redundancy: false`). The redundancy tests run last and list all redundancies: one line per implication, and at most one per structure and kind (satisfied or unsatisfied) for assignments.
 - `pnpm db:sort`: sort the arrays in the JSON files in `expected-data/` and `decided-structures/` alphabetically and format them with Prettier.
 - `pnpm db:snapshot`: copy the database to `static/databases/catdat-snapshot.db` for the download page.
 - `pnpm db:update`: run `db:sort`, `db:seed`, `db:deduce`, `db:test`, and `db:snapshot` in sequence. **This is the standard command after editing any YAML data.** It also runs in the test workflow in CI. Use `--watch` to rerun it whenever a file in `database/data/` changes.
@@ -65,7 +65,7 @@ Main tables (full schema in [database/schema/](database/schema/)):
 - `structure_associations` / `associated_structures`: typed links between structures, e.g. a functor's `domain`, `codomain`, `left_adjoint`, `right_adjoint`, a morphism's `category`, or a symmetric monoidal category's `underlying_category`.
 - `properties`: primary key `(id, type)`, with a `relation` ("is", "has", "preserves", ...), `description`, `dual_property_id`, and `invariant_under_equivalences`.
 - `property_assignments`: links structures to properties with `is_satisfied` (TRUE, FALSE, or NULL for undecidable), `proof`, `is_deduced`, `is_inherited` (deduced from the parent structure), `check_redundancy`, and an optional `label`. Proofs can cite labeled assignments, recorded in `proof_references`.
-- `implications`, `assumptions`, `conclusions`: implications between properties of one type, with `is_equivalence`, `is_deduced`, and `dual_implication_id`. The `implications_view` view combines them into JSON arrays.
+- `implications`, `assumptions`, `conclusions`: implications between properties of one type, with `is_equivalence`, `is_deduced`, `check_redundancy`, and `dual_implication_id`. The `implications_view` view combines them into JSON arrays.
 - `associated_assumptions`: implication assumptions about associated structures, e.g. a functor implication that requires the domain category to be complete.
 - `special_objects` / `special_object_assignments` and `special_morphisms` / `special_morphism_assignments` / `special_morphism_rules`: special objects (terminal, initial, products, coproducts) and special morphisms (isos, monos, epis, regular monos and epis) of categories.
 - Additional tables: tags (`structure_tags`, `property_tags`, and their assignment tables), `related_structures`, `related_properties`, `structure_comments`, `structure_keywords`, `property_keywords`, `relations`.
@@ -80,7 +80,7 @@ Use existing files as templates: [database/data/categories/N.yaml](database/data
 - Use single quotes for values that contain `:`, and escape a literal single quote as `''`.
 - Use `>-` for multiline text; an empty line in it starts a new paragraph when rendered. Do not use `|-`.
 - Optional `keywords` (list of strings) on structures and properties: alternative names a user would search for that do not already occur in the `name` (for properties: the ID), e.g. `posets` for `Pos`, `aleph1-accessible` for `ℵ₁-accessible` (no special characters needed), or `tripleable` for `monadic`. Only terms that identify the structure or property, not related concepts. The search filters on the list pages match them.
-- Set `check_redundancy: false` on a property assignment that is redundant but deliberately kept (see below).
+- Set `check_redundancy: false` on a property assignment or implication that is redundant but deliberately kept (see below).
 
 ## Contribution guidelines
 
@@ -89,7 +89,7 @@ Full guidelines: [CONTRIBUTING.md](CONTRIBUTING.md). Contributions come in throu
 - **Proofs for every claim**: satisfied and unsatisfied properties, implications, and special morphisms all need a proof or reference. If a proof refers to another proof, make the link explicit with labels and references. Put reusable lemmas and proofs that require lemmas into a `content/` page and link to it; long proofs alone are fine in the YAML files.
 - **Reduce unknowns**: when adding a structure, decide as many of its properties as possible. When adding a property, try to decide it for all existing structures, and include implications connecting it to existing properties. For the structures in `database/scripts/decided-structures/`, deciding every property is mandatory (enforced by `db:test`).
 - **No redundant assignments**: only assign properties that cannot be deduced or inherited from the parent structure. Redundant satisfied assignments may be kept when the proof is trivial anyway, insightful, constructs (co)limits used later, avoids an overly complex automatic deduction, or establishes an intermediate result used later. Mark them with `check_redundancy: false`. Redundant unsatisfied assignments are almost always removed. All other redundant assignments must be removed, since `db:test` reports them as errors.
-- **Atomic implications**: do not add implications that follow from others, and do not add dual implications, since dualization is automatic. Prefer the "limit" variant over the "colimit" variant. When adding an implication, check whether it simplifies existing ones.
+- **Atomic implications**: do not add implications that follow from others, and do not add dual implications, since dualization is automatic. Prefer the "limit" variant over the "colimit" variant. When adding an implication, check whether it simplifies existing ones. `db:test` reports implications that follow from others; keep one only if it states a definition or if removing it would lead to an overly complex automatic deduction (e.g. `ccc_no_strict_terminal`), and mark it with `check_redundancy: false`.
 - **Positive properties only**: never add negated properties (e.g. "large" for "not small"); record them as unsatisfied instead. Every category property must hold for the trivial category, and every functor property must hold for identity functors.
 - **Counterexamples**: every new property needs at least one structure that does not satisfy it. If none exists yet, add one.
 - **No duplicates**: do not add the dual of an existing category (assign the dual properties to the original instead), and do not add categories equivalent or isomorphic to existing ones, except when this matters for non-invariant properties such as being skeletal.
@@ -135,5 +135,5 @@ Format:
 
 1. Edit the YAML files in `database/data/` (or the `content/` pages).
 2. Run `pnpm db:update`, or `pnpm db:text` for text-only changes to existing structures, properties, and implications. If the schema changed, run `pnpm db:setup` first.
-3. If `db:update` fails, the cause is usually malformed YAML or a schema validation error, a contradiction found during deduction, a failing data-quality test, or a redundant assignment.
+3. If `db:update` fails, the cause is usually malformed YAML or a schema validation error, a contradiction found during deduction, a failing data-quality test, or a redundant assignment or implication.
 4. Run `pnpm cspell`.

CONTRIBUTING.md

@@ -88,7 +88,7 @@ The `pnpm db:test` command runs several tests to ensure the data behaves as expe
 6. Adjoint functors are recorded on both sides (left and right adjoint), and their domains and codomains match.
 7. All links in proofs point to existing structures, properties, implications, and content pages.
 8. Every entry of the history file [history.json](/shared/history.json) exists. When you rename a structure or property, rename it in the history file as well (new entries are added automatically by `pnpm db:seed`).
-9. There are no redundant property assignments (see [below](#redundant-assignments)).
+9. There are no redundant property assignments (see [below](#redundant-assignments)) and no redundant implications (see [below](#redundant-implications)).
 
 When you add a property to the JSON files in these two folders, you can insert it anywhere: `pnpm db:update` sorts them alphabetically.
 
@@ -130,7 +130,7 @@ When contributing new data (categories, functors, properties, implications, etc.
 
 - **Proofs for claims**: Provide proofs for all new claims (satisfied properties, unsatisfied properties, implications, special morphisms).
 
-- **Atomic implications**: Do not add implications that can be deduced from others. For example, do not add "complete => finite products" since it can be deduced from "complete => finitely complete" and "finitely complete => finite products". These are combined automatically.
+- **Atomic implications**: Do not add implications that can be deduced from others. For example, do not add "complete => finite products" since it can be deduced from "complete => finitely complete" and "finitely complete => finite products". These are combined automatically. This also applies to single conclusions of an implication and to single directions of an equivalence. Redundant implications are reported by `pnpm db:test`, see below.
 
 - **No dual implications**: Implications are dualized automatically when applicable. For this reason, adding the category implication "finitely cocomplete => pushouts" is not necessary when "finitely complete => pullbacks" has already been added. Similarly, the functor implication "comonadic => left adjoint" is automatically dualized from "monadic => right adjoint". When an implication can be phrased in either a "limit" or a "colimit" variant, prefer the "limit" variant (unless the literature focusses on the "colimit" variant).
 
@@ -160,6 +160,19 @@ For example, you may first prove that a category has zero morphisms, and then pr
 
 Every redundant assignment that is intentionally kept must be explicitly marked to skip the redundancy check. See [`Man.yaml`](/database/data/categories/Man.yaml) for an example.
 
+### Redundant implications
+
+As noted above, implications should be atomic. `pnpm db:test` reports an implication if one of its conclusions (or one direction of an equivalence) can be deduced from the other implications.
+
+Redundant implications must be removed, or, if they are deliberately kept, marked with `check_redundancy: false`. Usually, removal is the right choice, since _CatDat_ combines implications automatically. It makes sense to **keep** a redundant implication in the following cases:
+
+- It states a definition or a standard characterization from the literature, even if one of its conclusions follows from the others.
+- Removing it would lead to an overly complex deduction, typically when the deduction needs a long chain or a detour through unrelated notions, while the implication has a short direct proof.
+
+For example, the implication "cartesian closed + strict terminal object => thin" can be deduced via natural numbers objects, one-way categories, and core-thin categories. Its direct proof takes three lines, and it is used for many deductions, such as that **Set** has no strict terminal object. Without it, these deductions would go through the long chain.
+
+Every redundant implication that is intentionally kept must be explicitly marked to skip the redundancy check. See [`accessible.yaml`](/database/data/category-implications/accessible.yaml) for some examples.
+
 ### 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/data/category-implications/accessible.yaml

@@ -9,6 +9,7 @@
     - finitely accessible
   proof: This follows from one of the equivalent formulations of locally finitely presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_presentable_definition_countable
   assumptions:
@@ -18,6 +19,7 @@
     - ℵ₁-accessible
   proof: This follows from one of the equivalent formulations of locally ℵ₁-presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_presentable_definition
   assumptions:
@@ -27,6 +29,7 @@
     - cocomplete
   proof: This follows from one of the equivalent formulations of locally presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_finitely_presentable_consequence
   assumptions:
@@ -42,20 +45,6 @@
     - filtered-colimit-stable monomorphisms
   proof: 'Let $\C$ be a finitely accessible category and let $G$ be an essentially small collection of finitely presentable objects which generates $\C$ under filtered colimits. Consider $G$ as a full subcategory and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $G$ is a generating collection. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.'
 
-- id: locally_finitely_presentable_raise
-  assumptions:
-    - locally finitely presentable
-  conclusions:
-    - locally ℵ₁-presentable
-  proof: This is trivial.
-
-- id: locally_countably_presentable_raise
-  assumptions:
-    - locally ℵ₁-presentable
-  conclusions:
-    - locally presentable
-  proof: This is trivial.
-
 - id: accessible_trivial_consequence
   assumptions:
     - accessible
@@ -119,6 +108,7 @@
   conclusions:
     - locally finitely presentable
   proof: See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories">Adámek–Rosický</a>, Cor. 3.7.
+  check_redundancy: false
 
 - id: finitely_accessible_raise
   assumptions:
@@ -141,6 +131,7 @@
   conclusions:
     - filtered colimits
   proof: This holds by definition.
+  check_redundancy: false
 
 - id: accessible_require_Cauchy_complete
   assumptions:
@@ -212,6 +203,7 @@
     - locally presentable
   proof: This follows from one of the equivalent formulations of locally presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_strongly_finitely_presentable_characterization
   assumptions:
@@ -221,6 +213,7 @@
     - generalized variety
   proof: This follows from the equivalence between finitary algebraic categories and locally strongly finitely presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_multi-presentable_definition
   assumptions:
@@ -230,6 +223,7 @@
     - connected limits
   proof: This follows from one of the equivalent formulations of locally multi-presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_multi-presentable_another_definition
   assumptions:
@@ -239,6 +233,7 @@
     - multi-cocomplete
   proof: This follows from one of the equivalent formulations of locally multi-presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_finitely_multi-presentable_definition
   assumptions:
@@ -248,6 +243,7 @@
     - finitely accessible
   proof: This follows from one of the equivalent formulations of locally finitely multi-presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_finitely_multi-presentable_another_definition
   assumptions:
@@ -257,6 +253,7 @@
     - multi-cocomplete
   proof: This follows from one of the equivalent formulations of locally finitely multi-presentable categories.
   is_equivalence: true
+  check_redundancy: false
 
 - id: locally_poly-presentable_definition
   assumptions:
@@ -266,10 +263,3 @@
     - wide pullbacks
   proof: This holds by definition.
   is_equivalence: true
-
-- id: locally-finitely-multi-presentable_stable-monos
-  assumptions:
-    - locally finitely multi-presentable
-  conclusions:
-    - filtered-colimit-stable monomorphisms
-  proof: Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories">Adámek–Rosický</a>, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories">Adámek–Rosický</a>, Thm. 4.26), we can in particular calculate not only filtered colimits but also kernel pairs as in a presheaf category.

database/data/category-implications/additive.yaml

@@ -14,6 +14,7 @@
   conclusions:
     - finite products
   proof: See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician">Mac Lane</a>, VIII.2, Theorem 2.
+  check_redundancy: false
 
 - id: additive_definition
   assumptions:
@@ -23,6 +24,7 @@
     - preadditive
   proof: This holds by definition.
   is_equivalence: true
+  check_redundancy: false
 
 - id: additive_biproducts
   assumptions:
@@ -42,6 +44,7 @@
     - normal
   proof: This holds by definition.
   is_equivalence: true
+  check_redundancy: false
 
 - id: abelian_implies_regular
   assumptions:
@@ -60,6 +63,7 @@
     - generator
   proof: This holds by definition.
   is_equivalence: true
+  check_redundancy: false
 
 - id: grothendieck_abelian_cogenerator
   assumptions: