Coequalizers of kernel pairs

.cspell.json

@@ -77,6 +77,7 @@
 		"codistributivity",
 		"codomain",
 		"codomains",
+		"coequalize",
 		"coequalized",
 		"coequalizer",
 		"coequalizers",
@@ -95,6 +96,7 @@
 		"cogenerator",
 		"cogenerators",
 		"Cohomology",
+		"coimage",
 		"cokernel",
 		"cokernels",
 		"colimit",

content/monic_sequential_colimits.md

@@ -0,0 +1,46 @@
+---
+title: The colimit of a sequence of monomorphisms
+description: We find conditions under which a countably extensive category has colimits of sequences of monomorphisms.
+---
+
+## The colimit of a sequence of monomorphisms
+
+::: Lemma 1
+Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms.
+:::
+
+::: Proof
+Suppose we have a sequence $X_0 \hookrightarrow X_1 \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} \coloneqq 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} \coloneqq 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 that the maps are jointly monomorphic, and again when proving transitivity, we use extensivity to split the domain of the generalized elements of $\coprod_{m,n \geq 0}^\infty E_{m,n}$ so that, without loss of generality, we may assume that each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence.
+:::
+
+::: Lemma 2
+Let $\C$ be a countably extensive category with coequalizers of kernel pairs. Assume that $X_0 \hookrightarrow X_1 \hookrightarrow \cdots$ is a sequence of monomorphisms that has a cocone $(X_n \hookrightarrow Y)$ consisting of monomorphisms. Then this sequence has a colimit.
+:::
+
+::: Proof
+We consider the morphism $\coprod_{n \geq 0} X_n \to Y$ induced by the monomorphisms $X_n \hookrightarrow Y$. By assumption, its kernel pair $\coprod_{n \geq 0} X_n \times_Y \coprod_{n \geq 0} X_n$ exists, and the two projections to $\coprod_{n \geq 0} X_n$ have a coequalizer. We will prove that this coequalizer is a colimit of the sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$. For this, it suffices to find a natural bijection between cocones $(h_n : X_n \to T)_{n \geq 0}$ and morphisms $h : \coprod_{n \geq 0} X_n \to T$ that coequalize the two projections, where $T \in \C$ is any object.
+
+A morphism $h : \coprod_{n \geq 0} X_n \to Y$ is equivalent to a family of morphisms $(h_n : X_n \to T)_{n \geq 0}$. Since $\C$ is countably extensive, the canonical morphism
+$$\textstyle \coprod_{n,m \geq 0} X_n \times_Y X_m \to \coprod_{n \geq 0} X_n \times_Y \coprod_{m \geq 0} X_m$$
+is an isomorphism. Hence, $h$ coequalizes the two projections if and only if for all $n,m \geq 0$ the diagram
+
+$$
+\begin{CD}
+X_n \times_Y X_m @>>> X_n \\
+@VVV @VVV \\
+X_m @>>> T
+\end{CD}
+$$
+
+commutes. Without loss of generality, we may assume $n \leq m$. But then $X_n \times_Y X_m \cong X_n$, and the diagram simplifies to
+
+$$
+\begin{CD}
+X_n @>{=}>> X_n \\
+@VVV @VVV \\
+X_m @>>> T,
+\end{CD}
+$$
+
+which is precisely the cocone condition for $(h_n : X_n \to T)_{n \geq 0}$.
+:::

content/subcategories.md

