diff --git a/databases/catdat/data/categories/FreeAb.yaml b/databases/catdat/data/categories/FreeAb.yaml
index 5a0cd19c..de14a680 100644
--- a/databases/catdat/data/categories/FreeAb.yaml
+++ b/databases/catdat/data/categories/FreeAb.yaml
@@ -54,11 +54,6 @@ unsatisfied_properties:
- property: sequential colimits
reason: See MO/509715.
- - property: effective cocongruences
- reason: |-
- We will let $E$ be the abelian group with presentation $\langle a, b, c \mid a - b = 2c \rangle$, with two morphisms $\IZ \rightrightarrows E$ given by $1\mapsto a$, $1\mapsto b$. Note that $E$ is free with basis $\{ b, c \}$. Then $\Hom(E, G) \cong \{ (x, y, z) \in G^3 \mid x - y = 2z \}$. Observe that since $G$ is torsion-free, the projection onto the first two coordinates is injective; and $(x, y)$ is in the image precisely when $x \equiv y \pmod{2G}$, which gives an equivalence relation. Therefore, $E$ gives a cocongruence on $\IZ$.
- On the other hand, if $E$ were the cokernel pair of $h : H \to \IZ$, that would mean that for $x, y : \IZ \to G$, $x \equiv y \pmod{2G}$ if and only if $x \circ h = y \circ h$. In particular, from the case $G := \IZ$, $x := 2 \id$, $y := 0$, we would have $2h = 0$. That implies $h = 0$, but then that would give $\id_{\IZ} \equiv 0 \pmod{2}$, resulting in a contradiction.
-
category_property_comments:
- property: accessible
comment: The question if this category is accessible is undecidable in ZFC. See MSE/720885.
diff --git a/databases/catdat/data/category-implications/congruences.yaml b/databases/catdat/data/category-implications/congruences.yaml
index def9ee3a..689225cd 100644
--- a/databases/catdat/data/category-implications/congruences.yaml
+++ b/databases/catdat/data/category-implications/congruences.yaml
@@ -74,13 +74,10 @@
assumptions:
- additive
- effective congruences
- - finitely complete
conclusions:
- normal
reason: >-
- Let $i : Y \hookrightarrow X$ be a monomorphism. Then the pullback $E$ of
- $$X \times X \xrightarrow{p_1 - p_2} X \xhookleftarrow{~~~i~~~} Y$$
- is a congruence on $X$. This is because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$.
+ Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E := X \times Y$ with maps $f, g : E \rightrightarrows X$ defined by $f : (x, y) \mapsto x+i(y)$ and $g : (x, y) \mapsto x$. It is straightforward to check that $f$ and $g$ are jointly monomorphic. Now $E$ is a congruence because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$.
is_equivalence: false
- id: regular_effective_congruences_implies_quotients