Add property of every regular congruence being effective (and its dual)

database/data/categories/Alg(R).yaml

@@ -72,7 +72,7 @@ unsatisfied_properties:
   - property: cofiltered-limit-stable epimorphisms
     proof: We already know that <a href="/category/CAlg(R)">$\CAlg(R)$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488">MSE/5133488</a>.
 
-  - property: effective cocongruences
+  - property: effective regular cocongruences
     proof: '<a href="https://mathoverflow.net/a/510809">MO/510744</a> 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:

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 <a href="https://mathoverflow.net/a/510809">MO/510744</a> 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*}$$

database/data/categories/SemiGrp.yaml

@@ -58,7 +58,7 @@ unsatisfied_properties:
   - property: cofiltered-limit-stable epimorphisms
     proof: We already know that <a href="/category/Set">$\Set$</a> does not have this property (by <a href="/category-implication/topos_no_stable_epis">this result</a>). Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> 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 <a href="/category/Mon">$\Mon$</a>, i.e. we adapt the counterexample from <a href="https://mathoverflow.net/a/510809">MO/510744</a>. 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*}$$

database/data/category-implications/congruences.yaml

@@ -127,6 +127,14 @@
 
     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 <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories">Borceux–Bourn</a>, Example 2.2.18. An alternative proof of this special case is given later in A.5.17.
 
+- id: extensive_equalizers_consequences
+  assumptions:
+    - extensive
+    - 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.)
+
 - id: pretopos_balanced
   assumptions:
     - effective congruences
@@ -153,3 +161,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.

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$.

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

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

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 <i>regular</i> if the epimorphism $(j_1; j_2) : X + X \twoheadrightarrow E$ is in fact a regular epimorphism.
+
+  A category <i>has effective regular cocongruences</i> if it has binary copowers, and every regular cocongruence in the category is effective (see <a href="/category-property/effective cocongruences">here</a> for definition).
+nlab_link: null
+dual: effective regular congruences
+invariant_under_equivalences: true
+
+related:
+  - effective cocongruences
+  - cokernel pairs
+
+tags:
+  - congruences

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 <i>regular</i> if the monomorphism $(q_1, q_2) : E \hookrightarrow X \times X$ is in fact a regular monomorphism.
+
+  A category <i>has effective regular congruences</i> if it has binary powers, and every regular congruence in the category is effective (see <a href="/category-property/effective congruences">here</a> for definition).
+nlab_link: null
+dual: effective regular cocongruences
+invariant_under_equivalences: true
+
+related:
+  - effective congruences
+  - kernel pairs
+
+tags:
+  - congruences