diff --git a/CLAUDE.md b/CLAUDE.md index 9595feb21..8bfb1f015 100644 --- a/CLAUDE.md +++ b/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`. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ba701d399..c490f4f0d 100644 --- a/CONTRIBUTING.md +++ b/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. diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 3339a7f5b..e68317e0c 100644 --- a/database/data/category-implications/accessible.yaml +++ b/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 Adámek–Rosický, 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 (Adámek–Rosický, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adámek–Rosický, Thm. 4.26), we can in particular calculate not only filtered colimits but also kernel pairs as in a presheaf category. diff --git a/database/data/category-implications/additive.yaml b/database/data/category-implications/additive.yaml index 4b9773221..da2824580 100644 --- a/database/data/category-implications/additive.yaml +++ b/database/data/category-implications/additive.yaml @@ -14,6 +14,7 @@ conclusions: - finite products proof: See Mac Lane, 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: diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index 9af175a4f..587464870 100644 --- a/database/data/category-implications/algebraic.yaml +++ b/database/data/category-implications/algebraic.yaml @@ -13,13 +13,7 @@ conclusions: - well-copowered proof: See MO/486607. Alternatively, one may combine the facts that one-sorted finitary algebraic categories are locally (finitely) presentable and that locally presentable categories are well-copowered, both of which are saved in the database. But we include the direct proof here as well, since it makes it easier to deduce the property for one-sorted finitary algebraic categories appearing in practice. - -- id: finitary_algebraic_implies_regular - assumptions: - - finitary algebraic - conclusions: - - pullback-stable regular epimorphisms - proof: The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks. + check_redundancy: false - id: generalized_variety_require_sifted_colimit assumptions: @@ -38,23 +32,13 @@ Remark: A generalized variety is not necessarily finitely accessible, see Kawase. -- id: groupoids_are_generalized_varieties - assumptions: - - groupoid - - essentially small - conclusions: - - generalized variety - proof: This is proven as Corollary 3 here. - -# This needs to be a separate implication from "groupoids_are_generalized_varieties" -# as long as "generalized variety" is not dualized yet - id: groupoids_are_finitely_accessible assumptions: - groupoid - essentially small conclusions: - finitely accessible - proof: This is proven as Corollary 4 here. + proof: This follows from Corollary 4 here. - id: generalized_variety_left_cancellative assumptions: @@ -103,6 +87,7 @@ conclusions: - multi-algebraic proof: This is because every finite-product-sketch is clearly a (finite product, coproduct)-sketch. + check_redundancy: false - id: multi-algebraic_another_definition assumptions: @@ -112,6 +97,7 @@ - multi-cocomplete proof: This follows from one of the equivalent formulations of multi-algebraic categories. is_equivalence: true + check_redundancy: false - id: algebraic_cototal_criterion assumptions: diff --git a/database/data/category-implications/cancellative.yaml b/database/data/category-implications/cancellative.yaml index f83befd07..b5d177d1e 100644 --- a/database/data/category-implications/cancellative.yaml +++ b/database/data/category-implications/cancellative.yaml @@ -22,13 +22,4 @@ conclusions: - Cauchy complete proof: Any idempotent monomorphism must be the identity and therefore splits. - -- id: reflexive_pair_trivial - assumptions: - - left cancellative - conclusions: - - coreflexive equalizers - - effective cocongruences - - effective congruences - - reflexive coequalizers - proof: 'Any parallel pair of morphisms $f,g : A \rightrightarrows B$ with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of $\id_B$, and the cokernel pair of $\id_A$.' + check_redundancy: false diff --git a/database/data/category-implications/cartesian closed.yaml b/database/data/category-implications/cartesian closed.yaml index ce5c160c8..36cc8e581 100644 --- a/database/data/category-implications/cartesian closed.yaml +++ b/database/data/category-implications/cartesian closed.yaml @@ -30,6 +30,7 @@ conclusions: - thin proof: If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal. + check_redundancy: false - id: power_construction assumptions: @@ -70,15 +71,6 @@ - cartesian closed proof: The slice over the terminal object is the category itself. -- id: lcc_implies_regular - assumptions: - - coequalizers - - finitely complete - - locally cartesian closed - conclusions: - - regular - proof: See Johnstone, Lemma A1.5.13. From this it follows also that every elementary topos is regular. - - id: cartesian_closed_thin_criterion assumptions: - complete diff --git a/database/data/category-implications/completeness.yaml b/database/data/category-implications/completeness.yaml index 4d338e3c5..3648a18a4 100644 --- a/database/data/category-implications/completeness.yaml +++ b/database/data/category-implications/completeness.yaml @@ -5,36 +5,29 @@ assumptions: - complete conclusions: + - products - connected limits - finitely complete proof: This is trivial. + check_redundancy: false - id: complete_characterization assumptions: - - complete - conclusions: - equalizers - products + conclusions: + - complete proof: See Mac Lane, V.2, Thm. 2. - is_equivalence: true - id: finitely_complete_characterization assumptions: - - finitely complete - conclusions: - - equalizers - finite products + - equalizers + conclusions: + - finitely complete proof: See Mac Lane, V.2, Cor. 1. is_equivalence: true -- id: complete_criterion - assumptions: - - terminal object - - wide pullbacks - conclusions: - - complete - proof: See the nLab. - - id: multi-complete_generalize_limits assumptions: - complete @@ -49,6 +42,13 @@ - multi-terminal object proof: This is trivial. +- id: terminal_is_multi-terminal + assumptions: + - terminal object + conclusions: + - multi-terminal object + proof: This is trivial. + - id: multi-terminal_with_connected assumptions: - connected @@ -56,7 +56,6 @@ conclusions: - terminal object proof: Let $(T_i)_{i\in I}$ be a multi-terminal object in a connected category $\C$. By definition of multi-terminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial. - is_equivalence: true - id: multi-complete_with_initial_object assumptions: diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 6ce0c6732..95e9bafc6 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -32,16 +32,6 @@ - cokernels proof: 'By the regularity assumption, it suffices to consider cokernels of subobjects. Given a subobject $Y$ of $X$, we have the congruence on $X$ given by the pullback of ${-} : X \times X \to X$ and $Y$. The quotient of this congruence is a cokernel of $Y \hookrightarrow X$.' -- id: congruence_quotients_via_cokernels - assumptions: - - cokernels - - kernels - - preadditive - conclusions: - - quotients of congruences - proof: >- - Let $q_1, q_2 : R \rightrightarrows X$ be a congruence, let $k : R_0 \hookrightarrow R$ be the kernel of $q_2$, and let $m \coloneqq q_1 \circ k : R_0 \to X$. We claim that the cokernel of $m$ is a coequalizer of $q_1, q_2$. If $h \circ q_1 = h \circ q_2$, then $h \circ m = h \circ q_2 \circ k = 0$. Conversely, the image of $\Hom(R,R) \to \Hom(R,X)^2$, $e \mapsto (q_1 \circ e, q_2 \circ e)$ is a subgroup containing $(q_1, q_2)$ and, by reflexivity, $(q_2, q_2)$, hence also $(q_1 - q_2, 0)$. So $q_1 - q_2 = q_1 \circ e$ for some $e : R \to R$ with $q_2 \circ e = 0$. Then $e$ factors through $k$, so $q_1 - q_2$ factors through $m$, and $h \circ m = 0$ implies $h \circ q_1 = h \circ q_2$. - - id: core-thin_quotients assumptions: - core-thin diff --git a/database/data/category-implications/discrete.yaml b/database/data/category-implications/discrete.yaml index c718e7dcd..42162f525 100644 --- a/database/data/category-implications/discrete.yaml +++ b/database/data/category-implications/discrete.yaml @@ -11,6 +11,7 @@ - self-dual - split abelian proof: This is trivial. + check_redundancy: false - id: discrete_consequences assumptions: @@ -19,7 +20,6 @@ - direct - essentially discrete - locally small - - skeletal proof: This is trivial. - id: essentially_discrete_characterization @@ -30,6 +30,7 @@ - thin proof: This is trivial. is_equivalence: true + check_redundancy: false - id: essentially_discrete_consequence assumptions: @@ -38,14 +39,7 @@ - connected limits - locally essentially small proof: This is trivial. - -- id: essentially_discrete_trivial - assumptions: - - connected - - essentially discrete - conclusions: - - trivial - proof: This is trivial. + check_redundancy: false - id: discrete_multi_initial assumptions: @@ -62,3 +56,4 @@ conclusions: - essentially small proof: This is trivial. + check_redundancy: false diff --git a/database/data/category-implications/disjoint coproducts.yaml b/database/data/category-implications/disjoint coproducts.yaml index f635ddaff..8fd836450 100644 --- a/database/data/category-implications/disjoint coproducts.yaml +++ b/database/data/category-implications/disjoint coproducts.yaml @@ -16,14 +16,6 @@ - finite coproducts proof: This holds by definition. -- id: disjoint_coproducts_thin_trivial - assumptions: - - disjoint finite coproducts - - thin - conclusions: - - trivial - proof: For every object $A$ the two inclusions $A \rightrightarrows A + A$ must be equal, so their equalizer is $A$, but also $0$ since the coproduct is disjoint. Hence $A = 0$. - - id: disjoint_coproducts_strict assumptions: - disjoint finite coproducts diff --git a/database/data/category-implications/distributivity.yaml b/database/data/category-implications/distributivity.yaml index 1dad014cc..b074d2c94 100644 --- a/database/data/category-implications/distributivity.yaml +++ b/database/data/category-implications/distributivity.yaml @@ -7,6 +7,7 @@ - coproducts - finite products proof: This holds by definition. + check_redundancy: false - id: countably_distributive_assumption assumptions: @@ -15,6 +16,7 @@ - countable coproducts - finite products proof: This holds by definition. + check_redundancy: false - id: distributive_assumption assumptions: @@ -78,15 +80,6 @@ - infinitary distributive proof: Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts. -- id: countably_distributive_filtered_criterion - assumptions: - - cartesian filtered colimits - - countable coproducts - - distributive - conclusions: - - countably distributive - proof: Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all countable coproducts. - - id: distributive_duality assumptions: - distributive diff --git a/database/data/category-implications/equalizers.yaml b/database/data/category-implications/equalizers.yaml index f92516056..424ebd58a 100644 --- a/database/data/category-implications/equalizers.yaml +++ b/database/data/category-implications/equalizers.yaml @@ -1,4 +1,4 @@ -# results on equalizers, coreflexive coequalizers, and kernels +# results on equalizers, coreflexive equalizers, and kernels - id: equalizers_criterion assumptions: @@ -6,7 +6,11 @@ - pullbacks conclusions: - equalizers - proof: 'The equalizer of $f,g : X \rightrightarrows Y$ is the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$.' + proof: >- + The equalizer of $f,g : X \rightrightarrows Y$ can be constructed as the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$. + + Alternatively, the claim follows from this implication and this implication. The resulting construction of the equalizer is the pullback of $(\id_X,f) : X \to X \times Y$ and $(\id_X, g) : X \to X \times Y$. + check_redundancy: false - id: coreflexive_equalizers_are_equalizers assumptions: @@ -21,7 +25,7 @@ - coreflexive equalizers conclusions: - equalizers - proof: 'If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\id_X,f), (\id_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\id_X,f)$ and $(\id_X,g)$. Thus, their equalizers agree.' + proof: 'If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\id_X,f), (\id_X,g) : X \rightrightarrows X \times Y$, with the projection $X \times Y \to X$ as a common retraction. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\id_X,f)$ and $(\id_X,g)$. Thus, their equalizers agree.' - id: equalizers_consequence assumptions: @@ -77,6 +81,7 @@ Choose an object $A$ and a kernel $k : K \to A$ of $\id_A$. Then $k = \id_A \circ k = 0_{A,A} \circ k = 0_{K,A}$. For every object $T$, the zero morphism $0_{T,K}$ provides a morphism $T \to K$. Conversely, if $f : T \to K$ is any morphism, then $k \circ f = k \circ 0_{T,K}$ since $k$ is a zero morphism, hence $f = 0_{T,K}$, using that $k$ is also a monomorphism. Thus, $K$ is a terminal object. Remark: With this result it follows that $K$ is even a zero object. + check_redundancy: false - id: kernels_multi-terminal assumptions: diff --git a/database/data/category-implications/exact filtered colimits.yaml b/database/data/category-implications/exact filtered colimits.yaml index 17fdc590e..986b46200 100644 --- a/database/data/category-implications/exact filtered colimits.yaml +++ b/database/data/category-implications/exact filtered colimits.yaml @@ -8,6 +8,7 @@ - filtered colimits - finitely complete proof: This holds by definition. + check_redundancy: false - id: exact_filtered_colimits_monos assumptions: diff --git a/database/data/category-implications/extensive.yaml b/database/data/category-implications/extensive.yaml index 13c4ecaaa..4af040b4b 100644 --- a/database/data/category-implications/extensive.yaml +++ b/database/data/category-implications/extensive.yaml @@ -6,6 +6,7 @@ conclusions: - finite coproducts proof: This holds by definition. + check_redundancy: false - id: countably_extensive_assumption assumptions: @@ -111,9 +112,9 @@ - countably extensive - cofiltered-limit-stable epimorphisms conclusions: - - trivial + - thin proof: >- - Let $\C$ be a countably extensive category with cofiltered-limit-stable epimorphisms. We show that $\C$ is thin. Since $\C$ has disjoint finite coproducts, it is then trivial by this implication. + Let $\C$ be a countably extensive category with cofiltered-limit-stable epimorphisms. We show that $\C$ is thin. (With other results, one can further deduce that $\C$ is trivial.) Let $T$ be an object, let $T_m$ be the summand with index $m$ of the coproduct $\coprod_{m \in \IN} T$, and for $n \in \IN$ let $$\textstyle D(n) \coloneqq \coprod_{m \geq n} T_m.$$ diff --git a/database/data/category-implications/groupoids.yaml b/database/data/category-implications/groupoids.yaml index a92ffdde9..89ae5061e 100644 --- a/database/data/category-implications/groupoids.yaml +++ b/database/data/category-implications/groupoids.yaml @@ -6,10 +6,7 @@ conclusions: - directed limits - left cancellative - - mono-regular - - pullbacks - self-dual - - well-powered proof: This is easy. - id: groupoid_criterion @@ -36,24 +33,6 @@ - locally cartesian closed proof: Every slice category is a trivial category. -- id: groupoid_generator - assumptions: - - groupoid - - generator - conclusions: - - extremal generator - proof: This is trivial. - -- id: groupoid_generating_collection - # redundant because of "generating_collection_balanced_consequence", - # but we can keep it, because the proof is simpler. - assumptions: - - groupoid - - generating collection - conclusions: - - extremal generating collection - proof: This is trivial. - - id: groupoid_with_multi-terminal assumptions: - groupoid diff --git a/database/data/category-implications/products.yaml b/database/data/category-implications/products.yaml index bb752887c..aaddce060 100644 --- a/database/data/category-implications/products.yaml +++ b/database/data/category-implications/products.yaml @@ -30,6 +30,7 @@ - terminal object proof: The non-trivial direction follows since finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$. is_equivalence: true + check_redundancy: false - id: products_criterion assumptions: @@ -38,6 +39,7 @@ conclusions: - products proof: The product $\prod_{i \in I} X_i$ is the cofiltered limit of the finite partial products $\prod_{i \in E} X_i$ where $E$ ranges over the finite subsets of $I$. + check_redundancy: false - id: products_criterion_countable assumptions: @@ -129,6 +131,7 @@ conclusions: - copowers proof: Let $\C$ be a category with filtered colimits and finite copowers. Let $X \in \C$ be an object and $I$ be a set. The poset $P_{<\aleph_0}(I)$ of finite subsets of $I$ is filtered, and we have a diagram $P_{<\aleph_0}(I) \to \C$, $A \mapsto A \otimes X$. Its colimit is the copower $I \otimes X$. + check_redundancy: false - id: copowers_criterion_countable assumptions: diff --git a/database/data/category-implications/pullbacks.yaml b/database/data/category-implications/pullbacks.yaml index 8ccbe9824..196219b85 100644 --- a/database/data/category-implications/pullbacks.yaml +++ b/database/data/category-implications/pullbacks.yaml @@ -32,7 +32,8 @@ - pullbacks conclusions: - wide pullbacks - proof: Each slice category has finite products and is essentially finite, hence has all products by this result followed by this result. + proof: Each slice category has finite products and is essentially finite. By this result it is thin, and then by this result it has all products. + check_redundancy: false - id: pullback_implies_Cauchy_complete assumptions: diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index ffc00bdf1..f76e0cf20 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -14,7 +14,12 @@ conclusions: - extremal generating collection - locally essentially small - - well-copowered + proof: This is trivial. + +- id: essentially_small_well-powered + assumptions: + - essentially small + conclusions: - well-powered proof: This is trivial. diff --git a/database/data/category-implications/subobject classifiers.yaml b/database/data/category-implications/subobject classifiers.yaml index 1635b5999..23cdaedf2 100644 --- a/database/data/category-implications/subobject classifiers.yaml +++ b/database/data/category-implications/subobject classifiers.yaml @@ -1,12 +1,19 @@ # results on subobject classifiers and regular subobject classifiers -- id: subobject_classifier_consequence +- id: subobject_classifier_assumption assumptions: - subobject classifier conclusions: - finitely complete + proof: This holds by definition of a subobject classifier. We assume that finite limits exist. + check_redundancy: false + +- id: subobject_classifier_consequence + assumptions: + - subobject classifier + conclusions: - mono-regular - proof: 'The first part holds by convention. For the second part, note that any monomorphism $U \to X$ is the equalizer of $\chi_U,\chi_X : X \rightrightarrows \Omega$.' + proof: 'Any monomorphism $U \to X$ is the equalizer of $\chi_U,\chi_X : X \rightrightarrows \Omega$.' - id: subobject_classifier_well-powered assumptions: @@ -24,14 +31,6 @@ - normal proof: 'The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.' -- id: additive_trivial_condition - assumptions: - - additive - - regular subobject classifier - conclusions: - - trivial - proof: See MSE/4086192. - - id: regular_subobjects_trivial assumptions: - finitely complete @@ -47,12 +46,12 @@ - regular subobject classifier proof: This is obvious. -- id: regular_subobject_assumption +- id: regular_subobject_classifier_assumption assumptions: - regular subobject classifier conclusions: - finitely complete - proof: This holds by definition. + proof: This holds by definition of a regular subobject classifier. We assume that finite limits exist. - id: regular_subobjects_suffice assumptions: diff --git a/database/data/category-implications/subobject-trivial.yaml b/database/data/category-implications/subobject-trivial.yaml index 7424cdefc..c2808eeeb 100644 --- a/database/data/category-implications/subobject-trivial.yaml +++ b/database/data/category-implications/subobject-trivial.yaml @@ -13,8 +13,7 @@ - regular-subobject-trivial conclusions: - thin - proof: 'For the forward direction, if $f,g : X \rightrightarrows Y$ are morphisms, their equalizer is a regular monomorphism $E \hookrightarrow X$, hence an isomorphism. But this means $f = g$. The reverse implication is trivial.' - is_equivalence: true + proof: 'If $f,g : X \rightrightarrows Y$ are morphisms, their equalizer is a regular monomorphism $E \hookrightarrow X$, hence an isomorphism. But this means $f = g$.' - id: subobject-trivial_characterization assumptions: @@ -63,14 +62,6 @@ - trivial proof: 'For any object $X$, the unique morphism $! : 0 \to X$ is a regular monomorphism, as the equalizer of the two coprojections $X \rightrightarrows X \sqcup X$. Therefore, it is an isomorphism.' -- id: disjoint_finite_coproducts_disallows_regular-quotient-trivial - assumptions: - - disjoint finite coproducts - - regular-quotient-trivial - conclusions: - - trivial - proof: 'For any object $X$, the coequalizer of the two coprojections $X \rightrightarrows X \sqcup X$ is the codiagonal $\nabla : X \sqcup X \to X$. Therefore, these two coprojections are equal. But their equalizer is also the unique morphism $! : 0 \to X$. It follows that $! : 0 \to X$ is an isomorphism.' - - id: regular_subobject_trivial_congruences # TODO: refactor this once we add "split-mono-trivial", cf. #383 assumptions: diff --git a/database/data/category-implications/thin.yaml b/database/data/category-implications/thin.yaml index 7979ee2f5..0ea296ac7 100644 --- a/database/data/category-implications/thin.yaml +++ b/database/data/category-implications/thin.yaml @@ -119,6 +119,7 @@ conclusions: - products proof: The category is equivalent to a finite preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a finite one. + check_redundancy: false - id: thin_countable_product_reduction assumptions: @@ -128,6 +129,7 @@ conclusions: - products proof: The category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one. + check_redundancy: false - id: cocomplete_thin_criterion assumptions: @@ -137,15 +139,7 @@ conclusions: - cocomplete proof: The supremum of a subset in a preordered set is the infimum of the set of upper bounds. - -- id: thin_zero_trivial - assumptions: - - inhabited - - thin - - zero morphisms - conclusions: - - trivial - proof: This is easy. + check_redundancy: false - id: thin_power assumptions: diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index 728cb291f..7298ba6a3 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -9,6 +9,7 @@ - subobject classifier proof: This holds by definition. is_equivalence: true + check_redundancy: false - id: topos_consequences assumptions: @@ -16,18 +17,9 @@ conclusions: - disjoint finite coproducts - effective congruences - - epi-regular - finitely cocomplete - locally cartesian closed - proof: See Mac Lane–Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. IV.7.8; and Johnstone, Part A, Prop. 2.4.1 and Cor. 2.3.4. - -- id: topos_well-copowered_criterion - assumptions: - - elementary topos - - locally essentially small - conclusions: - - well-copowered - proof: This follows from Mac Lane–Moerdijk, Theorem IV.7.8 (and Prop. I.3.1). + proof: See Mac Lane–Moerdijk, Cor. IV.5.4 (finite cocompleteness), Cor. IV.10.5 (disjoint finite coproducts); and Johnstone, Part A, Cor. 2.3.4 (locally cartesian closed) and Prop. 2.4.1 (effective congruences). - id: topos_implies_coregular assumptions: @@ -45,6 +37,7 @@ conclusions: - cocomplete proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_powers assumptions: @@ -77,6 +70,7 @@ conclusions: - coproducts proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_countable_products assumptions: @@ -85,6 +79,7 @@ conclusions: - countable coproducts proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_aleph2_products assumptions: @@ -101,6 +96,7 @@ conclusions: - sequential colimits proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_sifted assumptions: @@ -109,6 +105,7 @@ conclusions: - sifted colimits proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_filtered assumptions: @@ -117,6 +114,7 @@ conclusions: - filtered colimits proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_aleph1_filtered assumptions: @@ -133,6 +131,7 @@ conclusions: - connected colimits proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_monadic_over_itself_wide_pullbacks assumptions: @@ -141,6 +140,7 @@ conclusions: - wide pushouts proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + check_redundancy: false - id: topos_generator_implies_cogenerator assumptions: @@ -160,26 +160,25 @@ # ---- end of consequences of the monadicity of P ---- -- id: grothendieck_topos_definition +- id: grothendieck_topos_criterion assumptions: - - Grothendieck topos - conclusions: - coproducts - elementary topos - generating collection - locally essentially small + conclusions: + - Grothendieck topos proof: See Mac Lane–Moerdijk, Appendix, Prop. 4.4. - is_equivalence: true - id: grothendieck_topos_consequence assumptions: - Grothendieck topos conclusions: - - cogenerator - - exact filtered colimits - - infinitary extensive - locally presentable - proof: A Grothendieck topos is locally presentable by Borceux, Vol. 3, Prop. 3.4.16, has a cogenerator (see nLab) and is infinitary extensive by Giraud's Theorem. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). Every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits (nLab), so we conclude with Lemma 3 here. + - subobject classifier + - cartesian closed + - exact filtered colimits + proof: A Grothendieck topos is locally presentable by Borceux, Vol. 3, Prop. 3.4.16. It is cartesian closed by Mac Lane–Moerdijk, Prop. III.6.1 (or Borceux, Prop. 3.4.17), and it has a subobject classifier by Prop. III.7.3 in op. cit. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). By Theorem III.5.1 in op. cit., every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits, so we conclude with Lemma 3 here. - id: pretopos_definition assumptions: @@ -200,3 +199,4 @@ - regular subobject classifier proof: This is true by definition. is_equivalence: true + check_redundancy: false diff --git a/database/data/functor-implications/equivalences.yaml b/database/data/functor-implications/equivalences.yaml index 3f6535275..799c6805a 100644 --- a/database/data/functor-implications/equivalences.yaml +++ b/database/data/functor-implications/equivalences.yaml @@ -6,6 +6,7 @@ - equivalence proof: This is standard, see Mac Lane, Ch. IV, Theorem 4.1. is_equivalence: true + check_redundancy: false - id: equivalence_invertible assumptions: @@ -18,6 +19,7 @@ $$L \cong L \circ F \circ R \cong R.$$ Hence, $R$ and $L$ are (pseudo-)inverse to $F$. is_equivalence: true + check_redundancy: false - id: equivalence_consequences assumptions: @@ -26,6 +28,7 @@ - monadic - reflector proof: This is easy. + check_redundancy: false - id: isomorphism_is_equivalence assumptions: diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index 1a7b7dd97..2e02d3cc8 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/database/data/morphism-implications/mono-epi-iso.yaml @@ -22,6 +22,7 @@ conclusions: - isomorphism proof: 'Assume that $m : A \to B$ is a split monomorphism, and choose a morphism $e : B \to A$ with $e \circ m = \id_A$. Then $m \circ e \circ m = m = \id_B \circ m$. Thus, if $m$ is also an epimorphism, we conclude $m \circ e = \id_B$, showing that $m$ is an isomorphism with inverse $e$.' + check_redundancy: false - id: mono_is_iso assumptions: @@ -33,17 +34,6 @@ - isomorphism proof: This holds by definition of a subobject-trivial category. -- id: balanced_def - assumptions: - - monomorphism - - epimorphism - associated_assumptions: - category: - - balanced - conclusions: - - isomorphism - proof: This holds by definition of a balanced category. - - id: mono-regular_def assumptions: - monomorphism diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 7765e4b57..476344f54 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -5,6 +5,8 @@ CREATE TABLE implications ( is_equivalence INTEGER NOT NULL DEFAULT FALSE CHECK (is_equivalence IN (TRUE, FALSE)), is_deduced INTEGER NOT NULL DEFAULT FALSE, + check_redundancy INTEGER NOT NULL DEFAULT TRUE + CHECK (check_redundancy in (TRUE, FALSE)), dual_implication_id TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 201bdaa04..3e5c60318 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -436,8 +436,8 @@ function seed_implications(type: StructureType) { const implication_insert = db.prepare( `INSERT INTO implications ( - id, type, proof, is_equivalence - ) VALUES (?, ?, ?, ?)` + id, type, proof, is_equivalence, check_redundancy + ) VALUES (?, ?, ?, ?, ?)` ) const assumption_insert = db.prepare( @@ -462,7 +462,13 @@ function seed_implications(type: StructureType) { implications: v.InferOutput ) { for (const impl of implications) { - implication_insert.run(impl.id, type, impl.proof, impl.is_equivalence ? 1 : 0) + implication_insert.run( + impl.id, + type, + impl.proof, + impl.is_equivalence ? 1 : 0, + impl.check_redundancy === false ? 0 : 1 + ) for (const assumption of impl.assumptions) { assumption_insert.run(impl.id, assumption, type) diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 2b40ee5dd..5c6f904ac 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -22,7 +22,8 @@ import { STRUCTURE_TYPES, type StructureType, PLURALS } from '#shared/config.ts' import fs from 'node:fs' import path from 'node:path' import { decode_property_ID } from '#shared/property.utils.ts' -import { test_no_redundant_assignments } from './utils/redundancies' +import { test_no_redundant_assignments } from './utils/redundant-assignments' +import { test_no_redundant_implications } from './utils/redundant-implications' const db = get_client({ readonly: true }) @@ -94,6 +95,7 @@ function execute_tests() { devlog('\n--- Test redundancies ---') + test_no_redundant_implications(db) test_no_redundant_assignments(db) } catch (err) { if (err instanceof Error) { diff --git a/database/scripts/utils/redundancies.ts b/database/scripts/utils/redundant-assignments.ts similarity index 100% rename from database/scripts/utils/redundancies.ts rename to database/scripts/utils/redundant-assignments.ts diff --git a/database/scripts/utils/redundant-implications.ts b/database/scripts/utils/redundant-implications.ts new file mode 100644 index 000000000..14841c0e4 --- /dev/null +++ b/database/scripts/utils/redundant-implications.ts @@ -0,0 +1,139 @@ +import type { Database } from 'better-sqlite3' +import { STRUCTURE_TYPES, type StructureType } from '#shared/config.ts' +import { + get_associated_implications, + get_normalized_implications, + has_associated_assumptions, + stringify_with_asterisk +} from '#shared/implications.ts' +import { close_associated_assumptions, find_deduction } from '#shared/deduction.utils.ts' +import { capitalize, devlog, remove_underscores } from '#shared/utils.ts' + +/** + * Tests that there are no redundant implications, + * except for those marked with check_redundancy: false. + * All redundancies are collected before an error is thrown. + */ +export function test_no_redundant_implications(db: Database) { + const errors: string[] = [] + + for (const type of STRUCTURE_TYPES) { + errors.push(...get_redundant_implication_errors(db, type)) + } + + if (errors.length > 0) { + const hint = [ + '', + 'Remove each redundant implication or conclusion from its YAML file.', + 'Only keep it if there is a good reason, e.g. it states a definition', + 'or an insightful consequence, and then mark it with check_redundancy: false.' + ] + throw new Error([errors.join('\n\n'), ...hint].join('\n')) + } +} + +/** + * Checks for redundant implications and returns one error message per implication. + * An implication is redundant if one of its normalized implications + * P_1 + ... + P_n ===> Q can be deduced from all other normalized implications, + * except the dual one. Implications marked with check_redundancy: false are skipped. + */ +function get_redundant_implication_errors(db: Database, type: StructureType): string[] { + const implications = get_normalized_implications(db, type) + + const original_implications = db + .prepare< + [StructureType], + { id: string; dual_implication_id: string | null; check_redundancy: 0 | 1 } + >( + `SELECT id, dual_implication_id, check_redundancy + FROM implications + WHERE type = ? AND is_deduced = FALSE` + ) + .all(type) + + const dual_properties_list = db + .prepare<[StructureType], [string, string | null]>( + `SELECT id, dual_property_id FROM properties WHERE type = ?` + ) + .raw() + .all(type) + + const dual_properties_map = new Map(dual_properties_list) + + const associated_implications = get_associated_implications(db, type) + + let ignore_count = 0 + + const errors: string[] = [] + + for (const original of original_implications) { + const { id, dual_implication_id, check_redundancy } = original + + if (!check_redundancy) { + ignore_count++ + continue + } + + const redundancies: string[] = [] + let has_asterisk = false + + for (const piece of implications.filter((impl) => impl.id === id)) { + const dual_conclusion = dual_properties_map.get(piece.conclusion) + + const other_implications = implications.filter( + (impl) => + impl !== piece && + !( + impl.id === dual_implication_id && + impl.conclusion === dual_conclusion + ) + ) + + const deduction = find_deduction( + piece.assumptions, + other_implications, + (property) => property === piece.conclusion, + close_associated_assumptions( + piece.associated_assumptions, + associated_implications + ) + ) + + if (!deduction) continue + + if ([piece, ...deduction].some(has_associated_assumptions)) { + has_asterisk = true + } + + redundancies.push( + [ + ` Claim: ${stringify_with_asterisk(piece)}`, + ' Proof:', + ...deduction.map( + (impl) => ` - ${stringify_with_asterisk(impl)} [${impl.id}]` + ) + ].join('\n') + ) + } + + if (redundancies.length > 0) { + const lines = [ + `❌ Redundant ${remove_underscores(type)} implication [${id}]`, + ...redundancies + ] + if (has_asterisk) { + lines.push(' * has assumptions about associated structures (not shown)') + } + errors.push(lines.join('\n')) + } + } + + if (errors.length === 0) { + devlog( + `✅ ${capitalize(remove_underscores(type))} implications are not redundant (${ignore_count} ignored)` + ) + } + + return errors +} diff --git a/database/scripts/utils/seed.schemas.ts b/database/scripts/utils/seed.schemas.ts index 6d37d7704..8873b0d69 100644 --- a/database/scripts/utils/seed.schemas.ts +++ b/database/scripts/utils/seed.schemas.ts @@ -127,7 +127,8 @@ export const implications_yaml_schema = v.array( v.record(v.string(), distinct_strings_schema) ), proof: v.string(), - is_equivalence: v.optional(v.literal(true)) + is_equivalence: v.optional(v.literal(true)), + check_redundancy: v.optional(v.literal(false)) }), v.check( (impl) => diff --git a/shared/deduction.utils.ts b/shared/deduction.utils.ts index 541c3c5cb..be28d7702 100644 --- a/shared/deduction.utils.ts +++ b/shared/deduction.utils.ts @@ -132,3 +132,86 @@ function is_applicable( }) ) } + +/** + * Deduces properties from the satisfied ones until one of them satisfies + * the given predicate. Returns the implications used for its deduction, + * in the order in which they are applied, or null if no such property + * can be deduced. + */ +export function find_deduction( + satisfied_properties: Set, + implications: NormalizedImplication[], + is_target: (property: string) => boolean, + associated_satisfied_properties?: Partial>> +): NormalizedImplication[] | null { + const { proofs, stop_property } = deduce_properties( + satisfied_properties, + implications, + (implication) => ({ + proof: implication, + stop: is_target(implication.conclusion) + }), + associated_satisfied_properties + ) + + if (!stop_property) return null + + return trace_deduction(satisfied_properties, proofs, stop_property) +} + +/** + * Traces back the deduction of a property from the satisfied properties + * and returns the implications used, in the order in which they are applied. + */ +function trace_deduction( + satisfied_properties: Set, + proofs: Partial>, + target_property: string +) { + const used_implications: NormalizedImplication[] = [] + + const visited_properties = new Set() + + function derive(property: string) { + if (visited_properties.has(property)) return + if (satisfied_properties.has(property)) return + visited_properties.add(property) + + const implication = proofs[property] + if (!implication) throw new Error(`Missing deduction for property: ${property}`) + + for (const p of implication.assumptions) derive(p) + + used_implications.push(implication) + } + + derive(target_property) + + return used_implications +} + +/** + * Returns the given associated assumptions (e.g. "the domain + * is complete"), each closed under the implications of the associated + * structure type (e.g. "the domain has products"). + */ +export function close_associated_assumptions( + associated_assumptions: Partial>> | undefined, + associated_implications: Record +) { + if (!associated_assumptions) return undefined + + const closed: Partial>> = {} + + for (const [label, properties] of Object.entries(associated_assumptions)) { + if (!properties) continue + closed[label] = deduce_properties( + properties, + associated_implications[label] ?? [], + () => ({ proof: null, stop: false }) + ).deduced_satisfied_properties + } + + return closed +} diff --git a/shared/implications.ts b/shared/implications.ts index 3f7574954..220bc92f8 100644 --- a/shared/implications.ts +++ b/shared/implications.ts @@ -89,6 +89,45 @@ export function get_normalized_implications( return implications } +/** + * Returns a dictionary mapping each label of a structure association + * of the given type (e.g. "domain" for functors) to the normalized + * implications of the associated structure type. + */ +export function get_associated_implications(db: Database, type: StructureType) { + const associations = db + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations WHERE source_type = ?` + ) + .all(type) + + const cache = new Map() + const result: Record = {} + + for (const { label, target_type } of associations) { + if (!cache.has(target_type)) { + cache.set(target_type, get_normalized_implications(db, target_type)) + } + result[label] = cache.get(target_type)! + } + + return result +} + export function stringify_implication(implication: NormalizedImplication) { return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` } + +export function has_associated_assumptions(implication: NormalizedImplication) { + return implication.associated_assumptions !== undefined +} + +/** + * Stringifies the implication and marks it with an asterisk + * if it has assumptions about associated structures. + */ +export function stringify_with_asterisk(implication: NormalizedImplication) { + const asterisk = has_associated_assumptions(implication) ? ' *' : '' + return stringify_implication(implication) + asterisk +} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 687bebd03..3494bb484 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -114,8 +114,13 @@ export type ImplicationDisplay = Replace< } > +export type ContradictionStep = { + implication_id: string | null + statement: string +} + export type SearchResults = { - contradiction: string[] | null + contradiction: ContradictionStep[] | null satisfied_properties: string[] unsatisfied_properties: string[] dual_satisfied_properties: (string | null)[] diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts deleted file mode 100644 index b4026b5d7..000000000 --- a/src/lib/server/consistency.ts +++ /dev/null @@ -1,81 +0,0 @@ -import { deduce_properties } from '#shared/deduction.utils.ts' -import type { StructureType } from '#lib/commons/types.ts' -import { - get_normalized_implications, - type NormalizedImplication, - stringify_implication -} from '#shared/implications.ts' -import { db } from './db' - -export function get_contradiction( - satisfied_properties: Set, - unsatisfied_properties: Set, - type: StructureType -): { contradiction: string[] | null } { - for (const p of satisfied_properties) { - const contradiction = [`${p} ⟹ ${p}`] - if (unsatisfied_properties.has(p)) return { contradiction } - } - - const implications = get_normalized_implications(db, type).filter( - (impl) => !impl.associated_assumptions - ) - - const contradiction = contradiction_worker( - satisfied_properties, - unsatisfied_properties, - implications - ) - - return { contradiction } -} - -function contradiction_worker( - satisfied_properties: Set, - unsatisfied_properties: Set, - implications: NormalizedImplication[] -): string[] | null { - for (const p of satisfied_properties) { - if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`] - } - - const { proofs, stop_property } = deduce_properties( - satisfied_properties, - implications, - (implication) => ({ - proof: implication, - stop: unsatisfied_properties.has(implication.conclusion) - }) - ) - - if (!stop_property) return null - - return build_shortest_proof(satisfied_properties, proofs, stop_property) -} - -function build_shortest_proof( - satisfied_properties: Set, - proofs: Partial>, - target_property: string -) { - const proof: string[] = [] - - const visited_properties = new Set() - - function derive(property: string) { - if (visited_properties.has(property)) return - if (satisfied_properties.has(property)) return - visited_properties.add(property) - - const implication = proofs[property] - if (!implication) throw new Error(`Missing deduction for property: ${property}`) - - for (const p of implication.assumptions) derive(p) - - proof.push(stringify_implication(implication)) - } - - derive(target_property) - - return proof -} diff --git a/src/lib/server/fetchers/search.ts b/src/lib/server/fetchers/search.ts index 0fead0fee..bc59480be 100644 --- a/src/lib/server/fetchers/search.ts +++ b/src/lib/server/fetchers/search.ts @@ -2,9 +2,18 @@ import { decode_property_ID } from '#shared/property.utils.ts' import { db } from '#lib/server/db.ts' import { error } from '@sveltejs/kit' import { SEARCH_SEPARATOR } from '#lib/commons/search.config.ts' -import { get_contradiction } from '#lib/server/consistency.ts' -import type { SearchResults, StructureShort, StructureType } from '#lib/commons/types.ts' +import type { + ContradictionStep, + SearchResults, + StructureShort, + StructureType +} from '#lib/commons/types.ts' import { to_placeholders } from '#shared/utils.ts' +import { find_deduction } from '#shared/deduction.utils.ts' +import { + get_normalized_implications, + stringify_implication +} from '#shared/implications.ts' export function fetch_search_results( satisfied_query: string | null, @@ -67,7 +76,7 @@ export function fetch_search_results( dual_satisfied_properties.every(Boolean) && dual_unsatisfied_properties.every(Boolean) - const { contradiction } = get_contradiction( + const contradiction = get_contradiction( new Set(satisfied_properties), new Set(unsatisfied_properties), type @@ -144,3 +153,35 @@ export function fetch_search_results( type } } + +/** + * Returns a deduction of a property that is required to be unsatisfied + * from the properties that are required to be satisfied, as a list of + * implications, or null if the requirements are consistent. + */ +function get_contradiction( + satisfied_properties: Set, + unsatisfied_properties: Set, + type: StructureType +): ContradictionStep[] | null { + for (const p of satisfied_properties) { + if (unsatisfied_properties.has(p)) { + return [{ implication_id: null, statement: `${p} ⟹ ${p}` }] + } + } + + const implications = get_normalized_implications(db, type).filter( + (impl) => !impl.associated_assumptions + ) + + const deduction = find_deduction(satisfied_properties, implications, (p) => + unsatisfied_properties.has(p) + ) + + return deduction + ? deduction.map((implication) => ({ + implication_id: implication.id, + statement: stringify_implication(implication) + })) + : null +} diff --git a/src/pages/SearchResultsPage.svelte b/src/pages/SearchResultsPage.svelte index 0fee8f939..1ca3640f0 100644 --- a/src/pages/SearchResultsPage.svelte +++ b/src/pages/SearchResultsPage.svelte @@ -104,8 +104,19 @@

    - {#each contradiction as segment} -
  1. {segment}
    2. + {#each contradiction as step} +
  2. + {#if step.implication_id} + + {step.statement} + + {:else} + {step.statement} + {/if} +
    3. {/each}
{/if} diff --git a/src/routes/app.css b/src/routes/app.css index a5f5bd72f..ca88f1207 100644 --- a/src/routes/app.css +++ b/src/routes/app.css @@ -277,6 +277,10 @@ a.button { display: inline-block; } +a.no-underline { + text-decoration: none; +} + label { display: block; margin-bottom: 0.1rem; diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index 82f8b2c98..d4601d230 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -116,10 +116,16 @@ @@ -141,9 +147,5 @@ diff --git a/tests/category-search.spec.ts b/tests/category-search.spec.ts index 5ff428e76..1db768ce1 100644 --- a/tests/category-search.spec.ts +++ b/tests/category-search.spec.ts @@ -205,5 +205,8 @@ test('contradictions are detected', async ({ page }) => { const body = page.locator('body') await expect(body).toContainText('the requirements are inconsistent') - await expect(body).toContainText('equalizers ∧ products ⟹ complete') + + await expect( + page.getByRole('link', { name: 'equalizers ∧ products ⟹ complete' }) + ).toHaveAttribute('href', '/category-implication/complete_characterization') }) diff --git a/tests/functor-search.spec.ts b/tests/functor-search.spec.ts index d24dfdfcf..d6f193803 100644 --- a/tests/functor-search.spec.ts +++ b/tests/functor-search.spec.ts @@ -192,9 +192,21 @@ test('contradictions are detected', async ({ page }) => { const body = page.locator('body') await expect(body).toContainText('the requirements are inconsistent') - await expect(body).toContainText('continuous ⟹ preserves products') - await expect(body).toContainText('preserves products ⟹ preserves finite products') - await expect(body).toContainText( - 'preserves finite products ⟹ preserves terminal objects' + + await expect( + page.getByRole('link', { name: 'continuous ⟹ preserves products' }) + ).toHaveAttribute('href', '/functor-implication/continuous_consequences') + + await expect( + page.getByRole('link', { name: 'preserves products ⟹ preserves finite products' }) + ).toHaveAttribute('href', '/functor-implication/products_consequences') + + await expect( + page.getByRole('link', { + name: 'preserves finite products ⟹ preserves terminal objects' + }) + ).toHaveAttribute( + 'href', + '/functor-implication/preserve_finite_products_consequences' ) }) diff --git a/tests/morphism-search.spec.ts b/tests/morphism-search.spec.ts index 75968b278..6eda4bd2e 100644 --- a/tests/morphism-search.spec.ts +++ b/tests/morphism-search.spec.ts @@ -186,5 +186,8 @@ test('contradictions are detected', async ({ page }) => { const body = page.locator('body') await expect(body).toContainText('the requirements are inconsistent') - await expect(body).toContainText('isomorphism ⟹ split epimorphism') + + await expect( + page.getByRole('link', { name: 'isomorphism ⟹ split epimorphism' }) + ).toHaveAttribute('href', '/morphism-implication/dual_iso_is_mono') })