@@ -86,15 +86,17 @@ The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${
 :::
 
 ::: Lemma 7
-Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves pullbacks and coequalizers. If $\D$ is regular, then so is $\C$.
+Let $U : \C \to \D$ be a functor preserving pullbacks. Assume that $\D$ is regular and that $\C$ has finite limits and coequalizers of kernel pairs. If $U$ preserves and reflects regular epimorphisms, then $\C$ is regular. Moreover, this condition is satisfied when $U$ is conservative and preserves coequalizers.
 :::
 
 ::: Proof
-Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullbacks in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram
-$$X \times_Y X \rightrightarrows X \to \im(f) \xrightarrow{i} Y$$
-where $X \times_Y X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
-$$UX \times_{UY} UX \rightrightarrows UX \to \im(Uf) \xrightarrow{Ui} UY$$
-where $UX \times_{UY} UX$ is the kernel pair of $Uf$, and $\im(Uf)$ is the coequalizer. Since $Uf$ is a regular epimorphism, we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $f$ is a regular epimorphism.
+Since $\C$ has finite limits and coequalizers of kernel pairs, it remains to prove that regular epimorphisms are stable under pullbacks in $\C$. Assume first that $U$ preserves and reflects regular epimorphisms. If $X \to Y$ is a regular epimorphism and $Z \to Y$ is any morphism in $\C$, then $U(X) \to U(Y)$ is a regular epimorphism, and therefore also $U(X) \times_{U(Y)} U(Z) \to U(Z)$ is a regular epimorphism. Since $U$ preserves pullbacks, this identifies with $U(X \times_Y Z) \to U(Z)$, the image under $U$ of $X \times_Y Z \to Z$. Since $U$ reflects regular epimorphisms, it follows that $X \times_Y Z \to Z$ is a regular epimorphism, finishing the proof.
+
+Now assume that $U$ is conservative and preserves coequalizers. Then it clearly preserves regular epimorphisms. Conversely, suppose that $f : X \to Y$ is a morphism in $\C$ such that $U(f)$ is a regular epimorphism. Then in $\C$ we have the diagram
+$$X \times_Y X \rightrightarrows X \xrightarrow{p} \im(f) \xrightarrow{i} Y$$
+where $X \times_Y X \rightrightarrows X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions on $U$, its image is equivalent to the diagram in $\D$:
+$$U(X) \times_{U(Y)} U(X) \rightrightarrows U(X) \xrightarrow{U(p)} U(\im(f)) \xrightarrow{U(i)} U(Y)$$
+where $U(X) \times_{U(Y)} U(X)$ is the kernel pair of $U(f)$, and $U(\im(f))$ is the coequalizer. Since $U(f)$ is a regular epimorphism and $\D$ is regular, we must have that $U(i)$ is an isomorphism. Since $U$ is conservative, $i$ is an isomorphism as well, so $f$ is a regular epimorphism.
 :::
 
 ::: Lemma 8

database/data/categories/FinGrp.yaml

@@ -48,7 +48,7 @@ satisfied_properties:
     proof: 'A proof can be found in <a href="https://mathoverflow.net/questions/511516" target="_blank">MO/511516</a>. It even shows that every cocongruence in $\FinGrp$ is trivial. In short, the proof goes like this: We know that <a href="/category/Grp">$\Grp$</a> has effective cocongruences. Using the fact that amalgamated sums of finite groups are residually finite, one can can show that every cocongruence in $\FinGrp$ is also a cocongruence in $\Grp$.'
 
   - property: regular
-    proof: The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.
+    proof: This follows from Lemma 7 <a href="/content/subcategories">here</a> applied to the inclusion functor $\FinGrp \hookrightarrow \Grp$ into the regular category $\Grp$ and the description of regular epimorphisms below.
 
   - property: ℵ₁-cofiltered limits
     proof: For <a href="/category/FinSet">$\FinSet$</a> know that the embedding $\FinSet \hookrightarrow \Set$ is closed under $\aleph_1$-cofiltered limits. From this and the fact that the forgetful functor $\Grp \to \Set$ preserves limits it follows that $\FinGrp \hookrightarrow \Grp$ is closed under $\aleph_1$-cofiltered limits.

database/data/categories/Grp_c.yaml

@@ -56,7 +56,7 @@ satisfied_properties:
       - grp_malcev
 
   - property: regular
-    proof: We already know that the category is finitely complete, and that it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.
+    proof: This follows from Lemma 7 <a href="/content/subcategories">here</a> applied to the inclusion functor $\Grp_\c \hookrightarrow \Grp$ into the regular category $\Grp$ and the description of regular epimorphisms below.
 
   - property: effective congruences
     proof: 'A congruence on a countable group $G$ has the form $\{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.'

database/data/categories/Met_c.yaml

@@ -97,37 +97,8 @@ unsatisfied_properties:
   - property: ℵ₁-filtered colimits
     proof: See <a href="https://mathoverflow.net/questions/511433" target="_blank">MO/511433</a> for a proof that the diagram $\omega_1 \to \Met_c$, $\alpha \mapsto \IR^\alpha$ does not have a colimit.
 
-  - property: regular
-    proof: >-
-      We will find a morphism $f : X \to Y$ in $\Met_c$ whose kernel pair has no coequalizer. The idea is to represent the <a href="https://doi.org/10.1016/0166-8641(95)00016-X" target="_blank">sequential fan</a> $S_\omega$ as such a coequalizer in $\Top$, and generalize the diagonal argument showing that it is not metrizable.
-
-
-      For $n \geq 1$ consider the subspace
-      $$S_n \coloneqq \{1/k : k \geq 1\} \cup \{0\}$$
-      of $\IR$, so that $\Hom(S_n,Y)$ corresponds to convergent sequences in $Y$. Each $S_n$ has diameter $1$, so we can endow the coproduct space
-      $$X \coloneqq \textstyle\coprod_n S_n$$
-      with a metric that extends the metric on each $S_n$ and in which points in $S_n$ and $S_m$ for $n \neq m$ have distance $1$. The points of $X$ will be written as $(n,x)$, where $x \in S_n$. If $p_n$ denotes the $n$th prime number, we have $\lim_{k \to \infty} p_n^{-k} = 0$ in $\IR$, so we have a continuous map $S_n \to \IR$ mapping $1/k \mapsto p_n^{-k}$ and $0 \mapsto 0$. Together, these yield a continuous map
-      $$f : X \to \IR, \, (n,0) \mapsto 0, \, (n,1/k) \mapsto p_n^{-k}.$$
-      Let $\pi_1,\pi_2 : E \rightrightarrows X$ be the kernel pair of $f$. Since $p_n^{-k}$ completely determines $n$ and $k$, $E$ consists precisely of the diagonal and all $((n,0),(m,0))$ for $n,m \geq 1$. Thus, the coequalizer of $\pi_1,\pi_2$ in $\Top$ is the quotient of $X$ that identifies all limit points $(n,0)$ for $n \geq 1$; this space is known as the sequential fan $S_\omega$.
-
-
-      Now assume that $\pi_1,\pi_2$ have a coequalizer $q : X \to Q$ in $\Met_c$, i.e. the universal continuous map from $X$ into a metrizable space such that the point
-      $$0_Q \coloneqq q(n,0) \in Q$$
-      does not depend on the choice of $n$. Since $Q$ is metrizable, there is a countable decreasing neighborhood basis $(B_m)_{m \geq 1}$ of $0_Q \in Q$. Then $U_m \coloneqq q^{-1}(B_m)$ is an open neighborhood of $(n,0) \in X$ for any $n$, and in particular of $(m,0)$. Hence, $U_m \cap S_m$ contains almost all points of $S_m$. In particular, we may choose a point $x_m \in U_m \cap S_m$ that is isolated in $S_m$.
-
-
-      Define the subset $A \coloneqq \{x_m : m \geq 1\}$ of $X$ and let $g : X \to \IR$ be its characteristic function, so that $g(a)=1$ for $a \in A$ and $g(x) = 0$ for $x \in X \setminus A$. To show that $g$ is continuous, it suffices to consider each restriction $g|_{S_m} : S_m \to \IR$. This is the characteristic function of the isolated point $x_m \in S_m$, hence continuous.
-
-
-      Since $g(n,0) = 0$ for all $n \geq 1$, there is a unique continuous map $\tilde{g} : Q \to \IR$ satisfying $\tilde{g} \circ q = g$. The points $q(x_m)$ in $Q$ converge to $0_Q$ because for all $k \geq m$ we have $x_k \in U_k$, hence $q(x_k) \in B_k \subseteq B_m$. Since $\tilde{g}$ is continuous, it follows that $\tilde{g}(q(x_m)) = g(x_m) = 1$ converges to $\tilde{g}(0_Q) = \tilde{g}(q(n,0)) = g(n,0) = 0$, which is a contradiction.
-
-
-      Sketch of an alternative proof: Consider the coproduct $X \coloneqq \coprod_n \IR^n$ in $\Met_c$. The canonical inclusions $\IR^n \to \ell^2$ into the Hilbert space of square-summable sequences yield a continuous map $f : X \to \ell^2$. A coequalizer of the kernel pair of $f$ would be a colimit of the sequence
-      $$\IR \hookrightarrow \IR^2 \hookrightarrow \IR^3 \cdots$$
-      where each map appends a zero coordinate, and we have seen above that this sequential colimit does not exist.
-
-  - property: quotients of congruences
-    proof: In the previous proof we have constructed a morphism whose kernel pair does not have a coequalizer, and every kernel pair is a congruence.
+  - property: coequalizers of kernel pairs
+    proof: The sequence of embeddings $\IR^1 \hookrightarrow \IR^2 \hookrightarrow \IR^3 \hookrightarrow \cdots$, where each map appends a zero coordinate, has no colimit by <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>. It has a cocone consisting of the embeddings $\IR^n \hookrightarrow \ell^2$, $x \mapsto (x,0,0,\dotsc)$, where $\ell^2$ is the Hilbert space of square-summable sequences. Since $\Met_c$ is infinitary extensive, it follows from Lemma 2 <a href="/content/monic_sequential_colimits">here</a> that $\Met_c$ does not have coequalizers of kernel pairs.
 
 special_objects:
   initial object:

database/data/categories/Sch_R.yaml

@@ -58,12 +58,19 @@ unsatisfied_properties:
   - property: cokernel pairs
     proof: Choose a residue field $K$ of $R$. Then the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout; see <a href="https://mathoverflow.net/questions/9961" target="_blank">MO/9961</a>.
 
-  - property: quotients of congruences
-    proof: If $\Sch_R$ had quotients of congruences, then by <a href="/content/pushouts-of-monos-via-congruence-quotients">this lemma</a> it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout where $K$ is a residue field of $R$; see <a href="https://mathoverflow.net/questions/9961" target="_blank">MO/9961</a>.
-
   - property: sequential colimits
     proof: It is shown in <a href="https://mathoverflow.net/questions/511944" target="_blank">MO/511944</a> that the diagram $$\IA^1_R \hookrightarrow \IA^2_R \hookrightarrow \IA^3_R \hookrightarrow \cdots$$ has no colimit.
 
+  - property: coequalizers of kernel pairs
+    proof: >-
+      We have a diagram of closed immersions of affine spaces
+      $$\begin{array}{cccc}
+      \IA^1_R & \to & \IA^2_R & \to ~ \cdots \\[1ex]
+      \downarrow & \swarrow & & \\[1ex]
+      \IA^\infty_R, &&&
+      \end{array}$$
+      where $\IA^n_R = \Spec(R[X_1,\dotsc,X_n])$ and $\IA^\infty_R = \Spec(R[X_1,X_2,\dotsc])$. By <a href="https://mathoverflow.net/questions/511944" target="_blank">MO/511944</a>, the sequence $\IA^1_R \hookrightarrow \IA^2_R \hookrightarrow \cdots$ has no colimit. Moreover, we already know that $\Sch_R$ is infinitary extensive. Hence, Lemma 2 <a href="/content/monic_sequential_colimits">here</a> implies that $\Sch_R$ does not have coequalizers of kernel pairs. Specifically, the kernel pair of $\coprod_{n \geq 0} \IA^n_R \to \IA^\infty_R$ has no coequalizer.
+
 special_objects:
   initial object:
     description: empty scheme

database/data/categories/Set_c.yaml

@@ -52,10 +52,10 @@ satisfied_properties:
     proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that <a href="/category/Set">$\Set$</a> has effective congruences (as does every topos). Using <a href="/content/effective-congruence-quotients">this result</a>, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects limits</a>. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.'
 
   - property: regular
-    proof: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullbacks since this holds in <a href="/category/Set">$\Set$</a> and both regular epimorphisms (they are surjective maps) and pullbacks coincide.
+    proof: This follows from Lemma 7 <a href="/content/subcategories">here</a> applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the regular category $\Set$ and the description of regular epimorphisms below.
 
   - property: coregular
-    proof: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushouts since this holds in <a href="/category/Set">$\Set$</a> and both regular monomorphisms (they are injective maps) and pushouts coincide.
+    proof: This follows from the dual of Lemma 7 <a href="/content/subcategories">here</a> applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the coregular category $\Set$ and the description of regular monomorphisms below.
 
 unsatisfied_properties:
   - property: small

database/data/categories/Set_pointed.yaml

@@ -32,10 +32,6 @@ satisfied_properties:
     proof: The pointed set $(\{0,1\},1)$ is a cogenerator.
     label: set_*_cogenerator
 
-  - property: coregular
-    proof: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for <a href="/category/Set">$\Set$</a> and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts.
-    check_redundancy: false
-
   - property: co-Malcev
     proof: Malcev categories are closed under slice categories by Prop. 2.2.14 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>. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of <a href="/category/Set">$\Set$</a>, which is co-Malcev since every elementary topos is co-Malcev.
 

database/data/categories/Setne.yaml

@@ -39,6 +39,9 @@ satisfied_properties:
   - property: binary coproducts
     proof: The disjoint union of two non-empty sets is non-empty.
 
+  - property: equalizers of cokernel pairs
+    proof: 'Let $f : X \to Y$ be a map of non-empty sets. The cokernel pair $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$ in <a href="/category/Set">$\Set$</a> is clearly also a cokernel pair in $\Setne$. Moreover, the equalizer of $i_1,i_2$ in $\Set$ is non-empty because it contains the elements of $X$.'
+
   - property: mono-regular
     proof: This follows easily from the fact that <a href="/category/Set">$\Set$</a> is mono-regular.
 
@@ -79,9 +82,6 @@ unsatisfied_properties:
   - property: coquotients of cocongruences
     proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ &mdash; namely the cofull cocongruence on $\{0\}$ &mdash; but they do not have an equalizer.
 
-  - property: effective cocongruences
-    proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ &mdash; namely the cofull cocongruence on $\{0\}$ &mdash; but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square.
-
   - property: coaccessible
     proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to <a href="/category/Set_*">$\Set_*$</a>, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in op. cit.).