From b9ebeb4093c7183781eaf151288dd0a37e61dc72 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 6 Apr 2026 12:07:02 +0200 Subject: [PATCH 1/2] add lemma about reduction to coreflexive equalizers --- database/data/004_property-assignments/Setne.sql | 6 ------ .../001_limits-colimits-existence-implications.sql | 11 +++++++++-- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql index 783535f2..708543ae 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/database/data/004_property-assignments/Setne.sql @@ -107,12 +107,6 @@ VALUES FALSE, 'Assume that the sequence of inclusions $\cdots \to \mathbb{N}_{\geq 2} \to \mathbb{N}_{\geq 1} \to \mathbb{N}_{\geq 0} = \mathbb{N}$ as a limit $X$, consisting of maps $X \to \mathbb{N}_{\geq n}$. Since $X$ is non-empty, there is a map $1 \to X$. This corresponds to a family of compatible maps $ 1 \to \mathbb{N}_{\geq n}$, i.e. to compatible elements in $\mathbb{N}_{\geq n}$. But the set $\bigcap_{n \geq 0} \mathbb{N}_{\geq n}$ is empty.' ), -( - 'Setne', - 'coreflexive equalizers', - FALSE, - 'The two distinct functions $1 \rightrightarrows \{0,1\}$ have a (unique) common retraction, but they cannot extend to a fork.' -), ( 'Setne', 'skeletal', diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 68df0784..5c064c0c 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -41,6 +41,13 @@ VALUES 'This is trivial.', FALSE ), +( + 'equalizers_via_coreflexive_equalizers', + '["coreflexive equalizers", "binary products"]', + '["equalizers"]', + 'If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\mathrm{id}_X,f), (\mathrm{id}_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\mathrm{id}_X,f)$ and $(\mathrm{id}_X,g)$. Thus, their equalizers agree.', + FALSE +), ( 'products_consequence', '["products"]', @@ -100,8 +107,8 @@ VALUES ( 'complete_characterization', '["complete"]', - '["products", "coreflexive equalizers"]', - 'See Mac Lane, V.2, Thm. 2. Note that the equalizer appearing the theorem is in fact coreflexive.', + '["products", "equalizers"]', + 'See Mac Lane, V.2, Thm. 2.', TRUE ), ( From a2dc794ce4f171467d293e7186e66f81e5cb64af Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 6 Apr 2026 12:11:21 +0200 Subject: [PATCH 2/2] document which implications we choose (limit / colimit) --- CONTRIBUTING.md | 2 +- .../001_limits-colimits-existence-implications.sql | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4b074754..f5fb1917 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -93,7 +93,7 @@ When contributing new data (categories, functors, properties, implications), ple - **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 deduced automatically. -- **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". +- **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 both in a "limit" or "colimit" variant, prefer the "limit" variant (unless the literature focusses on the "colimit" variant). - **Relevant implications**: When adding a new property, include implications involving this property and existing properties. For example, when adding the property of categories of having "countable products", also add the implication "countable products => finite products". Refactor existing implications if necessary. Ensure that for most categories and functors, it will be inferred if the property holds or not. diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 5c064c0c..03676930 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -35,9 +35,9 @@ VALUES FALSE ), ( - 'reflexive_coequalizers_are_coequalizers', - '["coequalizers"]', - '["reflexive coequalizers"]', + 'coreflexive_equalizers_are_equalizers', + '["equalizers"]', + '["coreflexive equalizers"]', 'This is trivial.', FALSE ),