From 241a3db535412a988e0078ed9d2d7bec5f24b09c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 02:05:43 +0200 Subject: [PATCH 1/7] use \coloneqq instead of := (and likewise \eqqcolon for =:) this has better spacing --- content/cocongruences_of_groups.md | 4 ++-- content/comphaus_copresentable.md | 8 ++++---- content/foundations.md | 4 ++-- databases/catdat/data/categories/Alg(R).yaml | 8 ++++---- databases/catdat/data/categories/Ban.yaml | 6 +++--- databases/catdat/data/categories/CAlg(R).yaml | 8 ++++---- databases/catdat/data/categories/CMon.yaml | 4 ++-- databases/catdat/data/categories/CRing.yaml | 4 ++-- databases/catdat/data/categories/Cat.yaml | 2 +- databases/catdat/data/categories/CompHaus.yaml | 6 +++--- databases/catdat/data/categories/Delta.yaml | 2 +- databases/catdat/data/categories/FI.yaml | 4 ++-- databases/catdat/data/categories/FS.yaml | 4 ++-- databases/catdat/data/categories/FinGrp.yaml | 2 +- databases/catdat/data/categories/FinOrd.yaml | 8 ++++---- databases/catdat/data/categories/Fld.yaml | 2 +- databases/catdat/data/categories/Grp.yaml | 2 +- databases/catdat/data/categories/J2.yaml | 2 +- databases/catdat/data/categories/LRS.yaml | 4 ++-- databases/catdat/data/categories/Meas.yaml | 2 +- databases/catdat/data/categories/Met.yaml | 6 +++--- databases/catdat/data/categories/Met_c.yaml | 2 +- databases/catdat/data/categories/Met_oo.yaml | 4 ++-- databases/catdat/data/categories/Mon.yaml | 6 +++--- databases/catdat/data/categories/PMet.yaml | 4 ++-- databases/catdat/data/categories/Pos.yaml | 4 ++-- databases/catdat/data/categories/Prost.yaml | 6 +++--- databases/catdat/data/categories/Rel.yaml | 2 +- databases/catdat/data/categories/Ring.yaml | 4 ++-- databases/catdat/data/categories/Rng.yaml | 4 ++-- databases/catdat/data/categories/SemiGrp.yaml | 18 +++++++++--------- databases/catdat/data/categories/Set_f.yaml | 4 ++-- databases/catdat/data/categories/Top.yaml | 2 +- .../catdat/data/categories/Top_pointed.yaml | 4 ++-- databases/catdat/data/categories/sSet.yaml | 2 +- .../catdat/data/categories/walking_fork.yaml | 2 +- .../data/categories/walking_splitting.yaml | 2 +- .../catdat/data/category-implications/NNO.yaml | 2 +- .../category-implications/congruences.yaml | 6 +++--- .../filtered colimits.yaml | 2 +- .../data/category-implications/generators.yaml | 2 +- .../data/category-implications/topos.yaml | 2 +- .../data/category-properties/copowers.yaml | 2 +- .../data/category-properties/powers.yaml | 2 +- .../catdat/data/functors/abelianization.yaml | 2 +- .../data/functors/power_set_covariant.yaml | 2 +- .../data/lemmas/generator_construction.yaml | 2 +- ...tial-colimits-via-congruence-quotients.yaml | 2 +- .../lemmas/nno_distributive_criterion.yaml | 6 +++--- .../lemmas/preadditive_structure_unique.yaml | 2 +- 50 files changed, 98 insertions(+), 98 deletions(-) diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md index cf295ff3..c39eb421 100644 --- a/content/cocongruences_of_groups.md +++ b/content/cocongruences_of_groups.md @@ -62,7 +62,7 @@ $$c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,$$ where $u_1,u_2 : Y \rightrightarrows Y \sqcup_{i_2,X,i_1} Y$ are the pushout inclusions satisfying $u_1 i_2 = u_2 i_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Define the monomorphism -$$E := \eq(i_1,i_2) \hookrightarrow X.$$ +$$E \coloneqq \eq(i_1,i_2) \hookrightarrow X.$$ Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism @@ -74,7 +74,7 @@ We must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, sin We will show that even the morphism -$$\gamma := c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y$$ +$$\gamma \coloneqq c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y$$ is a monomorphism. It is characterized by diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md index 332d6d9a..696caef7 100644 --- a/content/comphaus_copresentable.md +++ b/content/comphaus_copresentable.md @@ -19,10 +19,10 @@ Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltere _Proof._ Consider the product space $\prod_{i\in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset -$$\textstyle E_f := \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$ +$$\textstyle E_f \coloneqq \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$ Then each $E_f$ is a closed subset. -Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f\in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f\in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J := \{ i_f \mid f \in F \} \cup \{ j_f \mid f \in F \}$ and morphisms $\{ f \mid f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f\in F} E_f$, which finishes the proof of the claim. +Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f\in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f\in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J \coloneqq \{ i_f \mid f \in F \} \cup \{ j_f \mid f \in F \}$ and morphisms $\{ f \mid f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f\in F} E_f$, which finishes the proof of the claim. Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$. $\square$ ::: Lemma 2 @@ -64,7 +64,7 @@ The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally prove ::: _Proof._ -Suppose we have an $\aleph_1$-cofiltered limit $X = \lim_{i\in \I} X_i$ with projections $p_i : X \to X_i$, and a continuous function $\varphi : X \to [0,1]$. For the time being, fix $n\in \IN_{>0}$. Then for any $x\in X$, there exists an interval neighborhood $N_x$ of $\varphi(x)$ of diameter at most $1/n$ — for example, we can take $N_x := (\varphi(x) - 1/(2n), \varphi(x) + 1/(2n)) \cap [0,1]$. We can also take a basic open neighborhood whose image is contained in $N_x$; by lemma 2, we can write that basic open neighborhood in the form $p_i^{-1}(V)$ where $V$ is an open subset of $X_i$. +Suppose we have an $\aleph_1$-cofiltered limit $X = \lim_{i\in \I} X_i$ with projections $p_i : X \to X_i$, and a continuous function $\varphi : X \to [0,1]$. For the time being, fix $n\in \IN_{>0}$. Then for any $x\in X$, there exists an interval neighborhood $N_x$ of $\varphi(x)$ of diameter at most $1/n$ — for example, we can take $N_x \coloneqq (\varphi(x) - 1/(2n), \varphi(x) + 1/(2n)) \cap [0,1]$. We can also take a basic open neighborhood whose image is contained in $N_x$; by lemma 2, we can write that basic open neighborhood in the form $p_i^{-1}(V)$ where $V$ is an open subset of $X_i$. By compactness of $X$, we may take finitely many such basic open neighborhoods of the form $p_i^{-1}(V)$ which cover $X$. Again using the assumption that $\I$ is cofiltered, we may assume that $i$ is the same for each neighborhood. In particular, we see that whenever we have $x, y\in X$ with $p_i(x) = p_i(y)$, then $|\varphi(x) - \varphi(y)| < 1/n$. To summarize, we have shown that for each $n \in \IN_{>0}$, there exists $i \in \I$ and a finite cover $\{ V_\lambda \mid \lambda \in \Lambda \}$ of $\im(p_i)$ such that whenever $p_i(x), p_i(y) \in V_\lambda$ for some $\lambda$, we have $|\varphi(x) - \varphi(y)| < 1/n$. Now choose such a $i_n$ and associated finite cover of $\im(p_{i_n})$ for each $n$. Then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(j, f_n : j \to i_n)$ of the objects $i_n$. We then see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_j$. This function is continuous, since by construction for any $n\in \IN_{>0}$ and $x \in X$, there is a neighborhood $V$ of $p_j(x)$ such that whenever $p_j(y)\in V$ as well, $|\varphi(y) - \varphi(x)| < 1/n$. By the Tietze extension theorem, this induced function can then be extended to a continuous function $\psi : X_j \to [0,1]$. Then $\varphi = \psi \circ p_j$. @@ -73,7 +73,7 @@ This shows the canonical map $$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in \I} X_i, [0,1])$$ is surjective. -Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \IN_{>0}$, consider the set $D_n := \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption. +Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \IN_{>0}$, consider the set $D_n \coloneqq \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption. Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This implies that $\alpha \circ X_f = \beta \circ X_f$. This shows the canonical map diff --git a/content/foundations.md b/content/foundations.md index dc5f2c17..082afd8a 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -45,11 +45,11 @@ A _category_ $\C$ consists of a pair of collections $O, M$, whose elements are c - $t : M \to O$ (_target_), - $c : M \times_O M \to M$ (_composition_), -such that the usual [axioms of a category]() are satisfied. The domain of $c$ consists of all pairs of morphisms $(f,g)$ with $s(f) = t(g)$, and we write $f \circ g := c(f,g)$ for their composition. Instead of $i(X)$ one usually writes $\id_X$ for the identity morphism of $X$. Formally, a category is a tuple +such that the usual [axioms of a category]() are satisfied. The domain of $c$ consists of all pairs of morphisms $(f,g)$ with $s(f) = t(g)$, and we write $f \circ g \coloneqq c(f,g)$ for their composition. Instead of $i(X)$ one usually writes $\id_X$ for the identity morphism of $X$. Formally, a category is a tuple $$\C = (O,M,i,s,t,c)$$ -of collections (and hence a collection itself). We write $\Ob(\C) := O$ and $\Mor(\C) := M$. Instead of $X \in \Ob(\C)$, we often write $X \in \C$. +of collections (and hence a collection itself). We write $\Ob(\C) \coloneqq O$ and $\Mor(\C) \coloneqq M$. Instead of $X \in \Ob(\C)$, we often write $X \in \C$. When $f \in \Mor(\C)$ is a morphism with $s(f) = X$ and $t(f) = Y$, we write $$f : X \to Y.$$ diff --git a/databases/catdat/data/categories/Alg(R).yaml b/databases/catdat/data/categories/Alg(R).yaml index 1da3593b..be36dc57 100644 --- a/databases/catdat/data/categories/Alg(R).yaml +++ b/databases/catdat/data/categories/Alg(R).yaml @@ -35,7 +35,7 @@ unsatisfied_properties: reason: This is trivial. - property: balanced - reason: Take a prime ideal $P \subseteq R$ and consider the $R$-algebra $A := R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample. + reason: Take a prime ideal $P \subseteq R$ and consider the $R$-algebra $A \coloneqq R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample. - property: semi-strongly connected reason: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected. @@ -47,10 +47,10 @@ unsatisfied_properties: reason: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see MSE/625874 for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually no isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative, it has the algebra presentation $\langle X,E : E^2=E \rangle$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' - property: coregular - reason: 'We just need to tweak the proof for $\Ring$. Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B := M_2(K)$ and $A := K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M := \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' + reason: 'We just need to tweak the proof for $\Ring$. Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B \coloneqq M_2(K)$ and $A \coloneqq K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' - property: regular quotient object classifier reason: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in $\CAlg(R)$ by this lemma (dualized). @@ -65,7 +65,7 @@ unsatisfied_properties: reason: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. - property: effective cocongruences - reason: 'The counterexample is similar to the one for $\Ring$: Let $X := R[p] / (p^2-p)$ with cocongruence $E := R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.' + reason: 'The counterexample is similar to the one for $\Ring$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.' special_objects: initial object: diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index e9772630..8b7b63ec 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -55,7 +55,7 @@ unsatisfied_properties: reason: See the comments to MO/509552. - property: filtered-colimit-stable monomorphisms - reason: 'The proof is similar to $\Met$. For $n \geq 1$ let $V_n$ be the Banach space with underlying vector space $\IC$ and the norm $|x|_n := \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $V_n \to V_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $V$ be the colimit of all $V_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| := \inf \{|x|_m : n \leq m \}$ for $x \in V_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, also $0$. Thus, the monomorphisms $V_1 \to V_n$ become $V_1 \to 0$ in the colimit.' + reason: 'The proof is similar to $\Met$. For $n \geq 1$ let $V_n$ be the Banach space with underlying vector space $\IC$ and the norm $|x|_n \coloneqq \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $V_n \to V_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $V$ be the colimit of all $V_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| \coloneqq \inf \{|x|_m : n \leq m \}$ for $x \in V_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, also $0$. Thus, the monomorphisms $V_1 \to V_n$ become $V_1 \to 0$ in the colimit.' - property: cofiltered-limit-stable epimorphisms reason: 'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ and $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.' @@ -66,7 +66,7 @@ special_objects: terminal object: description: trivial Banach space coproducts: - description: 'The coproduct of a family of Banach spaces $(B_i)$ is the subspace $\bigl\{x \in \prod_i B_i : \sum_i |x_i| < \infty\bigr\}$ equipped with the $1$-norm $|x| := \sum_i |x_i|$.' + description: 'The coproduct of a family of Banach spaces $(B_i)$ is the subspace $\bigl\{x \in \prod_i B_i : \sum_i |x_i| < \infty\bigr\}$ equipped with the $1$-norm $|x| \coloneqq \sum_i |x_i|$.' products: description: direct products with the $\sup$-norm @@ -79,7 +79,7 @@ special_morphisms: reason: 'The unit ball functor $U : \Ban \to \Set$ is faithful and representable (by $\IC$), hence reflects and preserves monomorphisms.' epimorphisms: description: linear contractions with dense image - reason: 'Let $f : X \to Y$ be an epimorphism of Banach spaces. The subspace $U := \overline{f(X)} \subseteq Y$ is closed. It is well-known that the quotient $Y/U$ is also a Banach space with a projection $p : Y \to Y/U$. Since $p \circ f = 0 = 0 \circ f$, we infer $p = 0$, so that $U = Y$.' + reason: 'Let $f : X \to Y$ be an epimorphism of Banach spaces. The subspace $U \coloneqq \overline{f(X)} \subseteq Y$ is closed. It is well-known that the quotient $Y/U$ is also a Banach space with a projection $p : Y \to Y/U$. Since $p \circ f = 0 = 0 \circ f$, we infer $p = 0$, so that $U = Y$.' regular monomorphisms: description: closed embeddings reason: The non-trivial direction follows from the well-known fact that for every closed subspace of a Banach space its quotient space is again a Banach space. diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index 101ecd8a..f64e5c9e 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -36,22 +36,22 @@ unsatisfied_properties: reason: This is trivial. - property: balanced - reason: Take a prime ideal $P \subseteq R$ and consider the commutative $R$-algebra $A := R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample. + reason: Take a prime ideal $P \subseteq R$ and consider the commutative $R$-algebra $A \coloneqq R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample. - property: cogenerating set reason: 'We apply this lemma to the collection of commutative $R$-algebras which are fields: If $F$ is a commutative $R$-algebra that is also a field and $A$ is a non-trivial commutative $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' - property: countably codistributive - reason: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A := K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.' + reason: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A \coloneqq K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.' - property: semi-strongly connected - reason: Choose a maximal ideal $\mathfrak{m}$ of $R$, so $K := R/\mathfrak{m}$ is a field. If $\CAlg(R)$ is semi-strongly connected, then also $\CAlg(K)$ is semi-strongly connected. This has been disproven in MSE/5129689. + reason: Choose a maximal ideal $\mathfrak{m}$ of $R$, so $K \coloneqq R/\mathfrak{m}$ is a field. If $\CAlg(R)$ is semi-strongly connected, then also $\CAlg(K)$ is semi-strongly connected. This has been disproven in MSE/5129689. - property: coregular reason: See MSE/3745302. - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \CAlg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R[X,Y] / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \CAlg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R[X,Y] / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' - property: regular quotient object classifier reason: 'The strategy is similar to the one for $\CRing$: Assume that $P \to R$ is a regular quotient object classifier. If $J$ denotes the kernel of $P \to R$, every ideal $I \subseteq A$ of any commutative $R$-algebra has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed algebra of $\sigma$. But then $I$ is generated by elements in $A^{\sigma} \cap I$. If $K$ is a residue field of $R$, this fails for $A = K[X,Y]$, $I = \langle X,Y \rangle$, $\sigma(X)=Y$, $\sigma(Y)=X$. The fixed algebra is the subalgebra of symmetric polynomials, which is $K[X+Y,XY]$. So $\langle X,Y \rangle$ is generated by symmetric polynomials without constant term, which implies $\langle X,Y \rangle \subseteq \langle X+Y,XY \rangle$ in $K[X,Y]$. But reducing an equation like $X = a(X,Y) \cdot (X+Y) + b(X,Y) \cdot (XY)$ modulo $\langle X^2,Y^2,XY \rangle$ yields a contradiction.' diff --git a/databases/catdat/data/categories/CMon.yaml b/databases/catdat/data/categories/CMon.yaml index 4f61787d..b7a35bd9 100644 --- a/databases/catdat/data/categories/CMon.yaml +++ b/databases/catdat/data/categories/CMon.yaml @@ -39,13 +39,13 @@ unsatisfied_properties: reason: 'Consider the submonoid $\{(a,b) : a \leq b \}$ of $\IN^2$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \CMon \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by the free monoid on a single generator and $R$ by the free commutative monoid on two generators $x,y$ subject to the relation $xy=x^2$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \CMon \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by the free monoid on a single generator and $R$ by the free commutative monoid on two generators $x,y$ subject to the relation $xy=x^2$. It is clear that $R$ is reflexive, but not symmetric.' - property: cogenerator reason: See MO/509232. - property: coregular - reason: 'We can show this analogously to the case of commutative rings MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U\coloneqq\{(m,n)\mid m\ge n\}$ with the inclusion $i\colon U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D\coloneqq\{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j\colon U\hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I\coloneqq\{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v\colon D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' + reason: 'We can show this analogously to the case of commutative rings MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U \coloneqq \{(m,n)\mid m\ge n\}$ with the inclusion $i\colon U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D \coloneqq \{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j\colon U\hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I \coloneqq \{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v\colon D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' - property: regular subobject classifier reason: We can use exactly the same proof as for $\Mon$. diff --git a/databases/catdat/data/categories/CRing.yaml b/databases/catdat/data/categories/CRing.yaml index be5b145e..c5f34f4b 100644 --- a/databases/catdat/data/categories/CRing.yaml +++ b/databases/catdat/data/categories/CRing.yaml @@ -32,7 +32,7 @@ satisfied_properties: reason: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. - property: coextensive - reason: '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e := f(1,0) \in R$, so that $R \cong eR \times (1-e)R$. Then $f$ decomposes into the ring homomorphisms $f_A : A \to eR$, $f_A(a) := f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) := f(0,b)$.' + reason: '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e \coloneqq f(1,0) \in R$, so that $R \cong eR \times (1-e)R$. Then $f$ decomposes into the ring homomorphisms $f_A : A \to eR$, $f_A(a) \coloneqq f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) \coloneqq f(0,b)$.' unsatisfied_properties: - property: skeletal @@ -54,7 +54,7 @@ unsatisfied_properties: reason: See MSE/3745302. - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \CRing \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $R$ by $\IZ[X,Y] / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \CRing \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $R$ by $\IZ[X,Y] / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' - property: regular quotient object classifier reason: 'Assume that $P \to \IZ$ is a regular quotient object classifier. If $J$ denotes its kernel, this means that every ideal $I \subseteq A$ of any commutative ring has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed ring of $\sigma$. But then $I$ is generated by elements in the fixed ring. This fails for $A = \IZ[X]$, $I = \langle X \rangle$, $\sigma(X)=-X$. The fixed ring is $\IZ[X^2]$, and if $I$ was generated by elements $f \in \IZ[X^2] \cap I$, they would be multiples of $X^2$, but $X$ is not a multiple of $X^2$.' diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index bab8f2af..70835a9b 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -82,5 +82,5 @@ special_morphisms: description: faithful functors that are injective on objects reason: 'Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : 1 \to \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \to B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \to \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.' epimorphisms: - description: 'A functor $F : \C \to \D$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\D$ there is a zigzag over $U := F(\C)$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \D$ and $y_1,\dotsc,y_m \in \D$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' + description: 'A functor $F : \C \to \D$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\D$ there is a zigzag over $U \coloneqq F(\C)$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \D$ and $y_1,\dotsc,y_m \in \D$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' reason: This is an extension of the corresponding theorem for monoids and proven in Epimorphisms and Dominions, III by John R. Isbell. diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml index db92faa2..4e93e2e0 100644 --- a/databases/catdat/data/categories/CompHaus.yaml +++ b/databases/catdat/data/categories/CompHaus.yaml @@ -77,7 +77,7 @@ unsatisfied_properties: - property: natural numbers object reason: >- - Let $I := [0, 1]$. If a natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition + Let $I \coloneqq [0, 1]$. If a natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition $$\begin{align*} I & \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I, \\ x & \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1}, @@ -89,8 +89,8 @@ unsatisfied_properties: - property: exact cofiltered limits reason: |- - Consider the $\IN$-codirected systems $X_n := [0, 1] \times [0, 1/n]$ with the maps $X_{n+1} \to X_n$ being inclusion maps, and $Y_n := [0, 1+1/n]$ with the maps $Y_{n+1} \to Y_n$ also being inclusion maps. We define $f_n : X_n \to Y_n$, $(x, y) \mapsto x$ and $g_n : X_n \to Y_n$, $(x, y) \mapsto x+y$. It is straightforward to check these give morphisms of $\IN$-codirected systems in $\CompHaus$. - Now for each $n$, we claim the coequalizer of $f_n$ and $g_n$ is a singleton space. To see this, we prove the more general result that for $r, s > 0$ the coequalizer of $f, g : [0, r] \times [0, s] \rightrightarrows [0, r+s]$, $f(x,y) = x$, $g(x,y) = x+y$ is a singleton. We must show that for any $h : [0, r+s] \to T$ with $h\circ f = h\circ g$, then $h$ is constant. To this end, we show by induction on $n$ that whenever $x \in [0, r+s]$ and $x \le ns$, we have $h(x) = h(0)$. The base case $n=0$ is trivial. For the inductive step, if $x \le s$, then $f(0,x) = 0$ and $g(0,x) = x$, so $h(0) = h(x)$. Otherwise, we have $x-s \in [0,r]$ and $x-s \le (n-1)s$, so by inductive hypothesis $h(x-s) = h(0)$. Also, $f(x-s, s) = x-s$ and $g(x-s, s) = x$, so $h(x-s) = h(x)$, completing the induction. With this established, the desired result follows from the case $n := \lceil r/s \rceil + 1$. + Consider the $\IN$-codirected systems $X_n \coloneqq [0, 1] \times [0, 1/n]$ with the maps $X_{n+1} \to X_n$ being inclusion maps, and $Y_n \coloneqq [0, 1+1/n]$ with the maps $Y_{n+1} \to Y_n$ also being inclusion maps. We define $f_n : X_n \to Y_n$, $(x, y) \mapsto x$ and $g_n : X_n \to Y_n$, $(x, y) \mapsto x+y$. It is straightforward to check these give morphisms of $\IN$-codirected systems in $\CompHaus$. + Now for each $n$, we claim the coequalizer of $f_n$ and $g_n$ is a singleton space. To see this, we prove the more general result that for $r, s > 0$ the coequalizer of $f, g : [0, r] \times [0, s] \rightrightarrows [0, r+s]$, $f(x,y) = x$, $g(x,y) = x+y$ is a singleton. We must show that for any $h : [0, r+s] \to T$ with $h\circ f = h\circ g$, then $h$ is constant. To this end, we show by induction on $n$ that whenever $x \in [0, r+s]$ and $x \le ns$, we have $h(x) = h(0)$. The base case $n=0$ is trivial. For the inductive step, if $x \le s$, then $f(0,x) = 0$ and $g(0,x) = x$, so $h(0) = h(x)$. Otherwise, we have $x-s \in [0,r]$ and $x-s \le (n-1)s$, so by inductive hypothesis $h(x-s) = h(0)$. Also, $f(x-s, s) = x-s$ and $g(x-s, s) = x$, so $h(x-s) = h(x)$, completing the induction. With this established, the desired result follows from the case $n \coloneqq \lceil r/s \rceil + 1$. On the other hand, $\lim X_n \simeq [0, 1] \times \{ 0 \}$; $\lim Y_n \simeq [0, 1]$; and $\lim f_n = \lim g_n$, $(x, 0) \mapsto x$. Thus, the coequalizer of $\lim f_n$ and $\lim g_n$ is $[0, 1]$, showing that the limit does not preserve this coequalizer. special_objects: diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index 4e8df641..de07bf0d 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/databases/catdat/data/categories/Delta.yaml @@ -1,7 +1,7 @@ id: Delta name: simplex category notation: $\Delta$ -objects: the non-empty ordered sets $[n] := \{0 < \cdots < n\}$ for $n \in \IN$ +objects: the non-empty ordered sets $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$ morphisms: order-preserving maps description: The simplex category is a skeleton of $\FinOrd \setminus \{\varnothing\}$. It plays an important role in topology and is used to define the category of simplicial sets. nlab_link: https://ncatlab.org/nlab/show/simplex+category diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index 1397b75d..5cedc9ca 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/databases/catdat/data/categories/FI.yaml @@ -69,7 +69,7 @@ unsatisfied_properties: reason: Assume that two finite sets $X,Y$ have a product $P$ in this category. Elements of $P$ are the same as maps $1 \to P$, and they are automatically injective. Therefore, $P \cong \Hom(1,P) \times \Hom(1,X) \times \Hom(1,Y) \cong X \times Y$, and the projections must agree as well. But they are usually not injective. In particular, the product $X \times X$ never exists when $X$ has $>1$ elements. - property: sequential colimits - reason: 'Let $X_n := \{1,\dotsc,n\}$. Assume the sequence of inclusion maps $X_n \hookrightarrow X_{n+1}$ has a colimit $(f_n : X_n \to X)$ in this category. But $f_n$ must be an injective map, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.' + reason: 'Let $X_n \coloneqq \{1,\dotsc,n\}$. Assume the sequence of inclusion maps $X_n \hookrightarrow X_{n+1}$ has a colimit $(f_n : X_n \to X)$ in this category. But $f_n$ must be an injective map, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.' special_objects: initial object: @@ -84,7 +84,7 @@ special_morphisms: reason: This is trivial. epimorphisms: description: bijective maps - reason: 'Take an epimorphism $X \to Y$ in this category, w.l.o.g. the inclusion of a subset $X \subseteq Y$. This means that for two injective maps $f,g : Y \rightrightarrows T$ with $f|_X = g|_X$ we must have $f = g$. Let $T := Y + (Y \setminus X)$ (disjoint union), $f$ be the inclusion into the first summand, $g|_X$ be the inclusion into the first summand, and $g|_{Y \setminus X}$ be the inclusion into the second summand. Then $f$ and $g$ are injective with $f|_X = g|_X$, so that $f = g$. But this means $X = Y$.' + reason: 'Take an epimorphism $X \to Y$ in this category, w.l.o.g. the inclusion of a subset $X \subseteq Y$. This means that for two injective maps $f,g : Y \rightrightarrows T$ with $f|_X = g|_X$ we must have $f = g$. Let $T \coloneqq Y + (Y \setminus X)$ (disjoint union), $f$ be the inclusion into the first summand, $g|_X$ be the inclusion into the first summand, and $g|_{Y \setminus X}$ be the inclusion into the second summand. Then $f$ and $g$ are injective with $f|_X = g|_X$, so that $f = g$. But this means $X = Y$.' regular monomorphisms: description: same as monomorphisms reason: This is because the category is mono-regular. diff --git a/databases/catdat/data/categories/FS.yaml b/databases/catdat/data/categories/FS.yaml index c4149c70..cc599800 100644 --- a/databases/catdat/data/categories/FS.yaml +++ b/databases/catdat/data/categories/FS.yaml @@ -63,13 +63,13 @@ unsatisfied_properties: reason: 'If $f : \varnothing \to X$ is surjective, then $X = \varnothing$, and if $f : X \to \varnothing$ is any map, then also $X = \varnothing$. This shows that $\{ \varnothing \}$ is a connected component in this category. (The other connected component consists of all non-empty finite sets.)' - property: sequential limits - reason: 'Let $X_n := \{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) := 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.' + reason: '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 reason: 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 - reason: Assume that the copower $X := 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$. + reason: 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$. - property: locally cocartesian coclosed reason: >- diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index 5fd2c814..2baeab87 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/databases/catdat/data/categories/FinGrp.yaml @@ -63,7 +63,7 @@ unsatisfied_properties: reason: Every non-normal subgroup of a finite group (such as $C_2 \hookrightarrow S_3$) provides a counterexample. - property: binary copowers - reason: 'Assume that $C_2 \sqcup C_2$ exists. This is a finite group, say of order $N$, with two involutions $u,v$ such that for every finite group $G$ with two involutions $a,b$ there is a unique homomorphism $\varphi : C_2 \sqcup C_2 \to G$ with $\varphi(u)=a$ and $\varphi(v)=2$. In particular, when $G$ is generated by $a,b$, then $\ord(G) \leq N$. But then the dihedral group $G := D_N$ of order $2N$ yields a contradiction.' + reason: 'Assume that $C_2 \sqcup C_2$ exists. This is a finite group, say of order $N$, with two involutions $u,v$ such that for every finite group $G$ with two involutions $a,b$ there is a unique homomorphism $\varphi : C_2 \sqcup C_2 \to G$ with $\varphi(u)=a$ and $\varphi(v)=2$. In particular, when $G$ is generated by $a,b$, then $\ord(G) \leq N$. But then the dihedral group $G \coloneqq D_N$ of order $2N$ yields a contradiction.' - property: sequential colimits reason: This follows from this lemma. diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index f8ef77b0..bbb37262 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/databases/catdat/data/categories/FinOrd.yaml @@ -47,10 +47,10 @@ satisfied_properties: reason: It suffices to construct quotients by equivalence relations. Let $\sim$ be an equivalence relation on $X$, where $(X,\leq)$ is a finite ordered set. Since $X$ is finite, by induction we may assume that $\sim$ is generated by a single relation $(a,b)$. If $a=b$, there is nothing to prove. If $a < b$ and $X = \{0,1,\dotsc,n-1\}$ with the usual order, the quotient is $\{0,1,\dotsc,a,b+1,\dotsc,n-1\}$ with the usual order. - property: mono-regular - reason: 'Let $i : A \to B$ be a monomorphism of finite ordered sets. If $A$ is empty, then $i$ is clearly regular, so assume it is not. The map $i$ is injective (see below), hence order-reflecting. Define maps $u,v : B \to A$ by $u(b) := \max \{a \in A : i(a) \leq b \}$ and $v(b) := \min \{a \in A : b \leq i(a) \}$. These are order-preserving and satisfy $u \circ i = v \circ i$, both sides are $\id_A$. Conversely, if $b \in B$ satisfies $u(b) = v(b) =: a$, then $i(a) \leq b$ and $b \leq i(a)$, hence $b = i(a)$. This shows that $i$ is the equalizer of $u,v$.' + reason: 'Let $i : A \to B$ be a monomorphism of finite ordered sets. If $A$ is empty, then $i$ is clearly regular, so assume it is not. The map $i$ is injective (see below), hence order-reflecting. Define maps $u,v : B \to A$ by $u(b) \coloneqq \max \{a \in A : i(a) \leq b \}$ and $v(b) \coloneqq \min \{a \in A : b \leq i(a) \}$. These are order-preserving and satisfy $u \circ i = v \circ i$, both sides are $\id_A$. Conversely, if $b \in B$ satisfies $u(b) = v(b) \eqqcolon a$, then $i(a) \leq b$ and $b \leq i(a)$, hence $b = i(a)$. This shows that $i$ is the equalizer of $u,v$.' - property: epi-regular - reason: 'Let $f : A \to B$ be an epimorphism of finite ordered sets. It is surjective (see below). Define $u,v : B \to A$ by $u(b) := \min(f^{-1}(b))$ and $v(b) := \max(f^{-1}(b))$. One can easily check that $u,v$ are order-preserving maps with $f \circ u = f \circ v$ (both sides are $\id_B$). Let $h : A \to T$ be an order-preserving map with $h \circ u = h \circ v$. Then $h(a)$ only depends on $b := f(a)$: We have $u(b) \leq a \leq v(b)$, hence $h(u(b)) \leq h(a) \leq h(v(b)) = h(u(b))$. Therefore, there is a unique map $\tilde{h} : B \to T$ with $\tilde{h}(f(a)) = h(a)$, and one easily checks that it is order-preserving. This shows that $f$ is the coequalizer of $u,v$.' + reason: 'Let $f : A \to B$ be an epimorphism of finite ordered sets. It is surjective (see below). Define $u,v : B \to A$ by $u(b) \coloneqq \min(f^{-1}(b))$ and $v(b) \coloneqq \max(f^{-1}(b))$. One can easily check that $u,v$ are order-preserving maps with $f \circ u = f \circ v$ (both sides are $\id_B$). Let $h : A \to T$ be an order-preserving map with $h \circ u = h \circ v$. Then $h(a)$ only depends on $b \coloneqq f(a)$: We have $u(b) \leq a \leq v(b)$, hence $h(u(b)) \leq h(a) \leq h(v(b)) = h(u(b))$. Therefore, there is a unique map $\tilde{h} : B \to T$ with $\tilde{h}(f(a)) = h(a)$, and one easily checks that it is order-preserving. This shows that $f$ is the coequalizer of $u,v$.' - property: core-thin reason: 'Let $f : \{1 < \cdots < n \} \to \{1 < \cdots < n \}$ be an automorphism. Then $f(i)$ is the smallest element not contained in $\{f(j) : j < i\}$. From this one can deduce $f(i)=i$ by induction.' @@ -72,10 +72,10 @@ unsatisfied_properties: reason: This is trivial. - property: sequential limits - reason: Consider the (non-empty) ordered set $[n] := \{0 < \cdots < n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable, hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\FinOrd$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But this is not a finite set. + reason: Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable, hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\FinOrd$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But this is not a finite set. - property: sequential colimits - reason: 'Consider the (non-empty) ordered set $[n] := \{0 < \cdots < n\}$ for $n \in \IN$. Assume the sequence of inclusion maps $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has a colimit $(f_n : [n] \to X)$ in $\FinOrd$. Let $n_0 \geq 0$ be fixed. I claim that $f_{n_0}$ is injective, which will then yield a contradiction by taking $n_0 \geq \card(X)$. For $n \geq 0$ define $g_n : [n] \to [n_0]$ as follows. For $n \leq n_0$ it is the inclusion, and for $n \geq n_0$ it is the surjection which keeps all elements of $[n_0]$ and maps all other elements to $n_0$. Observe that $g_n$ preserves the order and $g_{n+1} |_{[n]} = g_n$. Hence, there is a unique order-preserving map $g : X \to [n_0]$ with $g \circ f_n = g_n$ for all $n$. For $n = n_0$ this shows $g \circ f_{n_0} = \id_{[n_0]}$, and $f_{n_0}$ is injective.' + reason: 'Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. Assume the sequence of inclusion maps $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has a colimit $(f_n : [n] \to X)$ in $\FinOrd$. Let $n_0 \geq 0$ be fixed. I claim that $f_{n_0}$ is injective, which will then yield a contradiction by taking $n_0 \geq \card(X)$. For $n \geq 0$ define $g_n : [n] \to [n_0]$ as follows. For $n \leq n_0$ it is the inclusion, and for $n \geq n_0$ it is the surjection which keeps all elements of $[n_0]$ and maps all other elements to $n_0$. Observe that $g_n$ preserves the order and $g_{n+1} |_{[n]} = g_n$. Hence, there is a unique order-preserving map $g : X \to [n_0]$ with $g \circ f_n = g_n$ for all $n$. For $n = n_0$ this shows $g \circ f_{n_0} = \id_{[n_0]}$, and $f_{n_0}$ is injective.' special_objects: initial object: diff --git a/databases/catdat/data/categories/Fld.yaml b/databases/catdat/data/categories/Fld.yaml index 9d22dc65..beefe4d8 100644 --- a/databases/catdat/data/categories/Fld.yaml +++ b/databases/catdat/data/categories/Fld.yaml @@ -60,7 +60,7 @@ unsatisfied_properties: reason: 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' - property: binary powers - reason: 'Assume that the product $P := \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which however fails for $K = \IQ(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.' + reason: 'Assume that the product $P \coloneqq \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which however fails for $K = \IQ(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.' - property: locally cartesian closed reason: 'Assume that $K$ is a field such that $\Fld / K$ is cartesian closed. This slice category is equivalent to the poset of subfields of $K$. This poset is a lattice, and our assumption implies that it is distributive (see here). But this is quite rare: Consider $K = \IQ(\sqrt{2}, \sqrt{3})$. By Galois theory, the lattice of subfields is isomorphic to the diamond lattice $M_3$ which is not distributive. Specifically, $(\IQ(\sqrt{2}) \wedge \IQ(\sqrt{6})) \vee (\IQ(\sqrt{3}) \wedge \IQ(\sqrt{6})) = \IQ \vee \IQ = \IQ$, while $(\IQ(\sqrt{2}) \vee \IQ(\sqrt{3})) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{2},\sqrt{3}) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{6})$.' diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index 4ed658ed..fb151ba3 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -73,7 +73,7 @@ unsatisfied_properties: For cofiltered diagrams of groups $(H_i)$ and a group $G$ the canonical homomorphism $$\textstyle \alpha : G \sqcup \lim_i H_i \to \lim_i (G \sqcup H_i)$$ is injective, but often fails to be surjective because the components of an element in the image have bounded free product length (the number of factors appearing in the reduced form). Specifically, consider the free groups $G = \langle y \rangle$ and $H_n = \langle x_1,\dotsc,x_n \rangle$ for $n \in \IN$ with the truncation maps $H_{n+1} \to H_n$, $x_{n+1} \mapsto 1$. Define - $$p_n := x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n.$$ + $$p_n \coloneqq x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n.$$ If we substitute $x_{n+1}=1$ in $p_{n+1}$, we get $p_n$. Thus, we have $p = (p_n) \in \lim_n (G \sqcup H_n)$. This element does not lie in the image of $\alpha$ since the free product length of $p_n$ (which is well-defined) is $2n$, which is unbounded. special_objects: diff --git a/databases/catdat/data/categories/J2.yaml b/databases/catdat/data/categories/J2.yaml index 1f897667..75f5a5a4 100644 --- a/databases/catdat/data/categories/J2.yaml +++ b/databases/catdat/data/categories/J2.yaml @@ -31,7 +31,7 @@ unsatisfied_properties: - property: semi-strongly connected reason: >- - There is a bijection $\alpha = (\lambda,\rho) : \IN \to \IN \times \IN$ such that $\lambda$ has a fixed point, but $\rho$ does not (see below). Then the isomorphism $\beta := (\rho,\lambda)$ has the opposite property. There cannot be any morphism $(\IN,\alpha) \to (\IN,\beta)$, as it would map the fixed point of $\lambda$ to a fixed point of $\rho$, and likewise there is no morphism $(\IN,\beta) \to (\IN,\alpha)$. + There is a bijection $\alpha = (\lambda,\rho) : \IN \to \IN \times \IN$ such that $\lambda$ has a fixed point, but $\rho$ does not (see below). Then the isomorphism $\beta \coloneqq (\rho,\lambda)$ has the opposite property. There cannot be any morphism $(\IN,\alpha) \to (\IN,\beta)$, as it would map the fixed point of $\lambda$ to a fixed point of $\rho$, and likewise there is no morphism $(\IN,\beta) \to (\IN,\alpha)$. To construct $\alpha$ or rather $\alpha^{-1} : \IN \times \IN \to \IN$, we can alter the standard bijection $(n,m) \mapsto 2^n (2m+1) - 1$ as follows: $$\alpha^{-1}(n,m) = \begin{cases} 2 & (n,m) = (0,0) \\ 0 & (n,m) = (0,1) \\ 2^n (2m+1) - 1 & \text{otherwise} \end{cases}$$ diff --git a/databases/catdat/data/categories/LRS.yaml b/databases/catdat/data/categories/LRS.yaml index 034f3cbf..2db18e49 100644 --- a/databases/catdat/data/categories/LRS.yaml +++ b/databases/catdat/data/categories/LRS.yaml @@ -23,13 +23,13 @@ satisfied_properties: reason: See Demazure-Gabriel's "Groupes algébriques", I. §1. 1.6. Specifically, the forgetful functor to ringed spaces preserves colimits, and colimits of ringed spaces are built from colimits of topological spaces and limits of commutative rings, see MSE/1646202. - property: well-powered - reason: 'Let $f : X \to Y$ be a monomorphism of locally ringed spaces. I claim that $f$ is injective, from which the claim will follow. The diagonal $\Delta : X \to X \times_Y X$ is an isomorphism. By the explicit construction of fiber products, $X \times_Y X$ consists of triples $(x_1,x_2,\mathfrak{p})$ where $x_1,x_2 \in X$, $y := f(x_1) = f(x_2)$ and $\mathfrak{p}$ is a prime ideal in $k(x_1) \otimes_{k(y)} k(x_2)$. The map $\Delta$ is given by $\Delta(x) = \bigl(x,x,\ker(k(x) \otimes_{k(f(x))} k(x) \to k(x)\bigr)$, and it is bijective. This clearly implies that $f$ is injective (and that each tensor product $k(x) \otimes_{k(f(x))} k(x)$ has a unique prime ideal, namely the kernel mentioned).' + reason: 'Let $f : X \to Y$ be a monomorphism of locally ringed spaces. I claim that $f$ is injective, from which the claim will follow. The diagonal $\Delta : X \to X \times_Y X$ is an isomorphism. By the explicit construction of fiber products, $X \times_Y X$ consists of triples $(x_1,x_2,\mathfrak{p})$ where $x_1,x_2 \in X$, $y \coloneqq f(x_1) = f(x_2)$ and $\mathfrak{p}$ is a prime ideal in $k(x_1) \otimes_{k(y)} k(x_2)$. The map $\Delta$ is given by $\Delta(x) = \bigl(x,x,\ker(k(x) \otimes_{k(f(x))} k(x) \to k(x)\bigr)$, and it is bijective. This clearly implies that $f$ is injective (and that each tensor product $k(x) \otimes_{k(f(x))} k(x)$ has a unique prime ideal, namely the kernel mentioned).' - property: well-copowered reason: It is enough to prove that every epimorphism of locally ringed spaces is surjective. The forgetful functor $\LRS \to \RS$ has a right adjoint (see Localization of ringed spaces by W. Gillam), so it preserves epimorphisms. The forgetful functor $\RS \to \Top$ also has a right adjoint, namely $X \mapsto (X,\underline{\IZ})$, so it also preserves epimorphisms. - property: infinitary extensive - reason: '[Sketch] Since $\Top$ is infinitary extensive, a morphism $f : Y \to \coprod_i X_i =: X$ yields a decomposition $Y = \coprod_i Y_i$ (as topological spaces) with continuous maps $f_i : Y_i \to X_i$. Endow the open subset $Y_i \subseteq Y$ with the restricted sheaf. Then each $f_i$ becomes a morphism of locally ringed spaces, and $Y = \coprod_i Y_i$ holds as locally ringed spaces.' + reason: '[Sketch] Since $\Top$ is infinitary extensive, a morphism $f : Y \to \coprod_i X_i \eqqcolon X$ yields a decomposition $Y = \coprod_i Y_i$ (as topological spaces) with continuous maps $f_i : Y_i \to X_i$. Endow the open subset $Y_i \subseteq Y$ with the restricted sheaf. Then each $f_i$ becomes a morphism of locally ringed spaces, and $Y = \coprod_i Y_i$ holds as locally ringed spaces.' unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index d2aea00f..0bfb2809 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -41,7 +41,7 @@ satisfied_properties: reason: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable. - property: infinitary extensive - reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i =: X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' + reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' - property: filtered-colimit-stable monomorphisms reason: This follows from this lemma applied to the forgetful functor to $\Set$. diff --git a/databases/catdat/data/categories/Met.yaml b/databases/catdat/data/categories/Met.yaml index 8e13a962..18e0362b 100644 --- a/databases/catdat/data/categories/Met.yaml +++ b/databases/catdat/data/categories/Met.yaml @@ -26,7 +26,7 @@ satisfied_properties: reason: The one-point metric space is a generator since it represents the forgetful functor $\Met \to \Set$. - property: cogenerator - reason: 'We claim that $\IR$ with the usual metric is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR$. This applies in particular to $f(x) := d(a,x)$ and shows that $0=d(a,a)=d(a,b)$, so that $a=b$.' + reason: 'We claim that $\IR$ with the usual metric is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR$. This applies in particular to $f(x) \coloneqq d(a,x)$ and shows that $0=d(a,a)=d(a,b)$, so that $a=b$.' - property: semi-strongly connected reason: Every non-empty metric space is weakly terminal (by using constant maps). @@ -35,7 +35,7 @@ satisfied_properties: reason: Just restrict the metric to the equalizer built from the sets. - property: binary products - reason: The product of two metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) := \sup(d(x_1,x_2),d(y_1,y_2))$. + reason: The product of two metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) \coloneqq \sup(d(x_1,x_2),d(y_1,y_2))$. check_redundancy: false - property: terminal object @@ -103,7 +103,7 @@ unsatisfied_properties: - property: effective cocongruences reason: >- - We will define a cocongruence on the interval $(0,1) \subseteq \IR$ where $E := (-1, 0) \cup (0, 1) \subseteq \IR$, and the two maps $(0, 1) \rightrightarrows E$ are the inclusion map and $x \mapsto -x$. Then for any metric space $X$, the induced relation on non-expansive maps $(0, 1) \to X$ is that $f \sim g$ if and only if + We will define a cocongruence on the interval $(0,1) \subseteq \IR$ where $E \coloneqq (-1, 0) \cup (0, 1) \subseteq \IR$, and the two maps $(0, 1) \rightrightarrows E$ are the inclusion map and $x \mapsto -x$. Then for any metric space $X$, the induced relation on non-expansive maps $(0, 1) \to X$ is that $f \sim g$ if and only if $$d(f(x), g(y)) \le x+y$$ for each $x, y \in (0, 1)$. This is reflexive since $d(f(x), f(y)) \le |x-y| < x+y$, and it is clearly symmetric. For transitivity, suppose $f\sim g$ and $g\sim h$. Then for any $\varepsilon > 0$, we have $$d(f(x), h(y)) \le d(f(x), g(\varepsilon)) + d(g(\varepsilon), h(y)) \le (x + \varepsilon) + (y + \varepsilon).$$ diff --git a/databases/catdat/data/categories/Met_c.yaml b/databases/catdat/data/categories/Met_c.yaml index bb8c99c1..f7854f0c 100644 --- a/databases/catdat/data/categories/Met_c.yaml +++ b/databases/catdat/data/categories/Met_c.yaml @@ -26,7 +26,7 @@ satisfied_properties: reason: Just restrict the metric to the equalizer built from the sets. - property: countable products - reason: For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking's book General Topology. + reason: For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) \coloneqq \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking's book General Topology. - property: coproducts reason: See MSE/5004389. diff --git a/databases/catdat/data/categories/Met_oo.yaml b/databases/catdat/data/categories/Met_oo.yaml index f79db0b9..d4d0754c 100644 --- a/databases/catdat/data/categories/Met_oo.yaml +++ b/databases/catdat/data/categories/Met_oo.yaml @@ -33,7 +33,7 @@ satisfied_properties: reason: We can use the same proof as for $\Met$ since the equation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ also holds for for $r, s_i \in \IR \cup \{\infty\}$. - property: infinitary extensive - reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i =: X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the restricted metric. If $f$ is non-expansive, each $f_i$ is non-expansive, and for $x_i \in Y_i$ and $i \neq j$ we have $d_Y(x_i,x_j) \geq d_X(f(x_i),f(x_j)) = \infty$, so that $Y = \coprod_i Y_i$ holds as metric spaces.' + reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the restricted metric. If $f$ is non-expansive, each $f_i$ is non-expansive, and for $x_i \in Y_i$ and $i \neq j$ we have $d_Y(x_i,x_j) \geq d_X(f(x_i),f(x_j)) = \infty$, so that $Y = \coprod_i Y_i$ holds as metric spaces.' unsatisfied_properties: - property: skeletal @@ -46,7 +46,7 @@ unsatisfied_properties: reason: 'Consider the metric subspace $\{(a,b) \in \IR^2 : a \leq b\}$ of $\IR^2$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \Met_{\infty} \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(a,b) \in U(X)^2 : d(x,y) \leq 1 \}$. Both are representable: $U$ by the singleton metric space and $R$ by the metric space $\{ 0,1 \}$ where $d(0,1) := 1$. It is clear that $R$ is reflexive, but not transitive.' + reason: 'See MO/509552: Consider the forgetful functor $U : \Met_{\infty} \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(a,b) \in U(X)^2 : d(x,y) \leq 1 \}$. Both are representable: $U$ by the singleton metric space and $R$ by the metric space $\{ 0,1 \}$ where $d(0,1) \coloneqq 1$. It is clear that $R$ is reflexive, but not transitive.' - property: cartesian closed reason: This is proven in MSE/5131457. diff --git a/databases/catdat/data/categories/Mon.yaml b/databases/catdat/data/categories/Mon.yaml index cc00e780..ecd4f46b 100644 --- a/databases/catdat/data/categories/Mon.yaml +++ b/databases/catdat/data/categories/Mon.yaml @@ -53,7 +53,7 @@ unsatisfied_properties: reason: If $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see MO/510431). This implies that in $\Mon$ the canonical homomorphism $\coprod_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable. - property: coregular - reason: 'Consider the monoid $M := \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not pushout-stable. Consider $N := \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' + reason: 'Consider the monoid $M \coloneqq \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not pushout-stable. Consider $N \coloneqq \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' - property: regular subobject classifier reason: 'Assume that $\Omega$ is a regular subobject classifier. Since the trivial monoid is a zero object, every regular submonoid $U \subseteq M$ of any monoid $M$ would have the form $\{m \in M : h(m) = 1 \}$ for some homomorphism $M \to \Omega$. Now take any monoid $M$ with zero that has two different homomorphisms with zero $f,g : M \rightrightarrows N$ (for example, let $M = N = \{0\} \cup \{x^n : n \geq 0\}$ be the free monoid with zero on one generator, $f(x) = 0$,and $g(x) = x$). Take their equalizer $U \subseteq M$, and choose a homomorphism $h : M \to \Omega$ with $U = \{m \in M : h(m) = 1\}$. Since $0 \in U$, we have $h(0)=1$. But then for all $m \in M$ we have $h(m) = h(m) h(0) = h(m 0) = h(0) = 1$, i.e. $U = M$, which yields the contradiction $f = g$.' @@ -70,7 +70,7 @@ unsatisfied_properties: - property: effective cocongruences reason: >- We adapt the counterexample from MO/510744 for $\Ring$. Namely, consider the monoids - $$\begin{align*} X & := \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\ E & := \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle. \end{align*}$$ + $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle. \end{align*}$$ Then $X$ represents the functor sending a monoid $M$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $M$ that $ab = b$, $ba = a$. The equations are equivalent to $aM = bM$, showing that the relation is indeed an equivalence relation. On the other hand, using the multiplicative map $$E \to M_{2\times 2}(\IZ), \quad p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},\quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix},$$ @@ -94,7 +94,7 @@ special_morphisms: description: injective homomorphisms reason: 'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.' epimorphisms: - description: 'A monoid map $f : T \to S$ is an epimorphism iff $S$ equals the dominion of $U := f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' + description: 'A monoid map $f : T \to S$ is an epimorphism iff $S$ equals the dominion of $U \coloneqq f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' reason: This is Isbell's zigzag Theorem, see references there. regular epimorphisms: description: surjective homomorphisms diff --git a/databases/catdat/data/categories/PMet.yaml b/databases/catdat/data/categories/PMet.yaml index 5237d792..797798b7 100644 --- a/databases/catdat/data/categories/PMet.yaml +++ b/databases/catdat/data/categories/PMet.yaml @@ -39,7 +39,7 @@ satisfied_properties: check_redundancy: false - property: binary products - reason: The product of two pseudo-metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) := \sup(d(x_1,x_2),d(y_1,y_2))$. + reason: The product of two pseudo-metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) \coloneqq \sup(d(x_1,x_2),d(y_1,y_2))$. check_redundancy: false - property: terminal object @@ -110,4 +110,4 @@ special_morphisms: reason: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. epimorphisms: description: surjective non-expansive maps - reason: 'Let $f : X \to Y$ be a non-expansive map that is not surjective. Choose $y_0 \in Y \setminus f(X)$. We extend the pseudo-metric from $Y$ to $Z := Y \sqcup \{y''_0\}$ via $d(y,y''_0) := d(y,y_0)$, i.e., we make $y_0,y''_0$ indistinguishable. Let $g : Y \to Z$ be the inclusion and $h : Y \to Z$ be the map that composes $g$ with the swap between $y_0$ and $y''_0$. Both are isometric and satisfy $g \circ f = h \circ f$. Therefore, $f$ is not an epimorphism.' + reason: 'Let $f : X \to Y$ be a non-expansive map that is not surjective. Choose $y_0 \in Y \setminus f(X)$. We extend the pseudo-metric from $Y$ to $Z \coloneqq Y \sqcup \{y''_0\}$ via $d(y,y''_0) \coloneqq d(y,y_0)$, i.e., we make $y_0,y''_0$ indistinguishable. Let $g : Y \to Z$ be the inclusion and $h : Y \to Z$ be the map that composes $g$ with the swap between $y_0$ and $y''_0$. Both are isometric and satisfy $g \circ f = h \circ f$. Therefore, $f$ is not an epimorphism.' diff --git a/databases/catdat/data/categories/Pos.yaml b/databases/catdat/data/categories/Pos.yaml index 6bd3a976..a1eda4c8 100644 --- a/databases/catdat/data/categories/Pos.yaml +++ b/databases/catdat/data/categories/Pos.yaml @@ -52,7 +52,7 @@ unsatisfied_properties: reason: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \Pos \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton poset and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \Pos \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton poset and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' - property: regular subobject classifier reason: Assume that there is a regular subobject classifier $\Omega$, so that (by the classification of regular monomorphisms) $\Hom(P,\Omega)$ is isomorphic to the set of subsets of $P$. By taking $P = \{0\}$ we see that $\Omega$ has $2$ elements, so that either $\Omega \cong \{0,1\}$ (discrete) or $\Omega \cong \{0 < 1\}$. By taking $P = \{0 < 1\}$ we see that $\Omega$ has four pairs $(x,y)$ with $x \leq y$. But $\{0,1\}$ has only two and $\{0 < 1\}$ has only three such pairs. @@ -87,4 +87,4 @@ special_morphisms: reason: 'Clearly, surjective maps are epimorphisms. Conversely, assume that $f : P \to Q$ is an order-preserving map which is not surjective. Choose $q \in Q \setminus f(P)$. The order-preserving maps $Q \to \{0 < 1\}$ correspond to the upper sets in $Q$, and composing them with $f$ corresponds to taking their $f$-preimages. Consider the two upper sets $Q_{> q}$ and $Q_{\geq q}$. Their $f$-preimages are the same since $q \notin f(P)$. Therefore, $f$ is not an epimorphism.' regular monomorphisms: description: embeddings - reason: 'Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C := Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p''$ in $C$ iff $p \leq p''$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a partial order, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.' + reason: 'Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C \coloneqq Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p''$ in $C$ iff $p \leq p''$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a partial order, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.' diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index efb9412f..5c0f008a 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -54,13 +54,13 @@ unsatisfied_properties: reason: 'Consider the subproset $\{(a,b) : a \leq b \}$ of $\IN^2$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' - property: cofiltered-limit-stable epimorphisms reason: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\Set \to \Prost$ that equips a set with the chaotic preorder. - property: effective cocongruences - reason: 'Consider the proset $E := \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.' + reason: 'Consider the proset $E \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.' special_objects: initial object: @@ -84,4 +84,4 @@ special_morphisms: reason: Clearly, surjective maps are epimorphisms. The converse follows since, as mentioned, the forgetful functor $\Prost \to \Set$ has a right adjoint hence preserves epimorphisms. regular monomorphisms: description: embeddings - reason: 'Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C := Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p''$ in $C$ iff $p \leq p''$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a preorder, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.' + reason: 'Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C \coloneqq Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p''$ in $C$ iff $p \leq p''$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a preorder, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.' diff --git a/databases/catdat/data/categories/Rel.yaml b/databases/catdat/data/categories/Rel.yaml index 67d4e8ee..460a1679 100644 --- a/databases/catdat/data/categories/Rel.yaml +++ b/databases/catdat/data/categories/Rel.yaml @@ -17,7 +17,7 @@ satisfied_properties: reason: The set of morphisms $X \to Y$ is the set $P(X \times Y)$. - property: self-dual - reason: 'There is an isomorphism $\Rel \to \Rel^{\op}$ that is the identity on objects (sets) and maps a relation $R \subseteq X \times Y$ to the opposite relation $R^{\op} \subseteq Y \times X$ defined by $R^{\op} := \{(y,x) : (x,y) \in R \}$.' + reason: 'There is an isomorphism $\Rel \to \Rel^{\op}$ that is the identity on objects (sets) and maps a relation $R \subseteq X \times Y$ to the opposite relation $R^{\op} \subseteq Y \times X$ defined by $R^{\op} \coloneqq \{(y,x) : (x,y) \in R \}$.' - property: pointed reason: The empty set is clearly both initial and terminal. The zero morphisms are the empty relations. diff --git a/databases/catdat/data/categories/Ring.yaml b/databases/catdat/data/categories/Ring.yaml index 08ee049a..13b0cc3b 100644 --- a/databases/catdat/data/categories/Ring.yaml +++ b/databases/catdat/data/categories/Ring.yaml @@ -50,10 +50,10 @@ unsatisfied_properties: reason: 'If $\sqcup$ denotes the coproduct of rings (see MSE/625874 for their description) and $R$ is a ring, the canonical morphism $R \sqcup \IZ^2 \to (R \sqcup \IZ)^2 = R^2$ is usually no isomorphism. For example, for $R = \IZ[X]$ the coproduct on the LHS is not commutative, it has the ring presentation $\langle X,E : E^2=E \rangle$.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \Ring \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $S$ by $\IZ \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \Ring \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $S$ by $\IZ \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' - property: coregular - reason: 'Let $B := M_2(\IQ)$ and $A := \IQ^2$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M := \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & 2 \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' + reason: 'Let $B \coloneqq M_2(\IQ)$ and $A \coloneqq \IQ^2$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & 2 \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' - property: regular quotient object classifier reason: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Ring$ would produce one in $\CRing$ by this lemma (dualized). diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index 75ea489d..34ed7537 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -76,9 +76,9 @@ unsatisfied_properties: - property: effective cocongruences reason: >- The counterexample is similar to the one at MO/510744 for $\Ring$: in this case, - $$X := \langle p \mid p^2 = p \rangle_{\Rng} \cong \IZ$$ + $$X \coloneqq \langle p \mid p^2 = p \rangle_{\Rng} \cong \IZ$$ and - $$E := \langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle_{\Rng} \cong \begin{pmatrix} \IZ & \IZ \\ 0 & 0 \end{pmatrix}$$ + $$E \coloneqq \langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle_{\Rng} \cong \begin{pmatrix} \IZ & \IZ \\ 0 & 0 \end{pmatrix}$$ via $$p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix}, \quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix}.$$ From here, the rest of the proof is similar to the one for $\Ring$. diff --git a/databases/catdat/data/categories/SemiGrp.yaml b/databases/catdat/data/categories/SemiGrp.yaml index 6acc26e6..cfab03e4 100644 --- a/databases/catdat/data/categories/SemiGrp.yaml +++ b/databases/catdat/data/categories/SemiGrp.yaml @@ -40,14 +40,14 @@ unsatisfied_properties: - property: balanced reason: |- - The inclusion of additive semigroups $\IN \hookrightarrow \IZ$ is a counterexample. Indeed, if $f,g : \IZ \to G$ are semigroup homomorphisms which agree on $\IN$, the element $e := f(0) = g(0)$ provides a neutral element for $eGe$, which therefore becomes a monoid, and $f,g$ corestrict to monoid homomorphisms $f,g : \IZ \to eGe$ which agree on $\IN$. And we already know that $f = g$ in that case (inverses are uniquely determined). + The inclusion of additive semigroups $\IN \hookrightarrow \IZ$ is a counterexample. Indeed, if $f,g : \IZ \to G$ are semigroup homomorphisms which agree on $\IN$, the element $e \coloneqq f(0) = g(0)$ provides a neutral element for $eGe$, which therefore becomes a monoid, and $f,g$ corestrict to monoid homomorphisms $f,g : \IZ \to eGe$ which agree on $\IN$. And we already know that $f = g$ in that case (inverses are uniquely determined). Another example can be found in MO/510431. - property: Malcev reason: 'Consider the subsemigroup $\{(a,b) : a \leq b \}$ of $\IN^2$ under addition.' - property: co-Malcev - reason: 'See MO/509552: Consider the forgetful functor $U : \SemiGrp \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by the free semigroup on a single generator and $R$ by the free semigroup on two generators $x,y$ subject to the relation $xy=x^2$. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509552: Consider the forgetful functor $U : \SemiGrp \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by the free semigroup on a single generator and $R$ by the free semigroup on two generators $x,y$ subject to the relation $xy=x^2$. It is clear that $R$ is reflexive, but not symmetric.' - property: semi-strongly connected reason: |- @@ -59,16 +59,16 @@ unsatisfied_properties: # (or missing_cogenerator) which handles this. reason: >- The proof is similar to the proof for $\Grp$. Assume that there is a cogenerating set $S$. There is an infinite simple group $G$ larger than all the semigroups in $S$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a semigroup $H \in S$ and a homomorphism of semigroups $f : G \to H$ with $f \neq f \circ 1$. Then - $$N := \{g \in G : f(g) = f(1)\}$$ + $$N \coloneqq \{g \in G : f(g) = f(1)\}$$ is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction. - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b := a$. + reason: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. - property: effective cocongruences reason: >- The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups - $$\begin{align*} X & := \langle p \mid p^2 = p \rangle,\\ E & := \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$ + $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$ whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$. - property: natural numbers object @@ -87,9 +87,9 @@ unsatisfied_properties: reason: >- We will find a regular monomorphism $\iota : F \to M$ of semigroups and a homomorphism $F \to K$ such that $K \to K \sqcup_F M$ is not injective. It is similar to our example for $\Mon$. Consider these semigroups defined by generators and relations: $$\begin{align*} - F & := \langle a,b,c,d \rangle \\ - M & := \langle a,b,c,d,s : as = c, \, bs = d \rangle \cong \langle a,b,s \rangle \\ - K & := \langle x,c,d \rangle \\ N & := \langle a,b,c,d,s_0,s_1 : as_i = c, \, bs_i = d \rangle \\ + F & \coloneqq \langle a,b,c,d \rangle \\ + M & \coloneqq \langle a,b,c,d,s : as = c, \, bs = d \rangle \cong \langle a,b,s \rangle \\ + K & \coloneqq \langle x,c,d \rangle \\ N & \coloneqq \langle a,b,c,d,s_0,s_1 : as_i = c, \, bs_i = d \rangle \\ & \cong \langle a,b,s_0,s_1 : a s_0 = a s_1, \, b s_0 = b s_1 \rangle \end{align*}$$ There is a canonical homomorphism $\iota : F \to M$, which is the equalizer of the two canonical homomorphisms $M \rightrightarrows N$ defined by $s \mapsto s_i$. We define $F \to K$ by $a \mapsto x$, $b \mapsto x$, $c \mapsto c$, $d \mapsto d$. Then @@ -117,7 +117,7 @@ special_morphisms: description: injective semigroup homomorphisms reason: 'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.' epimorphisms: - description: 'A semigroup homomorphism $f : T \to S$ is an epimorphism iff $S$ equals the dominion of $U := f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' + description: 'A semigroup homomorphism $f : T \to S$ is an epimorphism iff $S$ equals the dominion of $U \coloneqq f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' reason: This is Isbell's zigzag Theorem, see references there. regular epimorphisms: description: surjective homomorphisms diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index 604ba432..f94ba80a 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/databases/catdat/data/categories/Set_f.yaml @@ -70,13 +70,13 @@ unsatisfied_properties: reason: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\f$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetric, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' - property: countable copowers - reason: 'Assume that the copower $X := \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' + reason: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' - property: filtered reason: 'Consider the maps $f,g : \IN \rightrightarrows \IN$ defined by $f(x)=x$ and $g(x)=2x$. They are injective, hence finite-to-one. If a map $h : \IN \to X$ coequalizes them, we have $h(x)=h(2x)$, in particular $h(1)=h(2^n)$ for all $n \in \IN$. Thus, $h$ is not finite-to-one.' - property: sequential limits - reason: Consider the set $[n] := \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\f$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. + reason: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\f$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. special_objects: initial object: diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index 87bdc1f7..03f73510 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -72,7 +72,7 @@ unsatisfied_properties: reason: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces. - property: co-Malcev - reason: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' - property: coaccessible reason: Assume $\Top$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction. diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index e4f769b1..5a841270 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/databases/catdat/data/categories/Top_pointed.yaml @@ -83,7 +83,7 @@ unsatisfied_properties: reason: 'The functor $\IQ \times - : \Top_* \to \Top_*$ does not preserve colimits, see MSE/2969372. The counterexample also works for pointed spaces.' - property: co-Malcev - reason: 'We can adjust the proof for $\Top$ as follows: Consider the forgetful functor $U : \Top_* \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the discrete space $\{0,1\}$ with base point $0$ and $R$ by the Sierpinski space with an isolated base point added. It is clear that $R$ is reflexive, but not symmetric.' + reason: 'We can adjust the proof for $\Top$ as follows: Consider the forgetful functor $U : \Top_* \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the discrete space $\{0,1\}$ with base point $0$ and $R$ by the Sierpinski space with an isolated base point added. It is clear that $R$ is reflexive, but not symmetric.' - property: unital reason: 'The joint image of $X \to X \times Y \leftarrow Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset of $X \times Y$ when both $X,Y$ are non-trivial.' @@ -105,7 +105,7 @@ unsatisfied_properties: reason: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case. - property: effective cocongruences - reason: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I := \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' + reason: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' special_objects: initial object: diff --git a/databases/catdat/data/categories/sSet.yaml b/databases/catdat/data/categories/sSet.yaml index 7b378ddd..db08c4ea 100644 --- a/databases/catdat/data/categories/sSet.yaml +++ b/databases/catdat/data/categories/sSet.yaml @@ -25,7 +25,7 @@ satisfied_properties: reason: Let $X,Y$ be two simplicial sets. Assume that $X_0$ is empty. Then $X_n$ is empty for all $n$ since there is a morphism $[0] \to [n]$, hence a map $X_n \to X_0$. So there is a morphism $X \to Y$ for trivial reasons. If $X_0$ is non-empty, pick an element. By the Yoneda Lemma it corresponds to a morphism $\Delta^0 \to X$. Since $\Delta^0 = 1$ is terminal, there is a morphism $Y \to \Delta^0$, and these compose to a morphism $Y \to X$. - property: generator - reason: 'Let $\Delta^n := \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' + reason: 'Let $\Delta^n \coloneqq \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' - property: locally strongly finitely presentable reason: This follows from the fact that every category of presheaves over a small category is locally strongly finitely presentable. diff --git a/databases/catdat/data/categories/walking_fork.yaml b/databases/catdat/data/categories/walking_fork.yaml index f9ecd66f..687393fc 100644 --- a/databases/catdat/data/categories/walking_fork.yaml +++ b/databases/catdat/data/categories/walking_fork.yaml @@ -54,7 +54,7 @@ unsatisfied_properties: reason: Both $f$ and $g$ are monomorphisms and epimorphisms. - property: binary powers - reason: 'Assume that $X := 2 \times 2$ exists. Since there is a diagonal morphism $2 \to X$, we must have $X = 2$, and the two projections $p_1,p_2 : X \rightrightarrows 2$ must be equal to the identity. But $f,g$ induce a morphism $(f,g) : 1 \to X$ with $p_1 (f,g) = f$ and $p_2 (f,g) = g$, so that $f=g$, a contradiction.' + reason: 'Assume that $X \coloneqq 2 \times 2$ exists. Since there is a diagonal morphism $2 \to X$, we must have $X = 2$, and the two projections $p_1,p_2 : X \rightrightarrows 2$ must be equal to the identity. But $f,g$ induce a morphism $(f,g) : 1 \to X$ with $p_1 (f,g) = f$ and $p_2 (f,g) = g$, so that $f=g$, a contradiction.' special_objects: initial object: diff --git a/databases/catdat/data/categories/walking_splitting.yaml b/databases/catdat/data/categories/walking_splitting.yaml index e1141e9e..0cf23801 100644 --- a/databases/catdat/data/categories/walking_splitting.yaml +++ b/databases/catdat/data/categories/walking_splitting.yaml @@ -42,7 +42,7 @@ satisfied_properties: reason: 'The object $1$ a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$.' - property: preadditive - reason: 'We can define $\id_1 + \id_1 := ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\Vect_{\IF_2}$ that consists only of the trivial vector space $\{0\}$ and $\IF_2$. Since $\Vect_{\IF_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \IF_2$, $p : \IF_2 \to \{0\}$, and the zero morphism $ip : \IF_2 \to \IF_2$. Clearly, $pi$ is the identity.' + reason: 'We can define $\id_1 + \id_1 \coloneqq ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\Vect_{\IF_2}$ that consists only of the trivial vector space $\{0\}$ and $\IF_2$. Since $\Vect_{\IF_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \IF_2$, $p : \IF_2 \to \{0\}$, and the zero morphism $ip : \IF_2 \to \IF_2$. Clearly, $pi$ is the identity.' - property: sifted colimits reason: |- diff --git a/databases/catdat/data/category-implications/NNO.yaml b/databases/catdat/data/category-implications/NNO.yaml index e21f4d74..43c531db 100644 --- a/databases/catdat/data/category-implications/NNO.yaml +++ b/databases/catdat/data/category-implications/NNO.yaml @@ -13,7 +13,7 @@ - countably distributive conclusions: - natural numbers object - reason: 'Consider the copower $N := \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. We define $z := i_1 : 1 \to N$ and $s : N \to N$ by $s \circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$, $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$. The condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. This recursively defines the morphisms $\phi_n$. (We are basically using that $\IN$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' + reason: 'Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. We define $z \coloneqq i_1 : 1 \to N$ and $s : N \to N$ by $s \circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$, $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$. The condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. This recursively defines the morphisms $\phi_n$. (We are basically using that $\IN$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' is_equivalence: false - id: nno_pointed_case diff --git a/databases/catdat/data/category-implications/congruences.yaml b/databases/catdat/data/category-implications/congruences.yaml index 7496b165..b4a63847 100644 --- a/databases/catdat/data/category-implications/congruences.yaml +++ b/databases/catdat/data/category-implications/congruences.yaml @@ -67,7 +67,7 @@ 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. + In particular, applying the forward implications in the case $T \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq 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. is_equivalence: false - id: additive_effective_congruences_imply_normal @@ -77,7 +77,7 @@ conclusions: - normal reason: >- - 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$. + Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E \coloneqq 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 @@ -119,7 +119,7 @@ - mono-regular reason: >- 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'$$ + $$E \coloneqq B + B' + A + A'$$ and define the two morphisms $$f, g : E \rightrightarrows B + B'$$ by extending the identity on $B + B'$ and diff --git a/databases/catdat/data/category-implications/filtered colimits.yaml b/databases/catdat/data/category-implications/filtered colimits.yaml index 54184796..5e3ff90a 100644 --- a/databases/catdat/data/category-implications/filtered colimits.yaml +++ b/databases/catdat/data/category-implications/filtered colimits.yaml @@ -46,7 +46,7 @@ - direct conclusions: - sequential limits - reason: Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 := n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction. + reason: Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 \coloneqq n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction. is_equivalence: false - id: finite_filtered_colimits diff --git a/databases/catdat/data/category-implications/generators.yaml b/databases/catdat/data/category-implications/generators.yaml index aad6d66a..f173956b 100644 --- a/databases/catdat/data/category-implications/generators.yaml +++ b/databases/catdat/data/category-implications/generators.yaml @@ -16,7 +16,7 @@ - zero morphisms conclusions: - generator - reason: 'If $S$ is a generating set, we claim that $U := \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' + reason: 'If $S$ is a generating set, we claim that $U \coloneqq \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' is_equivalence: false - id: free-algebra-generates diff --git a/databases/catdat/data/category-implications/topos.yaml b/databases/catdat/data/category-implications/topos.yaml index 8e294228..cb2943ca 100644 --- a/databases/catdat/data/category-implications/topos.yaml +++ b/databases/catdat/data/category-implications/topos.yaml @@ -75,5 +75,5 @@ - countable coproducts conclusions: - trivial - reason: 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$. + reason: Let $N \coloneqq \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$. is_equivalence: false diff --git a/databases/catdat/data/category-properties/copowers.yaml b/databases/catdat/data/category-properties/copowers.yaml index e3af72e9..e47a319e 100644 --- a/databases/catdat/data/category-properties/copowers.yaml +++ b/databases/catdat/data/category-properties/copowers.yaml @@ -1,6 +1,6 @@ id: copowers relation: has -description: If $X$ is an object and $I$ is a set, the copower is defined as the coproduct $I \otimes X := \coprod_{i \in I} X$. This property refers to the existence of copowers. +description: If $X$ is an object and $I$ is a set, the copower is defined as the coproduct $I \otimes X \coloneqq \coprod_{i \in I} X$. This property refers to the existence of copowers. nlab_link: https://ncatlab.org/nlab/show/copower dual_property: powers invariant_under_equivalences: true diff --git a/databases/catdat/data/category-properties/powers.yaml b/databases/catdat/data/category-properties/powers.yaml index 6e90b71a..421153b4 100644 --- a/databases/catdat/data/category-properties/powers.yaml +++ b/databases/catdat/data/category-properties/powers.yaml @@ -1,6 +1,6 @@ id: powers relation: has -description: If $X$ is an object and $I$ is a set, the power is defined as the product $X^I := \prod_{i \in I} X$. This property refers to the existence of powers. +description: If $X$ is an object and $I$ is a set, the power is defined as the product $X^I \coloneqq \prod_{i \in I} X$. This property refers to the existence of powers. nlab_link: https://ncatlab.org/nlab/show/powering dual_property: copowers invariant_under_equivalences: true diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml index 37bae25d..a46a43bd 100644 --- a/databases/catdat/data/functors/abelianization.yaml +++ b/databases/catdat/data/functors/abelianization.yaml @@ -2,7 +2,7 @@ id: abelianization name: abelianization functor for groups source: Grp target: Ab -description: This functor maps a group $G$ to its abelianization $G^{\ab} := G/[G,G]$. +description: This functor maps a group $G$ to its abelianization $G^{\ab} \coloneqq G/[G,G]$. nlab_link: https://ncatlab.org/nlab/show/abelianization satisfied_properties: diff --git a/databases/catdat/data/functors/power_set_covariant.yaml b/databases/catdat/data/functors/power_set_covariant.yaml index bd7c6448..4990a422 100644 --- a/databases/catdat/data/functors/power_set_covariant.yaml +++ b/databases/catdat/data/functors/power_set_covariant.yaml @@ -17,7 +17,7 @@ satisfied_properties: unsatisfied_properties: - property: coequalizer-preserving - reason: 'Let $X := \{x,y\}$. Consider the two maps $x,y : \{0\} \rightrightarrows X$. Their coequalizer $Q = X / (x = y)$ has just one element, so that $P(Q)$ has two elements. The induced maps $x_*,y_* : P(\{0\}) \rightrightarrows P(X)$ (which already agree on the empty set) have coequalizer $P(X) / (\{x\} = \{y\})$, which has $3$ elements. So it cannot be $P(Q)$.' + reason: 'Let $X \coloneqq \{x,y\}$. Consider the two maps $x,y : \{0\} \rightrightarrows X$. Their coequalizer $Q = X / (x = y)$ has just one element, so that $P(Q)$ has two elements. The induced maps $x_*,y_* : P(\{0\}) \rightrightarrows P(X)$ (which already agree on the empty set) have coequalizer $P(X) / (\{x\} = \{y\})$, which has $3$ elements. So it cannot be $P(Q)$.' - property: equalizer-preserving reason: 'Any pair of distinct surjective maps $f,g : X \rightrightarrows Y$ provides a counterexample: Their equalizer $E$ is a proper subset of $X$, so that $P(E)$ cannot contain $X$. But $f_*(X) = Y = g_*(X)$ shows that $X$ is contained in the equalizer of $f_*,g_* : P(X) \rightrightarrows P(Y)$.' - property: essentially surjective diff --git a/databases/catdat/data/lemmas/generator_construction.yaml b/databases/catdat/data/lemmas/generator_construction.yaml index a204432d..9ca26cb2 100644 --- a/databases/catdat/data/lemmas/generator_construction.yaml +++ b/databases/catdat/data/lemmas/generator_construction.yaml @@ -2,6 +2,6 @@ id: generator_construction title: Construction of Generators -claim: In a category let $S$ be a generating set which is strongly connected (between any two objects in $S$ there is a morphism). If the coproduct $U := \coprod_{G \in S} G$ exists, then it is a generator. +claim: In a category let $S$ be a generating set which is strongly connected (between any two objects in $S$ there is a morphism). If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. proof: 'This is a straight forward generalization of this result. We remark that the assumption about $S$ implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' diff --git a/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml b/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml index 375c718b..da44fc8f 100644 --- a/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml +++ b/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml @@ -4,4 +4,4 @@ title: Construction of a colimit of a sequence of monomorphisms as a quotient of claim: 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} := 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.' +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.' diff --git a/databases/catdat/data/lemmas/nno_distributive_criterion.yaml b/databases/catdat/data/lemmas/nno_distributive_criterion.yaml index f8926df4..e1313e6d 100644 --- a/databases/catdat/data/lemmas/nno_distributive_criterion.yaml +++ b/databases/catdat/data/lemmas/nno_distributive_criterion.yaml @@ -11,16 +11,16 @@ proof: >- We will use generalized elements extensively. In particular, for every element $a \in A$ and $n \in \IN$ there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by $$\alpha(n \otimes a) = (a , n \otimes 1).$$ In any category with finite products and arbitrary copowers, we can construct the non-parameterized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map - $$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) := (n+1) \otimes 1.$$ + $$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) \coloneqq (n+1) \otimes 1.$$ Its universal property states that it is initial in the category of pairs $1 \xrightarrow{x_0} X \xrightarrow{r} X$. Hence, it is unique up to isomorphism. Since by assumption $1 \xrightarrow{z} N \xrightarrow{s} N$ is a full, parameterized NNO, it is also a non-parameterized NNO and therefore isomorphic to the one described. We will assume w.l.o.g. that it is equal to it and continue to work with $N = \IN \otimes 1$. Next, we apply the (parameterized) universal property of the NNO to the diagram $$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$ - defined by $f(a) := 0 \otimes a$ and $g(n \otimes a) := (n+1) \otimes a$. It tells us that there is a map + defined by $f(a) \coloneqq 0 \otimes a$ and $g(n \otimes a) \coloneqq (n+1) \otimes a$. It tells us that there is a map $$\Phi : A \times N \to \IN \otimes A$$ with $$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a, s(m)) = g(\Phi(a,m)).$$ - For $m := n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads + For $m \coloneqq n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads $$\Phi(a, (n+1) \otimes 1) = g(\Phi(a, n \otimes 1)).$$ By classical induction on $n \in \IN$ it follows that $$\Phi(a, n \otimes 1) = n \otimes a,$$ diff --git a/databases/catdat/data/lemmas/preadditive_structure_unique.yaml b/databases/catdat/data/lemmas/preadditive_structure_unique.yaml index a6118dba..c5446112 100644 --- a/databases/catdat/data/lemmas/preadditive_structure_unique.yaml +++ b/databases/catdat/data/lemmas/preadditive_structure_unique.yaml @@ -14,7 +14,7 @@ proof: >- $$p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y,$$ $$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0.$$ It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define - $$\beta := i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y.$$ + $$\beta \coloneqq i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y.$$ Then $\alpha \circ \beta = \id_{X \times Y}$ because $$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_1 \circ p_1 + 0 \circ p_2 = p_1$$ and likewise $p_2 \circ \alpha \circ \beta = p_2$. We also have $\beta \circ \alpha = \id_{X \oplus Y}$ with a very similar calculation that shows $\beta \circ \alpha \circ i_1 = i_1$ and $\beta \circ \alpha \circ i_2 = i_2$. Therefore, for morphisms $f,g : A \rightrightarrows B$ the composite $A \to B$ in the claim is equal to From 00439f9900bb5a3736f7d73fbd3052dd1664dd55 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 02:27:23 +0200 Subject: [PATCH 2/7] replace all \colon with : (such as in f : X \to Y) this is not recommended by others for semantic reasons, but I find the spacing much better --- .../walking_parallel_pair_sifted_colimit.md | 20 +++++++++---------- databases/catdat/data/categories/CMon.yaml | 2 +- databases/catdat/data/categories/Sp.yaml | 2 +- databases/catdat/data/categories/Top.yaml | 2 +- .../catdat/data/categories/Top_pointed.yaml | 2 +- .../catdat/data/categories/walking_span.yaml | 2 +- .../category-implications/completeness.yaml | 2 +- .../data/category-implications/groupoids.yaml | 2 +- .../category-properties/multi-cocomplete.yaml | 2 +- .../category-properties/multi-complete.yaml | 2 +- 10 files changed, 19 insertions(+), 19 deletions(-) diff --git a/content/walking_parallel_pair_sifted_colimit.md b/content/walking_parallel_pair_sifted_colimit.md index a67b6d58..5def3939 100644 --- a/content/walking_parallel_pair_sifted_colimit.md +++ b/content/walking_parallel_pair_sifted_colimit.md @@ -6,22 +6,22 @@ author: Yuto Kawase ## The walking parallel pair has sifted colimits -We will prove that the [walking parallel pair](/category/walking_pair) $\{u,v \colon 0 \rightrightarrows 1\}$ has [sifted colimits](/category-property/sifted_colimits). +We will prove that the [walking parallel pair](/category/walking_pair) $\{u,v : 0 \rightrightarrows 1\}$ has [sifted colimits](/category-property/sifted_colimits). -Let $D \colon \C \to \{u,v \colon 0 \rightrightarrows 1\}$ be a functor from a sifted category. If the object $1$ is not contained in the image under $D$, the object $0$ gives a colimit of $D$ because the sifted category $\C$ is connected. +Let $D : \C \to \{u,v : 0 \rightrightarrows 1\}$ be a functor from a sifted category. If the object $1$ is not contained in the image under $D$, the object $0$ gives a colimit of $D$ because the sifted category $\C$ is connected. In what follows, we suppose that there is an object $c_0 \in \C$ such that $D(c_0)=1$. -We first claim that for every object $c \in \C$ such that $D(c)=0$, there is a morphism $f \colon c \to x$ with $D(x)=1$; moreover, which of $u$ and $v$ such a morphism is sent to by $D$ is independent of the choice of $f$. +We first claim that for every object $c \in \C$ such that $D(c)=0$, there is a morphism $f : c \to x$ with $D(x)=1$; moreover, which of $u$ and $v$ such a morphism is sent to by $D$ is independent of the choice of $f$. The existence of $f$ is easy. Indeed, since $\C$ is sifted, there is a cospan $c \rightarrow x \leftarrow c_0$, and $D(x)=1$ follows from $D(c_0)=1$. -To show the independence of the value of $D(f)$, suppose that there are morphisms $f \colon c \to x$ and $g \colon c \to y$ such that $D(f)=u$ and $D(g)=v$. -Since $\C$ is sifted, there is a cospan consisting of $p\colon x \rightarrow z$ and $q \colon z \leftarrow y$. +To show the independence of the value of $D(f)$, suppose that there are morphisms $f : c \to x$ and $g : c \to y$ such that $D(f)=u$ and $D(g)=v$. +Since $\C$ is sifted, there is a cospan consisting of $p : x \rightarrow z$ and $q : z \leftarrow y$. Since $\C$ is sifted again, two cospans $(p \circ f, q \circ g)$ and $(\id_c, \id_c)$ are connected to each other, that is, there are a zigzag consisting of -- $s_i \colon d_{i-1} \rightarrow e_i$, -- $t_i \colon e_i \leftarrow d_i$ $(1 \le i \le n)$, and -- parallel pairs $(l_i,r_i) \colon c \rightrightarrows d_i$ $(0 \le i \le n)$ +- $s_i : d_{i-1} \rightarrow e_i$, +- $t_i : e_i \leftarrow d_i$ $(1 \le i \le n)$, and +- parallel pairs $(l_i,r_i) : c \rightrightarrows d_i$ $(0 \le i \le n)$ such that @@ -44,10 +44,10 @@ By the claim, each object $c \in \C$ can be classified exclusively into the foll 2. $D(c)=0$ and there is a morphism from itself sent to $u$ by $D$; 3. $D(c)=0$ and there is a morphism from itself sent to $v$ by $D$. -Now, we have a cocone $(\alpha_c \colon D(c) \to 1)_{c \in \C}$ under $D$ by letting $\alpha_c \coloneqq \id_1$ if $c$ is classified into the first case, $\alpha_c \coloneqq u$ for the second case, and $\alpha_c \coloneqq v$ for the third case. +Now, we have a cocone $(\alpha_c : D(c) \to 1)_{c \in \C}$ under $D$ by letting $\alpha_c \coloneqq \id_1$ if $c$ is classified into the first case, $\alpha_c \coloneqq u$ for the second case, and $\alpha_c \coloneqq v$ for the third case. Moreover, this is a unique cocone under $D$: If $\beta$ is another cocone, its vertex should be $1$ by the existence of $c_0$. If $c \in \C$ is classified into the first case, $\beta_c$ should be the identity. -For the second case, taking a morphism $f \colon c \to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$. +For the second case, taking a morphism $f : c \to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$. Similarly, we have $\beta_c = v$ for the third case. This concludes $\beta = \alpha$, and since there is no non-trivial endomorphism on the vertex $1$, $\alpha$ gives a colimit. diff --git a/databases/catdat/data/categories/CMon.yaml b/databases/catdat/data/categories/CMon.yaml index b7a35bd9..171ebba7 100644 --- a/databases/catdat/data/categories/CMon.yaml +++ b/databases/catdat/data/categories/CMon.yaml @@ -45,7 +45,7 @@ unsatisfied_properties: reason: See MO/509232. - property: coregular - reason: 'We can show this analogously to the case of commutative rings MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U \coloneqq \{(m,n)\mid m\ge n\}$ with the inclusion $i\colon U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D \coloneqq \{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j\colon U\hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I \coloneqq \{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v\colon D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' + reason: 'We can show this analogously to the case of commutative rings MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U \coloneqq \{(m,n)\mid m\ge n\}$ with the inclusion $i : U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D \coloneqq \{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j : U \hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I \coloneqq \{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v : D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' - property: regular subobject classifier reason: We can use exactly the same proof as for $\Mon$. diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 317929af..22a5d9a4 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -34,7 +34,7 @@ unsatisfied_properties: reason: 'Disclaimer: This result and its proof are not relevant for category theory and are also depending on the concrete model of set theory. That this category is locally essentially small is only what matters. Now, consider the terminal species $F=G=1$. Then $\Hom(F,G)$ has just a single element, namely the natural transformation $\alpha$ that sends every finite set $X$ to the unique map $\alpha_X : 1 \to 1$. Formally, $\alpha$ is a map, modelled as a set of ordered pairs $(X,\id_1)$, where $X$ is a finite set. Hence, $\alpha$ is not a set (since finite sets do not form a set), and therefore $\Hom(F,G) = \{\alpha\}$ is also not a set.' - property: essentially countable - reason: Any function $f\colon\IN \to \IN$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species. + reason: 'Any function $f : \IN \to \IN$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.' - property: countable powers reason: If $\Sp \simeq \FinSet \times \prod_{n > 0} \Sigma_n{-}\FinSet$ has countable powers, then $\FinSet$ has countable powers as well by this lemma, which we already know is false. diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index 03f73510..3cb1e221 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -75,7 +75,7 @@ unsatisfied_properties: reason: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' - property: coaccessible - reason: Assume $\Top$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction. + reason: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' - property: cofiltered-limit-stable epimorphisms reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Top$ which equips a set with the indiscrete topology. diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index 5a841270..d9f3e38c 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/databases/catdat/data/categories/Top_pointed.yaml @@ -96,7 +96,7 @@ unsatisfied_properties: reason: We can recycle the proof for $\Set_*$ using discrete topological spaces. - property: coaccessible - reason: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' + reason: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' - property: cofiltered-limit-stable epimorphisms reason: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. diff --git a/databases/catdat/data/categories/walking_span.yaml b/databases/catdat/data/categories/walking_span.yaml index 2d11940c..20cc2f60 100644 --- a/databases/catdat/data/categories/walking_span.yaml +++ b/databases/catdat/data/categories/walking_span.yaml @@ -38,7 +38,7 @@ satisfied_properties: reason: The slice category over $0$ is the trivial category, and the slice category over $1$ is the walking morphism, which is cartesian closed. The same holds for $2$ by symmetry. - property: multi-algebraic - reason: We first remark that for a set $X$, the identity span $(\id,\id)\colon X \leftarrow X \rightarrow X$ exhibits a product if and only if $X$ is either a singleton or the empty set. Therefore, there is a (finite product, coproduct)-sketch whose $\Set$-model is precisely a pair $(X,Y)$ of sets such that each of $X$ and $Y$ is either a singleton or the empty set and the product $X \times Y$ is the empty set. Any $\Set$-model of such a sketch is isomorphic to either $(\varnothing, \varnothing)$, $(\varnothing, 1)$, or $(1, \varnothing)$; hence the category of models is equivalent to the walking span. + reason: 'We first remark that for a set $X$, the identity span $(\id,\id) : X \leftarrow X \rightarrow X$ exhibits a product if and only if $X$ is either a singleton or the empty set. Therefore, there is a (finite product, coproduct)-sketch whose $\Set$-model is precisely a pair $(X,Y)$ of sets such that each of $X$ and $Y$ is either a singleton or the empty set and the product $X \times Y$ is the empty set. Any $\Set$-model of such a sketch is isomorphic to either $(\varnothing, \varnothing)$, $(\varnothing, 1)$, or $(1, \varnothing)$; hence the category of models is equivalent to the walking span.' unsatisfied_properties: - property: sifted diff --git a/databases/catdat/data/category-implications/completeness.yaml b/databases/catdat/data/category-implications/completeness.yaml index 1019c86f..029f5313 100644 --- a/databases/catdat/data/category-implications/completeness.yaml +++ b/databases/catdat/data/category-implications/completeness.yaml @@ -68,5 +68,5 @@ - multi-complete conclusions: - complete - reason: Let $D\colon \S \to \C$ be a small diagram in a category $\C$. Since $\C$ has finite coproducts, the category $\Cone(D)$ of cones over $D$ has finite coproducts. In particular, $\Cone(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object. + reason: 'Let $D : \S \to \C$ be a small diagram in a category $\C$. Since $\C$ has finite coproducts, the category $\Cone(D)$ of cones over $D$ has finite coproducts. In particular, $\Cone(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object.' is_equivalence: false diff --git a/databases/catdat/data/category-implications/groupoids.yaml b/databases/catdat/data/category-implications/groupoids.yaml index 02abedbc..df267bf0 100644 --- a/databases/catdat/data/category-implications/groupoids.yaml +++ b/databases/catdat/data/category-implications/groupoids.yaml @@ -46,5 +46,5 @@ - multi-terminal object conclusions: - thin - reason: Let $f,g\colon A \rightrightarrows B$ be a parallel pair of morphisms. Since the category has a multi-terminal object, the connected component containing $A$ and $B$ has a terminal object. But since the category is a groupoid, both $A$ and $B$ are terminal objects in the connected component, hence $f=g$. + reason: 'Let $f,g : A \rightrightarrows B$ be a parallel pair of morphisms. Since the category has a multi-terminal object, the connected component containing $A$ and $B$ has a terminal object. But since the category is a groupoid, both $A$ and $B$ are terminal objects in the connected component, hence $f=g$.' is_equivalence: false diff --git a/databases/catdat/data/category-properties/multi-cocomplete.yaml b/databases/catdat/data/category-properties/multi-cocomplete.yaml index 69665468..465bf1e5 100644 --- a/databases/catdat/data/category-properties/multi-cocomplete.yaml +++ b/databases/catdat/data/category-properties/multi-cocomplete.yaml @@ -1,6 +1,6 @@ id: multi-cocomplete relation: is -description: A multi-colimit of a diagram $D\colon \S \to \C$ is a set $I$ of cocones under $D$ such that every cocone under $D$ uniquely factors through a unique cocone belonging to $I$. This property refers to the existence of multi-colimits of small diagrams. Note that any diagram with no cocone admits a multi-colimit, which is the empty set of cocones. +description: 'A multi-colimit of a diagram $D : \S \to \C$ is a set $I$ of cocones under $D$ such that every cocone under $D$ uniquely factors through a unique cocone belonging to $I$. This property refers to the existence of multi-colimits of small diagrams. Note that any diagram with no cocone admits a multi-colimit, which is the empty set of cocones.' nlab_link: https://ncatlab.org/nlab/show/multilimit dual_property: multi-complete invariant_under_equivalences: true diff --git a/databases/catdat/data/category-properties/multi-complete.yaml b/databases/catdat/data/category-properties/multi-complete.yaml index 6dfc881b..9f8497f6 100644 --- a/databases/catdat/data/category-properties/multi-complete.yaml +++ b/databases/catdat/data/category-properties/multi-complete.yaml @@ -1,6 +1,6 @@ id: multi-complete relation: is -description: A multi-limit of a diagram $D\colon \S \to \C$ is a set $I$ of cones over $D$ such that every cone over $D$ uniquely factors through a unique cone belonging to $I$. This property refers to the existence of multi-limits of small diagrams. Note that any diagram with no cone admits a multi-limit, which is the empty set of cones. +description: 'A multi-limit of a diagram $D : \S \to \C$ is a set $I$ of cones over $D$ such that every cone over $D$ uniquely factors through a unique cone belonging to $I$. This property refers to the existence of multi-limits of small diagrams. Note that any diagram with no cone admits a multi-limit, which is the empty set of cones.' nlab_link: https://ncatlab.org/nlab/show/multilimit dual_property: multi-cocomplete invariant_under_equivalences: true From 8a7a153c6516aae7997248098e84166525d7e39e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 04:39:07 +0200 Subject: [PATCH 3/7] update conventions --- CONTRIBUTING.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e91445b0..9ac21ba6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -169,9 +169,11 @@ As a practical guideline, avoid introducing more than four properties (or four c ### Conventions -1. Use `\varnothing` to display the empty set, not `\emptyset`. -2. Write `non-empty`, not `nonempty`. Same for `non-unital`, `non-expansive`, etc. -3. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](databases/catdat/data/macros.yaml). +1. Write `non-empty`, not `nonempty`. Same for `non-unital`, `non-expansive`, etc. +2. Use `\varnothing` to display the empty set, not `\emptyset`. +3. For declarations of functions or morphisms use `f : X \to Y`, not `f \colon X \to Y`. +4. For definitions use `\coloneqq` instead of `:=`. +5. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](databases/catdat/data/macros.yaml). ### Responsible Use of AI From 082d1931b2a27421e9205b302c4c53f9e802d2c2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 04:41:23 +0200 Subject: [PATCH 4/7] replace \simeq by \cong for isomorphisms --- content/comphaus_copresentable.md | 2 +- content/congruences_in_rel.md | 2 +- databases/catdat/data/categories/CompHaus.yaml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md index 696caef7..1e04850e 100644 --- a/content/comphaus_copresentable.md +++ b/content/comphaus_copresentable.md @@ -43,7 +43,7 @@ The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Original _Proof._ We use the crude monadicity theorem (see e.g. [SGL92](#references), Thm. IV.4.2). First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism -$$\Hom_{\CompHaus}(X, [0, 1]^S) \simeq \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])).$$ +$$\Hom_{\CompHaus}(X, [0, 1]^S) \cong \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])).$$ To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$ by Urysohn's lemma. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then by Urysohn's lemma there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism. diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md index e5e1ac1e..2287a49e 100644 --- a/content/congruences_in_rel.md +++ b/content/congruences_in_rel.md @@ -12,7 +12,7 @@ Let $i : E \hookrightarrow X \times X$ be a congruence in $\Rel$. Recall that pr $$R_* : P(X) \to P(Y),\, S \mapsto \bigl\{ y\in Y \mid \exists x\in S, (x, y) \in R \bigr\}$$ is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\Set$. In particular, we get -$$i_* : P(E) \to P(X + X) \simeq P(X) \times P(X)$$ +$$i_* : P(E) \to P(X + X) \cong P(X) \times P(X)$$ which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $i$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions. Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \id$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\Set$. diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml index 4e93e2e0..a1249639 100644 --- a/databases/catdat/data/categories/CompHaus.yaml +++ b/databases/catdat/data/categories/CompHaus.yaml @@ -91,7 +91,7 @@ unsatisfied_properties: reason: |- Consider the $\IN$-codirected systems $X_n \coloneqq [0, 1] \times [0, 1/n]$ with the maps $X_{n+1} \to X_n$ being inclusion maps, and $Y_n \coloneqq [0, 1+1/n]$ with the maps $Y_{n+1} \to Y_n$ also being inclusion maps. We define $f_n : X_n \to Y_n$, $(x, y) \mapsto x$ and $g_n : X_n \to Y_n$, $(x, y) \mapsto x+y$. It is straightforward to check these give morphisms of $\IN$-codirected systems in $\CompHaus$. Now for each $n$, we claim the coequalizer of $f_n$ and $g_n$ is a singleton space. To see this, we prove the more general result that for $r, s > 0$ the coequalizer of $f, g : [0, r] \times [0, s] \rightrightarrows [0, r+s]$, $f(x,y) = x$, $g(x,y) = x+y$ is a singleton. We must show that for any $h : [0, r+s] \to T$ with $h\circ f = h\circ g$, then $h$ is constant. To this end, we show by induction on $n$ that whenever $x \in [0, r+s]$ and $x \le ns$, we have $h(x) = h(0)$. The base case $n=0$ is trivial. For the inductive step, if $x \le s$, then $f(0,x) = 0$ and $g(0,x) = x$, so $h(0) = h(x)$. Otherwise, we have $x-s \in [0,r]$ and $x-s \le (n-1)s$, so by inductive hypothesis $h(x-s) = h(0)$. Also, $f(x-s, s) = x-s$ and $g(x-s, s) = x$, so $h(x-s) = h(x)$, completing the induction. With this established, the desired result follows from the case $n \coloneqq \lceil r/s \rceil + 1$. - On the other hand, $\lim X_n \simeq [0, 1] \times \{ 0 \}$; $\lim Y_n \simeq [0, 1]$; and $\lim f_n = \lim g_n$, $(x, 0) \mapsto x$. Thus, the coequalizer of $\lim f_n$ and $\lim g_n$ is $[0, 1]$, showing that the limit does not preserve this coequalizer. + On the other hand, $\lim X_n \cong [0, 1] \times \{ 0 \}$; $\lim Y_n \cong [0, 1]$; and $\lim f_n = \lim g_n$, $(x, 0) \mapsto x$. Thus, the coequalizer of $\lim f_n$ and $\lim g_n$ is $[0, 1]$, showing that the limit does not preserve this coequalizer. special_objects: initial object: From 24223ce3619222903d46dd108e796fd3fbe1236b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 04:45:59 +0200 Subject: [PATCH 5/7] macros for fraktur letters --- databases/catdat/data/categories/CAlg(R).yaml | 2 +- databases/catdat/data/categories/LRS.yaml | 2 +- databases/catdat/data/macros.yaml | 4 ++++ 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index f64e5c9e..77e873e4 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -45,7 +45,7 @@ unsatisfied_properties: reason: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A \coloneqq K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.' - property: semi-strongly connected - reason: Choose a maximal ideal $\mathfrak{m}$ of $R$, so $K \coloneqq R/\mathfrak{m}$ is a field. If $\CAlg(R)$ is semi-strongly connected, then also $\CAlg(K)$ is semi-strongly connected. This has been disproven in MSE/5129689. + reason: Choose a maximal ideal $\m$ of $R$, so $K \coloneqq R/\m$ is a field. If $\CAlg(R)$ is semi-strongly connected, then also $\CAlg(K)$ is semi-strongly connected. This has been disproven in MSE/5129689. - property: coregular reason: See MSE/3745302. diff --git a/databases/catdat/data/categories/LRS.yaml b/databases/catdat/data/categories/LRS.yaml index 2db18e49..5e36bcaa 100644 --- a/databases/catdat/data/categories/LRS.yaml +++ b/databases/catdat/data/categories/LRS.yaml @@ -23,7 +23,7 @@ satisfied_properties: reason: See Demazure-Gabriel's "Groupes algébriques", I. §1. 1.6. Specifically, the forgetful functor to ringed spaces preserves colimits, and colimits of ringed spaces are built from colimits of topological spaces and limits of commutative rings, see MSE/1646202. - property: well-powered - reason: 'Let $f : X \to Y$ be a monomorphism of locally ringed spaces. I claim that $f$ is injective, from which the claim will follow. The diagonal $\Delta : X \to X \times_Y X$ is an isomorphism. By the explicit construction of fiber products, $X \times_Y X$ consists of triples $(x_1,x_2,\mathfrak{p})$ where $x_1,x_2 \in X$, $y \coloneqq f(x_1) = f(x_2)$ and $\mathfrak{p}$ is a prime ideal in $k(x_1) \otimes_{k(y)} k(x_2)$. The map $\Delta$ is given by $\Delta(x) = \bigl(x,x,\ker(k(x) \otimes_{k(f(x))} k(x) \to k(x)\bigr)$, and it is bijective. This clearly implies that $f$ is injective (and that each tensor product $k(x) \otimes_{k(f(x))} k(x)$ has a unique prime ideal, namely the kernel mentioned).' + reason: 'Let $f : X \to Y$ be a monomorphism of locally ringed spaces. I claim that $f$ is injective, from which the claim will follow. The diagonal $\Delta : X \to X \times_Y X$ is an isomorphism. By the explicit construction of fiber products, $X \times_Y X$ consists of triples $(x_1,x_2,\p)$ where $x_1,x_2 \in X$, $y \coloneqq f(x_1) = f(x_2)$ and $\p$ is a prime ideal in $k(x_1) \otimes_{k(y)} k(x_2)$. The map $\Delta$ is given by $\Delta(x) = \bigl(x,x,\ker(k(x) \otimes_{k(f(x))} k(x) \to k(x)\bigr)$, and it is bijective. This clearly implies that $f$ is injective (and that each tensor product $k(x) \otimes_{k(f(x))} k(x)$ has a unique prime ideal, namely the kernel mentioned).' - property: well-copowered reason: It is enough to prove that every epimorphism of locally ringed spaces is surjective. The forgetful functor $\LRS \to \RS$ has a right adjoint (see Localization of ringed spaces by W. Gillam), so it preserves epimorphisms. The forgetful functor $\RS \to \Top$ also has a right adjoint, namely $X \mapsto (X,\underline{\IZ})$, so it also preserves epimorphisms. diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 5a4f891d..fe6c8e5b 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -24,6 +24,10 @@ \S: \mathcal{S} \T: \mathcal{T} +# fraktur letters +\p: \mathfrak{p} +\m: \mathfrak{m} + # abbreviations \op: \mathrm{op} \c: \mathrm{c} From 0c17d31abe11a3645a102606f082dad81077a0ef Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 04:47:18 +0200 Subject: [PATCH 6/7] remove check this can be checked in code reviews --- src/lib/server/formulas.ts | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/lib/server/formulas.ts b/src/lib/server/formulas.ts index fa5abc97..645bcdf4 100644 --- a/src/lib/server/formulas.ts +++ b/src/lib/server/formulas.ts @@ -8,12 +8,6 @@ export function render_formula( formula: string, options: { displayMode: boolean } = { displayMode: false }, ): string { - if (formula.includes('\\emptyset')) { - console.warn( - `Warning: Use \\varnothing instead of \\emptyset.\nFormula: ${formula}`, - ) - } - return katex.renderToString(formula, { throwOnError: true, macros: MACROS, From a610d99ffd1b40e524aa2eaa93fe85f64ccbb0bd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 04:55:38 +0200 Subject: [PATCH 7/7] adjust sizes of brackets --- content/comphaus_copresentable.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md index 1e04850e..ae8f0b3a 100644 --- a/content/comphaus_copresentable.md +++ b/content/comphaus_copresentable.md @@ -13,7 +13,7 @@ A good overview of some of these results is contained in the introduction of [HN We first prove a couple preliminary results. ::: Lemma 1 -Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i\in \I$. Then $\lim_i X_i$ is also non-empty. +Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i\in \I$. Then $\lim_{i\in \I} X_i$ is also non-empty. ::: _Proof._ @@ -43,7 +43,7 @@ The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Original _Proof._ We use the crude monadicity theorem (see e.g. [SGL92](#references), Thm. IV.4.2). First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism -$$\Hom_{\CompHaus}(X, [0, 1]^S) \cong \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])).$$ +$$\Hom_{\CompHaus}\bigl(X, [0, 1]^S\bigr) \cong \Hom_{\Set}\bigl(S, \Hom_{\CompHaus}(X, [0, 1])\bigr).$$ To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$ by Urysohn's lemma. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then by Urysohn's lemma there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism. @@ -57,7 +57,9 @@ $$\Hom(B, [0,1]) ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \Hom(A, [0, is a coequalizer diagram. We first define $s : \Hom(E,[0,1]) \to \Hom(A,[0,1])$ by choosing a Tietze extension of each continuous function $E \to [0,1]$. Now, for each $\varphi \in \Hom(A,[0,1])$, we can define a continuous function on $\im(f) \cup \im(g) \subseteq B$ to be $\varphi \circ r$ on $\im(f)$, and $s(i^*(\varphi))\circ r$ on $\im(g)$. Note that on the overlap $\im(f)\cap \im(g) = f(E) = g(E)$, the first expression gives $f(e) \mapsto \varphi(e)$, and the second expression gives $g(e) \mapsto s(i^*(\varphi))(e) = \varphi(e)$, so we have indeed given a well-defined function on $\im(f)\cup\im(g)$. Choosing a Tietze extension of this function to a function $B\to [0,1]$ for each $\varphi$, we get a map $t : \Hom(A,[0,1]) \to \Hom(B,[0,1])$. By construction, we have $i^* s = \id$, $f^* t = \id$, and $g^* t = s i^*$, so we have shown that the diagram above is a split coequalizer. $\square$ -This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$. We may view such algebras as being models of the infinitary algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. Indeed, we get the following somewhat stronger result: +This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad +$$S \mapsto \Hom_{\CompHaus}\bigl([0, 1]^S, [0, 1]\bigr).$$ +We may view such algebras as being models of the infinitary algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. Indeed, we get the following somewhat stronger result: ::: Proposition 4 The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally proved in [GU71](#references), 6.5(c)) @@ -70,14 +72,14 @@ By compactness of $X$, we may take finitely many such basic open neighborhoods o To summarize, we have shown that for each $n \in \IN_{>0}$, there exists $i \in \I$ and a finite cover $\{ V_\lambda \mid \lambda \in \Lambda \}$ of $\im(p_i)$ such that whenever $p_i(x), p_i(y) \in V_\lambda$ for some $\lambda$, we have $|\varphi(x) - \varphi(y)| < 1/n$. Now choose such a $i_n$ and associated finite cover of $\im(p_{i_n})$ for each $n$. Then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(j, f_n : j \to i_n)$ of the objects $i_n$. We then see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_j$. This function is continuous, since by construction for any $n\in \IN_{>0}$ and $x \in X$, there is a neighborhood $V$ of $p_j(x)$ such that whenever $p_j(y)\in V$ as well, $|\varphi(y) - \varphi(x)| < 1/n$. By the Tietze extension theorem, this induced function can then be extended to a continuous function $\psi : X_j \to [0,1]$. Then $\varphi = \psi \circ p_j$. This shows the canonical map -$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in \I} X_i, [0,1])$$ +$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom\bigl(\lim_{i\in \I} X_i, [0,1]\bigr)$$ is surjective. Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \IN_{>0}$, consider the set $D_n \coloneqq \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption. Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This implies that $\alpha \circ X_f = \beta \circ X_f$. This shows the canonical map -$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in I} X_i, [0,1])$$ +$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom\bigl(\lim_{i\in I} X_i, [0,1]\bigr)$$ is injective. $\square$ ::: Corollary 5 @@ -86,8 +88,8 @@ The category $\CompHaus$ is locally $\aleph_1$-copresentable. _Proof._ It suffices to show that the monad -$$S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$$ -is $\aleph_1$-accessible. This monad is the composition of +$$S \mapsto \Hom_{\CompHaus}\bigl([0, 1]^S, [0, 1]\bigr)$$ +is $\aleph_1$-accessible. This functor is the composition of $$[0, 1]^{-} : \Set \to \CompHaus^{\op}$$ followed by $$\Hom_{\CompHaus}({-}, [0,1]) : \CompHaus^{\op} \to \Set.$$