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/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..bab8c74b0 100644 --- a/database/data/category-implications/congruences.yaml +++ b/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 Borceux–Bourn, 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. 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..9c606c157 --- /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 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 + +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