Add kernel pairs and cokernel pairs

.cspell.json

@@ -180,6 +180,7 @@
 		"Groupes",
 		"groupoid",
 		"groupoids",
+		"Hanai",
 		"Haus",
 		"hausdorff",
 		"Hertweck",

database/data/categories/BOn.yaml

@@ -96,9 +96,6 @@ unsatisfied_properties:
   - property: sequential colimits
     proof: Assume that the sequence $\bullet \xrightarrow{1} \bullet \xrightarrow{1} \cdots$ has a colimit. This mounts to a (universal) sequence of ordinals $\alpha_n$ with $\alpha_n = \alpha_{n+1} + 1$. But then $\alpha_{n+1} < \alpha_n$, contradicting the fact that $\alpha_0$ is well-ordered.
 
-  - property: pushouts
-    proof: Assume that $1,\omega$ have a pushout. This is a (universal) pair of ordinals $\alpha,\beta$ with $\alpha + 1 = \beta + \omega$. But $\beta + \omega$ is a limit ordinal, while $\alpha + 1$ is not.
-
   - property: cofiltered-limit-stable epimorphisms
     proof: The epimorphisms are the finite ordinals (see below), but the limit of the sequential diagram $\cdots \xrightarrow{1} * \xrightarrow{1} *$ is the ordinal $\omega$ by <a href="https://math.stackexchange.com/questions/5129138">MSE/5129138</a>.
 

database/data/categories/Delta.yaml

@@ -87,6 +87,9 @@ unsatisfied_properties:
   - property: coreflexive equalizers
     proof: 'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ have a common left inverse, the unique map $s^0 : [1] \to [0]$, but are not equalized by any morphism.'
 
+  - property: cokernel pairs
+    proof: Assume that the inclusion $\{0\} \to \{0 < 1\}$ has a cokernel pair in $\FinOrd \setminus \{\varnothing\}$. This would be a universal finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction.
+
   - property: sequential colimits
     proof: We can just copy the proof for <a href="/category/FinOrd">$\FinOrd$</a> to show that the sequence of inclusions $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has no colimit.
     references:
@@ -100,9 +103,6 @@ unsatisfied_properties:
   - property: natural numbers object
     proof: Any natural numbers object in $\FinOrd \setminus \{\varnothing\}$ would also be a natural numbers object in <a href="/category/FinOrd">$\FinOrd$</a>, which we know does not exist.
 
-  - property: pushouts
-    proof: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction.
-
   - property: multi-complete
     proof: >-
       We will prove that the multi-product of $I \coloneqq \{0 < 1\}$ with itself does not exist in $\FinOrd \setminus \{\varnothing\}$. Assume that it does, i.e. there is a family of spans

database/data/categories/FS.yaml

@@ -88,9 +88,6 @@ unsatisfied_properties:
   - property: sequential limits
     proof: 'Let $X_n \coloneqq \{1,\dotsc,n\}$. We define the truncation $p_n : X_{n+1} \to X_n$ by extending the identity of $X_n$ with $p_n(n+1) \coloneqq n$. Assume the sequence of truncations $\cdots \to X_2 \to X_1$ has a limit $(f_n : X \to X_n)$ in this category. But $f_n$ is surjective, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.'
 
-  - property: pullbacks
-    proof: The connected component of non-empty sets has a terminal object, $1$, and it suffices to prove that it has no products. Let $X$ be a finite set with more than $1$ element. Assume that the product $P$ of $X$ with itself exists. The diagonal $X \to P$ is a split monomorphism, hence injective, but also surjective, i.e. an isomorphism. In other words, the two projections $P \rightrightarrows X$ are equal. The universal property of $P$ now implies that every two morphisms $Y \rightrightarrows X$ are equal, which is absurd.
-
   - property: binary copowers
     proof: Assume that the copower $X \coloneqq 2+2$ exists. Since we have a surjective map $2 \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to 2$ shows that $X$ has at least $2$ elements. Thus, $X \cong 2$. For all finite sets $Y$ we get a bijection $\Hom(2,Y) \cong \Hom(2,Y)^2$, in particular the cardinalities are the same. For $Y=2$ this gives the contradiction $2 = 4$.
 

database/data/categories/Fld.yaml

@@ -50,9 +50,6 @@ unsatisfied_properties:
   - property: multi-terminal object
     proof: Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists.
 
