From 3653928cd265a52a23a4d22ae386e0b807577d04 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 21 Jul 2026 20:50:00 +0200 Subject: [PATCH] Met_c is not regular --- ...ntial-colimits-via-congruence-quotients.md | 14 --------- database/data/categories/Met_c.yaml | 31 ++++++++++++++++++- 2 files changed, 30 insertions(+), 15 deletions(-) delete mode 100644 content/monic-sequential-colimits-via-congruence-quotients.md diff --git a/content/monic-sequential-colimits-via-congruence-quotients.md b/content/monic-sequential-colimits-via-congruence-quotients.md deleted file mode 100644 index 9305e9fad..000000000 --- a/content/monic-sequential-colimits-via-congruence-quotients.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -title: Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence -description: A countably extensive category with quotients of congruences has colimits of sequences of monomorphisms. -author: Daniel Schepler ---- - -## Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence - -::: Lemma -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_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} \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 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. $\square$ diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 74e9dd022..69df47463 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -72,8 +72,37 @@ unsatisfied_properties: - property: ℵ₁-filtered colimits proof: See MO/511433 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 sequential fan $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 := \{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 := \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 := 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 := 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 := \{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 := \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: If $\Met_c$ had quotients of congruences, then by this lemma it would have sequential colimits of sequences of monomorphisms. This contradicts MO/510316. + 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. special_objects: initial object: