Add results on effective congruences

Author: dschepler

databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql

@@ -37,8 +37,8 @@ VALUES
 (
 	'reflexive_pair_trivial',
 	'["left cancellative"]',
-	'["reflexive coequalizers", "coreflexive equalizers"]',
-	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
+	'["reflexive coequalizers", "coreflexive equalizers", "effective congruences", "effective cocongruences"]',
+	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of the identity morphism on the target, and the cokernel pair of the identity morphism on the source.',
 	FALSE
 ),
 (
@@ -192,8 +192,8 @@ VALUES
 (
 	'core-hin_quotients',
 	'["core-thin"]',
-	'["quotients of congruences"]',
-	'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer.',
+	'["quotients of congruences", "effective congruences"]',
+	'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \id$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \id$ and $p_2 \circ r \circ p_1 = p_2 \circ \id$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \id$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\id_X$.',
 	FALSE
 ),
 (
@@ -230,4 +230,4 @@ VALUES
 	'["subobject-trivial"]',
 	'This is because a monomorphism which is also a regular epimorphism is an isomorphism.',
 	FALSE
-);
+);

databases/catdat/data/004_category-implications/005_additional-structure-implications.sql

@@ -27,6 +27,30 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
+(
+	'preadditive_kernels_normal_imply_effective_congruences',
+	'["preadditive", "kernels", "normal"]',
+	'["effective congruences"]',
+	'Let $f, g : E \rightrightarrows X$ be a congruence. Then let $E_0$ be the kernel of $g$. We see that $f|_{E_0} : E_0 \to X$ is a monomorphism. Let $f|_{E_0}$ be the kernel of a morphism $h : X \to Y$. We claim that $E$ is also the kernel pair of $h$.<br>
+	To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$. Then we have
+	$$\begin{align*}
+	(x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\
+	& \iff x_1 - x_2 \in E_0 \\
+	& \iff h(x_1 - x_2) = 0 \\
+	& \iff h(x_1) = h(x_2).
+	\end{align*}$$
+	In particular, applying the forward implications in the case $T := E$, $x_1 := f$, $x_2 := g$, we conclude that $h \circ f = h \circ g$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square.',
+	FALSE
+),
+(
+	'additive_effective_congruences_imply_normal',
+	'["additive", "finitely complete", "effective congruences"]',
+	'["normal"]',
+	'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 $\mathbf{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$.',
+	FALSE
+),
 (
 	'additive_definition',
 	'["additive"]',
@@ -110,4 +134,4 @@ VALUES
 	'["trivial"]',
 	'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.',
 	FALSE
-);
+);

databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql

@@ -223,10 +223,17 @@ VALUES
 	'This follows from one of equivalent formulations of multi-algebraic categories.',
 	TRUE
 ),
+(
+	'multi-algebraic_implies_effective_congruences',
+	'["multi-algebraic"]',
+	'["effective congruences"]',
+	'This is Thm. 4.0 in <a href="https://doi.org/10.1007/BF01224953" target="_blank">Yves Diers, Catégories Multialgébriques</a> or <a href="https://translations.thosgood.net/ADM-34-1980-193.pdf" target="_blank">its English translation</a>.',
+	FALSE
+),
 (
 	'locally-finitely-multi-presentable_stable-monos',
 	'["locally finitely multi-presentable"]',
 	'["filtered-colimit-stable monomorphisms"]',
 	'Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.',
 	FALSE
-);
+);

databases/catdat/data/004_category-implications/008_topos-theory-implications.sql

@@ -121,8 +121,8 @@ VALUES
 (
 	'topos_consequence',
 	'["elementary topos"]',
-	'["finitely cocomplete", "disjoint finite coproducts", "epi-regular"]',
-	'See <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.',
+	'["finitely cocomplete", "disjoint finite coproducts", "epi-regular", "effective congruences"]',
+	'See <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8; and <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Proposition 2.4.1.',
 	FALSE
 ),
 (
@@ -167,6 +167,41 @@ VALUES
 	'This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, A2.6.3 (for every quasitopos).',
 	FALSE
 ),