-  - property: pushouts
-    proof: 'By <a href="https://math.stackexchange.com/questions/359352/" target="_blank">MSE/359352</a>, the pushout $E \sqcup_K F$ of two field homomorphisms $E \leftarrow K \rightarrow F$ exists if and only if the tensor product $E \otimes_K F$ has a "fieldification": this means that the nilradical is a prime ideal whose quotient ring is a field. This is quite rare: Consider $E = K(X)$, $F = K(Y)$. Then $E \otimes_K F$ is isomorphic to $K[X,Y] (K[X]-\{0\})^{-1} (K[Y]-\{0\})^{-1}$, which is an integral domain but not a field: for example, $X-Y$ has no inverse.'
-
   - property: generator
     proof: Assume that $G$ is a generator, say of characteristic $p$. Then for all $q \neq p$ all homomorphisms between two fields of characteristic $q$ would be equal, which is absurd.
 

database/data/categories/Man.yaml

@@ -81,8 +81,11 @@ unsatisfied_properties:
   - property: countable powers
     proof: 'The power $\IR^{\IN}$ does not exist. More generally, let $(M_n)_{n \geq 0}$ be a sequence of smooth manifolds of positive dimension whose product $(\pi_n : P \to M_n)_{n \geq 0}$ exists. This product cone in $\Man$ yields a product cone in $\Set$ since the forgetful functor $\Man \to \Set$ is representable, hence preserves all limits. Choose points $x_n \in M_n$ with $T_{x_n}(M_n) \neq 0$. Choose the point $x \in P$ with $\pi_n(x) = x_n$. Consider the linear map $T_x(P) \to \prod_{n \geq 0} T_{x_n}(M_n)$ induced by the derivatives $d_x(\pi_n) : T_x(P) \to T_{x_n}(M_n)$. Since $T_x(P)$ is finite-dimensional and $\prod_{n \geq 0} T_{x_n}(M_n)$ is not, it cannot be surjective. But actually, it is: Choose tangent vectors $v_n \in T_{x_n}(M_n)$. Choose smooth curves $\gamma_n : \IR \to M_n$ with $\gamma_n(0)=x_n$ and ${\gamma_n}''(0) = v_n$. By the universal property there is a unique smooth curve $\gamma : \IR \to P$ with $\pi_n \gamma = \gamma_n$. In particular, $\gamma(0) = x$. The chain rule now implies that $\gamma''(0) \in T_x(P)$ is a preimage of $(v_n)$ – a contradiction.'
 
-  - property: pullbacks
-    proof: See <a href="https://math.stackexchange.com/questions/5129579/" target="_blank">MSE/5129579</a> or <a href="https://math.stackexchange.com/questions/322485" target="_blank">MSE/322485</a>.
+  - property: kernel pairs
+    proof: One can show that the map $\IR \to \IR$, $x \mapsto x^2$ does not have a kernel pair, see <a href="https://math.stackexchange.com/a/322602" target="_blank">MSE/322485</a>.
+
+  - property: cokernel pairs
+    proof: The inclusion $\{0\} \to \IR$ does not have a cokernel pair, see <a href="https://mathoverflow.net/questions/19116">MO/19916</a>.
 
   - property: sequential colimits
     proof: If $\Man$ had sequential colimits, then by <a href="/content/special_sequential_colimits">this lemma</a> there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction.
@@ -101,7 +104,7 @@ unsatisfied_properties:
       - setc_no_aleph1-cofiltered_limits
 
   - property: quotients of congruences
-    proof: If $\Man$ had quotients of congruences, then by <a href="/content/pushouts-of-monos-via-congruence-quotients">this lemma</a>, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$.  This contradicts <a href="https://mathoverflow.net/questions/19116">MO/19916</a>.
+    proof: If $\Man$ had quotients of congruences, then by <a href="/content/pushouts-of-monos-via-congruence-quotients">this lemma</a>, it would have a pushout of $\IR \leftarrow \{0\} \rightarrow \IR$. This contradicts <a href="https://mathoverflow.net/questions/19116">MO/19916</a>.
 
 special_objects:
   initial object:

database/data/categories/Met_c.yaml

@@ -33,18 +33,23 @@ satisfied_properties:
     proof: See <a href="https://math.stackexchange.com/questions/5004389" target="_blank">MSE/5004389</a>.
     check_redundancy: false
 
-  - property: well-powered
-    proof: This follows easily from the fact that monomorphisms are injective in this category.
-
-  - property: well-copowered
-    proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.'
-
   - property: infinitary extensive
     proof: This follows from Lemma 11 <a href="/content/subcategories">here</a> since <a href="/category/Top">$\Top$</a> is infinitary extensive and its full subcategory $\Met_c$ of metrizable topological spaces is closed under pullbacks and coproducts in $\Top$.
 
+  - property: cokernel pairs
+    proof: >-
+      Since metric spaces are Hausdorff, the cokernel pair of $f : Y \to X$ coincides with the cokernel pair of the inclusion $C \hookrightarrow X$, where $C$ is the closure of the image of $f$ (if it exists). Thus, it suffices to prove that for every closed subset $C \subseteq X$ of a metric space, the pushout $X \sqcup_C X$ exists. In fact, the $\Top$-pushout $X \sqcup_C X$ is metrizable.
+      To see this, consider the canonical continuous map $p : X \sqcup X \to X \sqcup_C X$. It is surjective and closed, and its fibers have cardinality at most $2$. In particular, its fibers are compact. Since $X \sqcup X$ is metrizable, the claim now follows from the Hanai-Morita-Stone theorem; see Theorem 4.4.17 in Engelking's book <i>General Topology</i>.
+
   - property: effective cocongruences
     proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects colimits</a>, we conclude that $E$ is effective in $\Met_c$.'
 
+  - property: well-powered
+    proof: This follows easily from the fact that monomorphisms are injective in this category.
+
+  - property: well-copowered
+    proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.'
+
   - property: extremal generator
     proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to 1$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.'
 

database/data/categories/Rel.yaml

@@ -61,6 +61,9 @@ unsatisfied_properties:
   - property: normal
     proof: The construction of equalizers in $\Rel$ shows that they are injective functions, but <a href="https://math.stackexchange.com/questions/350716" target="_blank">MSE/350716</a> shows that monomorphisms in $\Rel$ don't have to be functions.
 
+  - property: kernel pairs
+    proof: 'Let $X$ be a finite set with $n$ elements. Consider the relation $R : X \to \{*\}$ corresponding to the set $\{(x,*) : x \in X\}$ (which is even a map). Assume that it has a kernel pair $E \rightrightarrows X$. Then, in particular, the set $P(E) \cong \Hom(\{*\},E)$ is isomorphic to the set of pairs $(S_1,S_2) \in \Hom(\{*\},X)^2$ such that $R \circ S_1 = R \circ S_2$. A relation $\{*\} \to X$ corresponds to a subset of $X$, and its composition with $R$ corresponds to the image of that subset under $R$, which is either $\varnothing$ or $\{*\}$, depending on whether the subset is empty or not. Therefore, the set of pairs $(S_1,S_2)$ with $R \circ S_1 = R \circ S_2$ has exactly $1 + (2^n - 1) (2^n - 1)$ elements. For $n=2$, for example, this is equal to $10$, and therefore not a power of $2$. Thus, the set cannot be isomorphic to $P(E)$ for any set $E$.'
+
 special_objects:
   initial object:
     description: empty set

database/data/categories/Sch_R.yaml

@@ -55,6 +55,9 @@ unsatisfied_properties:
   - property: generating set
     proof: If $S$ is a generating set of $R$-schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine $R$-schemes, corresponding to a cogenerating set in <a href="/category/CAlg(R)">$\CAlg(R)$</a>, which we know does not exist.
 
+  - 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>.
 

database/data/categories/Set_ff.yaml

@@ -33,6 +33,12 @@ satisfied_properties:
     proof: 'The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite.'
     check_redundancy: false
 
+  - property: cokernel pairs
+    proof: >-
+      Let $f : X \to Y$ be a finite-to-one map. Consider the cokernel pair $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$ in $\Set$. The maps $i_1,i_2$ are injective, in fact split monomorphisms in $\Set$, and therefore finite-to-one. To show that this cokernel pair is also a cokernel pair in $\Set_\ff$, it suffices to show that a map $h : Y \sqcup_X Y \to T$ is finite-to-one whenever both restrictions $h \circ i_1, h \circ i_2 : Y \rightrightarrows T$ are finite-to-one. Since $i_1,i_2$ are jointly surjective, we have
+      $$h^* \{y\} \subseteq (i_1)_* (h \circ i_1)^* \{y\} \cup (i_2)_* (h \circ i_2)^* \{y\},$$
+      and the right-hand side is finite.
+
   - property: extensive
     proof: We have already seen that finite coproducts exist in $\Set_\ff$, and pullbacks exist since the category is locally cartesian closed, although a direct argument is also possible. The forgetful functor $\Set_\ff \to \Set$ preserves finite coproducts and pullbacks, and is clearly faithful and conservative (but not full). Therefore, the claim follows from the extensivity of $\Set$ and Lemma 11 <a href="/content/subcategories">here</a>.
 

database/data/categories/Setne.yaml

@@ -33,6 +33,9 @@ satisfied_properties:
   - property: cartesian closed
     proof: This is because <a href="/category/Set">$\Set$</a> is cartesian closed and since for non-empty sets $X,Y$ there is at least one function $X \to Y$.
 
