From f494cc2eee4221758a6cf9688cb6781fe084dad8 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Fri, 15 May 2026 17:51:04 -0400 Subject: [PATCH] The pullback assumption for this implication turns out not to be necessary, and allows us to drop an explicit assignment in FreeAb --- databases/catdat/data/categories/FreeAb.yaml | 5 ----- databases/catdat/data/category-implications/congruences.yaml | 5 +---- 2 files changed, 1 insertion(+), 9 deletions(-) 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