+(
+	'regular_effective_congruences_implies_quotients',
+	'["regular", "effective congruences"]',
+	'["quotients of congruences"]',
+	'We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient.',
+	FALSE
+),
+(
+	'regular_epi-regular_extensive_consequences',
+	'["regular", "epi-regular", "extensive"]',
+	'["effective cocongruences", "co-Malcev"]',
+	'Suppose we have a coreflexive corelation
+	$$X+X'' \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$
+	on $X$, where we let $X''$ be an isomorphic copy of $X$ for clarity below. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. That means that for a generalized element $x \in X(T)$, $x \in Y(T)$ if and only if $p(x) = p(x'')$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer $K$ of
+	$$p \circ \pi_1,\, p\circ \pi_2 : (X+X'') \times (X+X'') \rightrightarrows E,$$
+	where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X'') \times (X+X'')$, i.e. the four copies of $X \times X$.<br>
+	On the $X\times X$ quadrant, for generalized elements $x_1, x_2 \in X(T)$, we have $(x_1, x_2) \in K(T)$ if and only if $p(x_1) = p(x_2)$. Since $p\circ i_1$ is a split monomorphism, this is equivalent to $x_1 = x_2$. Thus, the $X\times X$ quadrant of $K$ is the diagonal of $X$. On the $X\times X''$ quadrant, we have $(x_1, x_2'')\in K(T)$ if and only if $p(x_1) = p(x_2'')$. Since $r(p(x_1)) = x_1$ and $r(p(x_2'')) = x_2$, this condition implies $x_1 = x_2$; and then by definition of $Y$, $x_1 = x_2 \in Y(T)$. The converse is straightforward. Thus, the $X\times X''$ quadrant of $K$ is the diagonal of $Y$. Similarly, the $X''\times X$ quadrant of $K$ is the diagonal of $Y$, and the $X''\times X''$ quadrant of $K$ is the diagonal of $X$.<br>
+
+	Thus, we get that a morphism $h : X+X'' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y'')$ for every $y \in Y$; $h(y'') = h(y)$ for every $y\in Y$; and $h(x'') = h(x'')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y'')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \operatorname{inc}_Y$ and $i_2 \circ \operatorname{inc}_Y$. This means that $E$ is an effective cocongruence.<br><br>
+
+	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 Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof of this special case is given later in A.5.17.',
+	FALSE
+),
+(
+	'pretopos_balanced',
+	'["effective congruences", "extensive"]',
+	'["mono-regular"]',
+	'Let $\alpha : A \hookrightarrow B$ be a monomorphism. Let $B''$ be a copy of $B$, and likewise let $A''$ be a copy of $A$. Consider the congruence on $B + B''$ generated by $y \sim y''$ for $y \in A$. Formally, we define $E := B + B'' + A + A''$ and define the two morphisms $f, g : E \rightrightarrows B + B''$ by extending the identity on $B + B''$ and
+	$$\begin{align*}
+	f(y) & = \alpha(y), & f(y'') & = \alpha(y)'', \\
+	g(y) & = \alpha(y)'', & g(y'') & = \alpha(y),
+	\end{align*}$$
+	on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B'' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B''$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x'')$ if and only if $x = f(e)$, $x'' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$.',
+	FALSE
+),
 (
 	'lcc_implies_extensive',
 	'["locally cartesian closed", "disjoint finite coproducts"]',
@@ -181,18 +216,11 @@ VALUES
 	'The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the <a href="https://ncatlab.org/nlab/show/extensive+category" target="_blank">nLab</a>.',
 	FALSE
 ),
-(
-	'topos_is_co-malcev',
-	'["elementary topos"]',
-	'["co-Malcev"]',
-	'This is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof is given later in A.5.17.',
-	FALSE
-),
 (
 	'subobject_classifier_disallows_malcev',
 	'["subobject classifier", "Malcev"]',
-	'["thin"]',
-	'The subobject classifier $\Omega$ is an internal poset (cf. <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. Applying this to equalizers, we see that the category is thin. (And from here, we can infer that it is trivial.)',
+	'["subobject-trivial"]',
+	'The subobject classifier $\Omega$ is an internal poset (cf. <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. (From here, we can infer that the category is trivial.)',
 	FALSE
 ),
 (
@@ -236,4 +264,4 @@ VALUES
 	'["trivial"]',
 	'Let $N := \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n''$ we have $N_{\geq n''} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.',
 	FALSE
-);
+);

databases/catdat/data/009_lemmas/001_lemmas.sql

@@ -129,4 +129,36 @@ INSERT INTO lemmas (
     'Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence',
     'Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms.',
     'Suppose we have a sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Define $Y$ to be the coproduct of all $X_n$. Now for each $m\le n$, define $E_{m,n} := X_m$ with two maps $i_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y$, and similarly for $m \ge n$ define $E_{m,n} := X_n$ with two maps $i_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y$. Then the coproduct of all $E_{m,n}$, with the induced morphisms to $Y$, forms a congruence. Here to prove the maps are jointly monomorphic, and again in proving transitivity, we use extensivity to split the domain of the generalized elements of $\sum_{m,n=1}^\infty E_{m,n}$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence.'
+),
+(
+    'effective-congruence-quotients',
+    'Quotients of effective congruences are strict quotients',
+    'Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square
+    $$\begin{CD}
+    E @> f >> X \\
+    @V g VV  @VV p V \\
+    X @>> p > X/E.
+    \end{CD}$$',
+    'Suppose we have $h : X \to Z$ so that we have a cartesian square
+    $$\begin{CD}
+    E @> f >> X \\
+    @V g VV  @VV h V \\
+    X @>> h > Z.
+    \end{CD}$$
+    Then by the universal property of the coequalizer, there is a unique morphism $$\bar h : X/E \to Z$$
+    such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then
+    $$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$
+    so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic.'
+),
+(
+    'coslice-effective-congruences',
+    'Inheritance of effective congruences in coslice categories',
+    'Let $\mathcal{C}$ be an extensive category, and $A$ an object of $\mathcal{C}$. If the coslice category $A \backslash \mathcal{C}$ has effective congruences, then so does $\mathcal{C}$.',
+    'Let $f, g : E \rightrightarrows X$ be a congruence in $\mathcal{C}$. We then construct a congruence on $A+X$ in $A \backslash \mathcal{C}$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps
+    $$\mathrm{id}_A + f,\, \mathrm{id}_A + g : A+E \rightrightarrows A+X$$
+    form a congruence. To show the pair of maps is jointly monomorphic, we use extensivity to split the domains of the generalized elements, so without loss of generality we may assume each comes from either $A$ or $E$. Reflexivity and symmetry are straightforward; and for transitivity, we again use extensivity to split the domains of the generalized elements, and provide an argument on each subdomain where the three generalized elements all come from either $A$ or $E$.<br>
+    Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \mathcal{C}$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\mathcal{C}$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a map pair
+    $$\mathrm{id}_A + x_1,\, \mathrm{id}_A + x_2 : A+T \rightrightarrows A+X$$
+    in $A \backslash \mathcal{C}$ with $h \circ (\mathrm{id}_A + x_1) = h \circ (\mathrm{id}_A + x_2)$. Therefore, $\mathrm{id}_A + x_1, \mathrm{id}_A + x_2$ factors through $A+E$ in $A \backslash \mathcal{C}$, so $x_1, x_2$ factors through $A+E$ in $\mathcal{C}$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$.'
 );
+