+  - property: kernel pairs
+    proof: 'This is because <a href="/category/Set">$\Set$</a> has kernel pairs and for a map $f : X \to Y$ between non-empty sets $X,Y$ the kernel pair $\{(x,x'') \in X \times X : f(x) = f(x'')\}$ is also non-empty.'
+
   - property: binary coproducts
     proof: The disjoint union of two non-empty sets is non-empty.
 

database/data/categories/walking_coreflexive_pair.yaml

@@ -70,7 +70,7 @@ unsatisfied_properties:
   - property: coreflexive equalizers
     proof: 'The coreflexive pair $i,j : [0] \rightrightarrows [1]$ has no equalizer, in fact is not equalized by any morphism.'
 
-  - property: pushouts
+  - property: cokernel pairs
     proof: Assume that $[1] \xleftarrow{i} [0] \xrightarrow{i} [1]$ has a pushout in $\Delta^{\leq 1}$, where $i(0)=0$. This amounts to a universal totally ordered set of cardinality $\leq 2$ with elements $a,b,c$ satisfying $a \leq b$, $a \leq c$. Since a finite totally ordered set has trivial automorphism group, the automorphism defined by $a \mapsto a$, $b \mapsto c$, $c \mapsto b$ must be the identity, i.e., we have $b = c$. However, in $[1]$ the equations $0 \leq 0$, $0 \leq 1$ then show that the universal property fails.
 
   - property: natural numbers object

database/data/categories/walking_idempotent.yaml

@@ -44,6 +44,9 @@ unsatisfied_properties:
   - property: Cauchy complete
     proof: The idempotent $e$ does not split.
 
+  - property: kernel pairs
+    proof: Assume that $e$ has a kernel pair. Its underlying object must be $0$. Thus, there is a bijection between the morphisms $0 \to 0$ and the pairs of morphisms $0 \rightrightarrows 0$ that $e$ equalizes. But this holds for all pairs of morphisms. Counting these sets gives the contradiction $2 = 4$.
+
 special_objects: {}
 
 special_morphisms:

database/data/category-implications/pullbacks.yaml

@@ -1,4 +1,4 @@
-# results on pullbacks and wide pullbacks
+# results on pullbacks, wide pullbacks, and kernel pairs
 
 - id: pullbacks_criterion
   assumptions:
@@ -33,3 +33,53 @@
   conclusions:
     - wide pullbacks
   proof: Each slice category has finite products and is essentially finite, hence has all products by <a href="/category-implication/freyd_finite">this result</a> followed by <a href="/category-implication/thin_finite_product_reduction">this result</a>.
+
+- id: kernel_pair_is_pullback
+  assumptions:
+    - pullbacks
+  conclusions:
+    - kernel pairs
+  proof: This is trivial.
+
+- id: kernel_pair_terminal_power
+  assumptions:
+    - kernel pairs
+    - terminal object
+  conclusions:
+    - binary powers
+  proof: If $1$ is a terminal object, then $X \times_1 X = X \times X$.
+
+- id: left_cancellative_kernel_pairs
+  assumptions:
+    - left cancellative
+  conclusions:
+    - kernel pairs
+  proof: >-
+    In general, the kernel pair of a monomorphism $f : X \to Y$ exists and is given by
+    $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$
+
+- id: right_cancellative_kernel_pairs
+  assumptions:
+    - right cancellative
+    - kernel pairs
+  # TODO: rework this once we have split-mono-trivial
+  conclusions:
+    - left cancellative
+  proof: >-
+    Let $f : X \to Y$ be a morphism with kernel pair $E \rightrightarrows X$. The diagonal $X \to E$ is a split monomorphism. By assumption on the category, it is also an epimorphism. Thus, it is an isomorphism. Therefore,
+    $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$
+    is a pullback, so $f$ is a monomorphism.
+
+- id: additive_kernel_pairs
+  assumptions:
+    - preadditive
+    - kernel pairs
+    - Cauchy complete
+  conclusions:
+    - kernels
+  proof: >-
+    Let $f : X \to Y$ be a morphism. Since $f$ has a kernel pair, the functor
+    $$\C^{\op} \to \Set^+, \quad T \mapsto \{(u,v) \in \Hom(T,X)^2 : f \circ u = f \circ v\}$$
+    is representable. Using $w = u-v$, this functor is isomorphic to
+    $$T \mapsto \{(u,w) \in \Hom(T,X)^2 : f \circ w = 0\}.$$
+    The functor $T \mapsto \{w \in \Hom(T,X) : f \circ w = 0\}$ is a retract of this functor. Since the category is Cauchy complete, every retract of a representable functor is representable. Therefore, the kernel of $f$ exists.