From f1f9dbc650c110c468150bb0510ae5169caca36f Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 10 Oct 2026 14:14:10 -0400 Subject: [PATCH 1/3] Initial commit introducing property of every regular congruence being effective (and its dual) --- database/data/categories/Alg(R).yaml | 2 +- database/data/categories/Cat.yaml | 5 +-- database/data/categories/Mon.yaml | 2 +- database/data/categories/SemiGrp.yaml | 2 +- .../category-implications/congruences.yaml | 32 +++++++++++++++++++ .../data/category-implications/topos.yaml | 11 +++++++ .../effective cocongruences.yaml | 1 + .../effective congruences.yaml | 1 + .../effective regular cocongruences.yaml | 16 ++++++++++ .../effective regular congruences.yaml | 16 ++++++++++ 10 files changed, 81 insertions(+), 7 deletions(-) create mode 100644 database/data/category-properties/effective regular cocongruences.yaml create mode 100644 database/data/category-properties/effective regular congruences.yaml diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index 2a95f93c6..1dd582895 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -72,7 +72,7 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. - - property: effective cocongruences + - property: effective regular cocongruences proof: 'MO/510744 presents a counterexample for $\Ring$, and it can be easily generalized to $\Alg(R)$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.' special_objects: diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index cc24d2f7b..bd273d040 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -45,9 +45,6 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism, but not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. - - property: regular - proof: See Example 3.14 at the nLab. - - property: coregular proof: 'We already know that $\Mon$ is not coregular; in fact we have shown that there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' references: @@ -62,7 +59,7 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Cat$ that maps a set to its discrete category. - - property: effective cocongruences + - property: effective regular cocongruences proof: >- The counterexample is similar to the one for $\Mon$: Let $X$ be the walking idempotent, and let $E$ be the delooping of the monoid with presentation $$\langle p, q \mid p^2=p,\, q^2=q,\, pq=q,\, qp=p \rangle.$$ diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index 6fd588a00..d31049ee4 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -74,7 +74,7 @@ unsatisfied_properties: references: - Grp_no_cocartesian_cofiltered_limits - - property: effective cocongruences + - property: effective regular cocongruences proof: >- We adapt the counterexample from MO/510744 for $\Ring$. Namely, consider the monoids $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle. \end{align*}$$ diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index b773146cc..befe55a46 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -58,7 +58,7 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. - - property: effective cocongruences + - property: effective regular cocongruences proof: >- The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$ diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 5e6db445c..1c1737ec3 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -127,6 +127,15 @@ Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is treated in Borceux–Bourn, Example 2.2.18. An alternative proof of this special case is given later in A.5.17. +- id: regular_extensive_consequences + assumptions: + - regular + - extensive + - quotients of congruences + conclusions: + - effective regular cocongruences + proof: (For now, will leave this as a placeholder for a reference to the proof to be merged in from PR 373.) + - id: pretopos_balanced assumptions: - effective congruences @@ -153,3 +162,26 @@ - effective congruences proof: This holds by definition. is_equivalence: true + +- id: effective_regular_congruences_definition + assumptions: + - effective regular congruences + conclusions: + - binary powers + proof: This is part of the definition. + +- id: effective_congruences_imply_regular_effective_congruences + assumptions: + - effective congruences + - binary powers + conclusions: + - effective regular congruences + proof: This is trivial. + +- id: regular_effective_congruences_epi-regular_imply_effective_congruences + assumptions: + - effective regular congruences + - epi-regular + conclusions: + - effective congruences + proof: This is trivial. diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index 7005353db..306c8494a 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -85,3 +85,14 @@ - regular subobject classifier proof: This is true by definition. is_equivalence: true + +- id: quasitopos_effective_regular_congruences + assumptions: + - regular subobject classifier + - cartesian closed + conclusions: + - effective regular congruences + proof: >- + Let $E \hookrightarrow X \times X$ be the regular monomorphism corresponding to a regular congruence $q_1, q_2 : E \rightrightarrows X$. This further corresponds to a characteristic morphism $X\times X \to \Omega$, and furthermore to a morphism $X \to [X, \Omega]$ which we will call $[\cdot]_E$. (In the case of $\Set$ this corresponds to the function sending $x\in X$ to its equivalence class with respect to $E$.) + + As in the case of $\Set$, we can show that $q_1, q_2 : E \rightrightarrows X$ is the kernel pair of $[\cdot]_E$. diff --git a/database/data/category-properties/effective cocongruences.yaml b/database/data/category-properties/effective cocongruences.yaml index 6c053dd70..93b12333c 100644 --- a/database/data/category-properties/effective cocongruences.yaml +++ b/database/data/category-properties/effective cocongruences.yaml @@ -9,6 +9,7 @@ dual: effective congruences invariant_under_equivalences: true related: + - effective regular cocongruences - conormal - coquotients of cocongruences - epi-regular diff --git a/database/data/category-properties/effective congruences.yaml b/database/data/category-properties/effective congruences.yaml index b572cb05d..06514f3b7 100644 --- a/database/data/category-properties/effective congruences.yaml +++ b/database/data/category-properties/effective congruences.yaml @@ -9,6 +9,7 @@ dual: effective cocongruences invariant_under_equivalences: true related: + - effective regular congruences - mono-regular - normal - quotients of congruences diff --git a/database/data/category-properties/effective regular cocongruences.yaml b/database/data/category-properties/effective regular cocongruences.yaml new file mode 100644 index 000000000..b1d3a84db --- /dev/null +++ b/database/data/category-properties/effective regular cocongruences.yaml @@ -0,0 +1,16 @@ +id: effective regular cocongruences +relation: has +description: >- + Say a cocongruence $j_1, j_2 : X \rightrightarrows E$ in a category with binary copowers is regular if the epimorphism $(j_1; j_2) : X + X \twoheadrightarrow E$ is in fact a regular epimorphism. + + A category has effective regular congruences if it has binary copowers, and every regular cocongruence in the category is effective (see here for definition). +nlab_link: null +dual: effective regular congruences +invariant_under_equivalences: true + +related: + - effective cocongruences + - cokernel pairs + +tags: + - congruences diff --git a/database/data/category-properties/effective regular congruences.yaml b/database/data/category-properties/effective regular congruences.yaml new file mode 100644 index 000000000..2bc0b38ad --- /dev/null +++ b/database/data/category-properties/effective regular congruences.yaml @@ -0,0 +1,16 @@ +id: effective regular congruences +relation: has +description: >- + Say a congruence $q_1, q_2 : E \rightrightarrows X$ in a category with binary powers is regular if the monomorphism $(q_1, q_2) : E \hookrightarrow X \times X$ is in fact a regular monomorphism. + + A category has effective regular congruences if it has binary powers, and every regular congruence in the category is effective (see here for definition). +nlab_link: null +dual: effective regular cocongruences +invariant_under_equivalences: true + +related: + - effective congruences + - kernel pairs + +tags: + - congruences From 9ffbc24e3215690906b960b05cccef85d7abc453 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sun, 11 Oct 2026 16:30:20 -0400 Subject: [PATCH 2/3] Fix typo; update the property implication with proof to be merged in --- database/data/categories/Cat.yaml | 2 +- database/data/category-implications/congruences.yaml | 5 ++--- .../category-properties/effective regular cocongruences.yaml | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index bd273d040..7ca234742 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -59,7 +59,7 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Cat$ that maps a set to its discrete category. - - property: effective regular cocongruences + - property: effective cocongruences proof: >- The counterexample is similar to the one for $\Mon$: Let $X$ be the walking idempotent, and let $E$ be the delooping of the monoid with presentation $$\langle p, q \mid p^2=p,\, q^2=q,\, pq=q,\, qp=p \rangle.$$ diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 1c1737ec3..bab8c74b0 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -127,11 +127,10 @@ Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is treated in Borceux–Bourn, Example 2.2.18. An alternative proof of this special case is given later in A.5.17. -- id: regular_extensive_consequences +- id: extensive_equalizers_consequences assumptions: - - regular - extensive - - quotients of congruences + - equalizers conclusions: - effective regular cocongruences proof: (For now, will leave this as a placeholder for a reference to the proof to be merged in from PR 373.) diff --git a/database/data/category-properties/effective regular cocongruences.yaml b/database/data/category-properties/effective regular cocongruences.yaml index b1d3a84db..9c606c157 100644 --- a/database/data/category-properties/effective regular cocongruences.yaml +++ b/database/data/category-properties/effective regular cocongruences.yaml @@ -3,7 +3,7 @@ relation: has description: >- Say a cocongruence $j_1, j_2 : X \rightrightarrows E$ in a category with binary copowers is regular if the epimorphism $(j_1; j_2) : X + X \twoheadrightarrow E$ is in fact a regular epimorphism. - A category has effective regular congruences if it has binary copowers, and every regular cocongruence in the category is effective (see here for definition). + A category has effective regular cocongruences if it has binary copowers, and every regular cocongruence in the category is effective (see here for definition). nlab_link: null dual: effective regular congruences invariant_under_equivalences: true From 494cc46be375e2d8896394fef244bdab95dc2e0c Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sun, 11 Oct 2026 16:37:06 -0400 Subject: [PATCH 3/3] Revert accidental deletion of an assignment --- database/data/categories/Cat.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 7ca234742..cc24d2f7b 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -45,6 +45,9 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism, but not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. + - property: regular + proof: See Example 3.14 at the nLab. + - property: coregular proof: 'We already know that $\Mon$ is not coregular; in fact we have shown that there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' references: