From c8f341d17b0c93b9703a05ed85720e585ada162b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 00:15:48 +0200 Subject: [PATCH 1/3] add underlines in linked katex formulas --- src/components/Popup.svelte | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/components/Popup.svelte b/src/components/Popup.svelte index 830dc4b2..80bf6edd 100644 --- a/src/components/Popup.svelte +++ b/src/components/Popup.svelte @@ -89,6 +89,11 @@ an issue when clicking two reasons in a row. So it's a
then. .content { max-width: 800px; margin: 0 auto; + + :global(a:has(.katex)) { + text-decoration: none; + border-bottom: 1px solid var(--outline-color); + } } .popup { From b4f12876a90d947492e700c841d09df945e88e6f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 08:17:31 +0200 Subject: [PATCH 2/3] consistent links to categories in property proofs --- databases/catdat/data/categories/2.yaml | 2 +- databases/catdat/data/categories/Alg(R).yaml | 12 +++---- databases/catdat/data/categories/Ban.yaml | 2 +- databases/catdat/data/categories/CAlg(R).yaml | 8 ++--- databases/catdat/data/categories/CMon.yaml | 2 +- databases/catdat/data/categories/CRing.yaml | 2 +- databases/catdat/data/categories/Cat.yaml | 10 +++--- databases/catdat/data/categories/Delta.yaml | 16 +++++----- databases/catdat/data/categories/FI.yaml | 6 ++-- databases/catdat/data/categories/FS.yaml | 8 ++--- databases/catdat/data/categories/FinAb.yaml | 4 +-- databases/catdat/data/categories/FinGrp.yaml | 6 ++-- databases/catdat/data/categories/FinOrd.yaml | 4 +-- databases/catdat/data/categories/FreeAb.yaml | 6 ++-- databases/catdat/data/categories/Grp.yaml | 2 +- databases/catdat/data/categories/Haus.yaml | 12 +++---- databases/catdat/data/categories/LRS.yaml | 6 ++-- databases/catdat/data/categories/M-Set.yaml | 2 +- databases/catdat/data/categories/Man.yaml | 6 ++-- databases/catdat/data/categories/Meas.yaml | 8 ++--- databases/catdat/data/categories/Met.yaml | 8 ++--- databases/catdat/data/categories/Met_c.yaml | 6 ++-- databases/catdat/data/categories/Met_oo.yaml | 12 +++---- 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 | 8 ++--- .../catdat/data/categories/R-Mod_div.yaml | 2 +- databases/catdat/data/categories/Rel.yaml | 2 +- databases/catdat/data/categories/Ring.yaml | 10 +++--- databases/catdat/data/categories/Rng.yaml | 22 ++++++++----- databases/catdat/data/categories/Sch.yaml | 4 +-- databases/catdat/data/categories/Set_c.yaml | 16 +++++----- databases/catdat/data/categories/Set_f.yaml | 8 ++--- databases/catdat/data/categories/Set_op.yaml | 2 +- .../catdat/data/categories/Set_pointed.yaml | 6 ++-- databases/catdat/data/categories/Setne.yaml | 10 +++--- .../catdat/data/categories/Sh(X,Ab).yaml | 2 +- databases/catdat/data/categories/Sp.yaml | 8 ++--- databases/catdat/data/categories/Top.yaml | 8 ++--- .../catdat/data/categories/Top_pointed.yaml | 22 ++++++------- databases/catdat/data/categories/TorsAb.yaml | 10 +++--- .../catdat/data/categories/TorsFreeAb.yaml | 8 ++--- databases/catdat/data/categories/Vect.yaml | 2 +- databases/catdat/data/categories/Z.yaml | 32 +++++++++---------- databases/catdat/data/categories/sSet.yaml | 2 +- .../categories/walking_coreflexive_pair.yaml | 10 +++--- .../catdat/data/categories/walking_span.yaml | 2 +- .../data/categories/walking_splitting.yaml | 4 +-- .../catdat/data/functors/forget_vector.yaml | 2 +- 50 files changed, 186 insertions(+), 180 deletions(-) diff --git a/databases/catdat/data/categories/2.yaml b/databases/catdat/data/categories/2.yaml index d9d7bbea..45ee532a 100644 --- a/databases/catdat/data/categories/2.yaml +++ b/databases/catdat/data/categories/2.yaml @@ -3,7 +3,7 @@ name: discrete category on two objects notation: $\2$ objects: two objects $0$ and $1$ morphisms: only the two identity morphisms -description: A concrete representation is the full subcategory of $\CRing$ consisting of the two fields $\IF_2$ and $\IF_3$. +description: A concrete representation is the full subcategory of $\CRing$ consisting of the two fields $\IF_2$ and $\IF_3$. nlab_link: null tags: diff --git a/databases/catdat/data/categories/Alg(R).yaml b/databases/catdat/data/categories/Alg(R).yaml index c777a10a..67dd12ba 100644 --- a/databases/catdat/data/categories/Alg(R).yaml +++ b/databases/catdat/data/categories/Alg(R).yaml @@ -25,10 +25,10 @@ satisfied_properties: reason: 'If $f : 0 \to A$ is an algebra homomorphism, then $A$ satisfies $1=f(1)=f(0)=0$, so that $A=0$.' - property_id: Malcev - reason: This follows in the same way as for groups, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + 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_id: disjoint finite products - reason: One can take the same proof as for $\Ring$. + reason: One can take the same proof as for $\Ring$. unsatisfied_properties: - property_id: balanced @@ -44,16 +44,16 @@ 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_id: semi-strongly connected - reason: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected, see its category page for details. + reason: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected. - property_id: 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.' - property_id: 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 := 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.' - property_id: regular quotient object classifier - reason: We may copy the proof for the category of commutative algebras (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). + 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). - property_id: cocartesian cofiltered limits reason: >- @@ -62,7 +62,7 @@ unsatisfied_properties: Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded. - property_id: cofiltered-limit-stable epimorphisms - 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. + 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_id: 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)$.' diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index fbd1bc99..281e2655 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -24,7 +24,7 @@ satisfied_properties: reason: Example 1.48 in Adamek-Rosicky. - property_id: cartesian filtered colimits - reason: If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from the category of metric spaces with non-expansive maps. + reason: If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from $\Met$. - property_id: cocartesian cofiltered limits reason: 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\Ban \to \Vect$ preserves finite coproducts and all limits, and $\Vect$ has the claimed property (see here), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.' diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index 9f267c64..c93c6650 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -26,10 +26,10 @@ satisfied_properties: check_redundancy: false - property_id: Malcev - reason: This follows in the same way as for groups, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + 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_id: coextensive - reason: One can use the same proof as for $\CRing$. + reason: One can use the same proof as for $\CRing$. unsatisfied_properties: - property_id: balanced @@ -54,7 +54,7 @@ unsatisfied_properties: 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.' - property_id: 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.' + 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.' - property_id: cofiltered-limit-stable epimorphisms reason: Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see MSE/2391187. @@ -78,7 +78,7 @@ special_morphisms: 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 homomorphism of algebras which is an epimorphism of commutative rings - reason: The forgetful functor $\CAlg(R) \to \Ring$ is faithful and hence reflects epimorphisms, but it also preserves epimorphisms since it preserves pushouts (since $\CAlg(R) \cong R / \Ring$). For epimorphisms of commutative rings see their detail page. + reason: The forgetful functor $\CAlg(R) \to \CRing$ is faithful and hence reflects epimorphisms, but it also preserves epimorphisms since it preserves pushouts (since $\CAlg(R) \cong R / \CRing$). For epimorphisms of commutative rings see the page for $\CRing$. regular epimorphisms: description: surjective homomorphisms reason: This holds in every finitary algebraic category. diff --git a/databases/catdat/data/categories/CMon.yaml b/databases/catdat/data/categories/CMon.yaml index 48f84f67..465c4877 100644 --- a/databases/catdat/data/categories/CMon.yaml +++ b/databases/catdat/data/categories/CMon.yaml @@ -45,7 +45,7 @@ unsatisfied_properties: 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.' - property_id: regular subobject classifier - reason: We can use exactly the same proof as for the category of monoids. + reason: We can use exactly the same proof as for $\Mon$. - property_id: 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$.' diff --git a/databases/catdat/data/categories/CRing.yaml b/databases/catdat/data/categories/CRing.yaml index ac764981..5a65eb45 100644 --- a/databases/catdat/data/categories/CRing.yaml +++ b/databases/catdat/data/categories/CRing.yaml @@ -29,7 +29,7 @@ satisfied_properties: check_redundancy: false - property_id: Malcev - reason: This follows in the same way as for groups, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + 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_id: 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)$.' diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index 5c7c1379..e6598306 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -28,17 +28,17 @@ satisfied_properties: reason: 'The interval category $\{0 \to 1\}$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $\{0 \to 1\}$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms.' - property_id: infinitary extensive - reason: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' + reason: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' - property_id: semi-strongly connected reason: Every non-empty category is weakly terminal (by using constant functors). unsatisfied_properties: - property_id: balanced - reason: Since we know that the category of monoids is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. + reason: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. - property_id: cogenerating set - reason: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in the category of monoids, which we know does not exist.' + reason: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.' - property_id: skeletal reason: This is trivial. @@ -53,10 +53,10 @@ unsatisfied_properties: reason: 'We can adapt the proof from $\Mon$ as follows: Consider the functor $U : \Cat \to \Set^+$ sending a category $\C$ to the (large) set $\{(x,u) : x \in \Ob(\C) ,\, u \in \End(x) \}$. It is represented by $B \IN$, the one-object category associated to the free monoid in one generator. Consider the relation $R \subseteq U^2$ consisting of those pairs $((x,u),(y,v))$ where $x = y$ and $uv = u^2$. This also representable, namely be the one-object category associated to the monoid with the presentation $\langle u,v : uv = u^2 \rangle$. Clearly, $R$ is reflexive, but not symmetric.' - property_id: coregular - reason: 'We already know that the category of monoids is not coregular, in fact there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' + reason: 'We already know that $\Mon$ is not coregular, in fact there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' - property_id: 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 \Cat$ that maps a set to its discrete category. + 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 \Cat$ that maps a set to its discrete category. - property_id: effective cocongruences reason: >- diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index 9f2435ac..79d0306e 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/databases/catdat/data/categories/Delta.yaml @@ -31,10 +31,10 @@ satisfied_properties: reason: For all $n,m$ there are morphisms $[n] \to [0] \to [m]$. - property_id: cogenerator - reason: The ordered set $[1] = \{0 < 1\}$ is a cogenerator, even for the category of posets, see there for a proof. + reason: The ordered set $[1] = \{0 < 1\}$ is a cogenerator, even for $\Pos$. - property_id: coequalizers - reason: Assume that $X \rightrightarrows Y$ are morphisms in $\FinOrd \setminus \{\varnothing\}$. Since $\FinOrd$ has coequalizers, we have a coequalizer $Y \to Q$. Since $Y$ is non-empty, $Q$ is non-empty as well, and clearly $Y \to Q$ is then also the coequalizer in $\FinOrd \setminus \{\varnothing\}$. + reason: Assume that $X \rightrightarrows Y$ are morphisms in $\FinOrd \setminus \{\varnothing\}$. Since $\FinOrd$ has coequalizers, we have a coequalizer $Y \to Q$. Since $Y$ is non-empty, $Q$ is non-empty as well, and clearly $Y \to Q$ is then also the coequalizer in $\FinOrd \setminus \{\varnothing\}$. - property_id: generator reason: The ordered set $[0] = \{0\}$ is a generator. @@ -43,13 +43,13 @@ satisfied_properties: reason: 'If $f : [n] \to [m]$ is an isomorphism, then $n + 1 = m + 1$ by comparing the cardinalities, hence $n = m$.' - property_id: core-thin - reason: The category $\FinOrd \setminus \{\varnothing\}$ is core-thin because already $\FinOrd$ is core-thin (see its category page). + reason: The category $\FinOrd \setminus \{\varnothing\}$ is core-thin because already $\FinOrd$ is core-thin. - property_id: mono-regular - reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. - property_id: epi-regular - reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. - property_id: cosifted reason: >- @@ -70,10 +70,10 @@ unsatisfied_properties: reason: 'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ have a common left inverse, the unique map $s^0 : [1] \to [0]$, but are not equalized by any morphism.' - property_id: sequential colimits - reason: We can just copy the proof for $\FinOrd$ to show that the sequence of inclusions $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has no colimit. + reason: We can just copy the proof for $\FinOrd$ to show that the sequence of inclusions $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has no colimit. - property_id: sequential limits - reason: We can just copy the proof for $\FinOrd$ to show that the sequence of truncations $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has no limit. + reason: We can just copy the proof for $\FinOrd$ to show that the sequence of truncations $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has no limit. - property_id: pushouts reason: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. @@ -89,7 +89,7 @@ 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 order-preserving maps - reason: We can use the same proof as for $\FinOrd$ since this has merely used the non-empty ordered set $\{0 < 1\}$. + reason: We can use the same proof as for $\FinOrd$ since this has merely used the non-empty ordered set $\{0 < 1\}$. regular monomorphisms: description: same as monomorphisms reason: This is because the category is mono-regular. diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index f029b94d..343cb938 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/databases/catdat/data/categories/FI.yaml @@ -29,10 +29,10 @@ satisfied_properties: reason: The one-point set is a generator since it represents the forgetful functor $\FI \to \Set$. - property_id: equalizers - reason: We construct equalizers just like in $\FinSet$ and observe that the universal property still holds. + reason: We construct equalizers just like in $\FinSet$ and observe that the universal property still holds. - property_id: wide pullbacks - reason: 'We construct wide pullbacks just like in $\Set$, i.e., for a w.l.o.g. non-empty family of injective maps $f_i : X_i \to S$ we consider the subset $P \subseteq \prod_{i \in I} X_i$ of those tuples $x$ where $f_i(x_i) = f_j(x_j)$. Each projection $P \to X_i$ is injective, so in particular $P$ is finite, and $P \to X_i$ becomes a morphism in $\FI$. It is easy to check that the universal property still holds in $\FI$.' + reason: 'We construct wide pullbacks just like in $\Set$, i.e., for a w.l.o.g. non-empty family of injective maps $f_i : X_i \to S$ we consider the subset $P \subseteq \prod_{i \in I} X_i$ of those tuples $x$ where $f_i(x_i) = f_j(x_j)$. Each projection $P \to X_i$ is injective, so in particular $P$ is finite, and $P \to X_i$ becomes a morphism in $\FI$. It is easy to check that the universal property still holds in $\FI$.' - property_id: mono-regular reason: 'If $f : X \to Y$ is an injective map of finite sets, it is the equalizer of the two injective maps $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$, and $Y \sqcup_X Y$ is finite.' @@ -60,7 +60,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: core-thin - reason: Its core is the category of finite sets and bijections, which we know is not thin. + reason: Its core is $\IB$, which we know is not thin. - property_id: strongly connected reason: There is no map from a non-empty set to the empty set. diff --git a/databases/catdat/data/categories/FS.yaml b/databases/catdat/data/categories/FS.yaml index 408ace2d..442d61b1 100644 --- a/databases/catdat/data/categories/FS.yaml +++ b/databases/catdat/data/categories/FS.yaml @@ -29,13 +29,13 @@ satisfied_properties: reason: 'We prove that $\{0,1\}$ is a cogenerator: The surjective maps $X \to \{0,1\}$ correspond to the non-empty proper subsets of $X$. If $a,b \in X$ are elements that have the same image under each surjective map $X \to \{0,1\}$, it therefore means that they lie in the same non-empty proper subsets of $X$. This implies $a=b$: If $X = \{a\}$, this is trivial. Otherwise, use the subset $\{a\}$.' - property_id: wide pushouts - reason: 'We construct wide pushouts as in $\Set$ and observe that the universal property still holds when we restrict to surjective maps. If $f_i : S \to X_i$ are surjective maps and $P$ is their wide pushout, then each $X_i \to P$ is surjective, so that in particular $P$ is finite.' + reason: 'We construct wide pushouts as in $\Set$ and observe that the universal property still holds when we restrict to surjective maps. If $f_i : S \to X_i$ are surjective maps and $P$ is their wide pushout, then each $X_i \to P$ is surjective, so that in particular $P$ is finite.' - property_id: coequalizers - reason: We construct coequalizers as in $\FinSet$ (or $\Set$) and observe that the universal property still holds when we restrict to surjective maps. + reason: We construct coequalizers as in $\FinSet$ (or $\Set$) and observe that the universal property still holds when we restrict to surjective maps. - property_id: epi-regular - reason: 'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\FinSet$, but also in $\FS$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\FS$, we can use this finite set here.' + reason: 'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\FinSet$, but also in $\FS$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\FS$, we can use this finite set here.' - property_id: multi-terminal object reason: The empty set and a singleton give a multi-terminal object. @@ -60,7 +60,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: core-thin - reason: Its core is the category of finite sets and bijections, which we know is not thin. + reason: Its core is $\IB$, which we know is not thin. - property_id: 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$. diff --git a/databases/catdat/data/categories/FinAb.yaml b/databases/catdat/data/categories/FinAb.yaml index 179f1a09..80ea9028 100644 --- a/databases/catdat/data/categories/FinAb.yaml +++ b/databases/catdat/data/categories/FinAb.yaml @@ -23,13 +23,13 @@ satisfied_properties: reason: The underlying set of a finite structure can be chosen to be a subset of $\IN$. - property_id: abelian - reason: This follows from the fact for abelian groups. + reason: This follows from the fact for $\Ab$. - property_id: self-dual reason: 'This is a simple special case of Pontryagin duality: The functor $\Hom(-,\IQ/\IZ)$ provides the equivalence.' - property_id: ℵ₁-accessible - reason: The proof works exactly as for the category of finite sets. + reason: The proof works exactly as for $\FinSet$. unsatisfied_properties: - property_id: small diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index 7d9ea887..6d8be428 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/databases/catdat/data/categories/FinGrp.yaml @@ -40,10 +40,10 @@ satisfied_properties: reason: Since epimorphisms are surjective (see below), this is the first isomorphism theorem for finite groups. - property_id: ℵ₁-accessible - reason: The proof works exactly as for the category of finite sets. + reason: The proof works exactly as for $\FinSet$. - property_id: effective congruences - reason: 'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\Grp$ has effective congruences since it is algebraic. Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\FinGrp$ as well.' + reason: 'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\Grp$ has effective congruences since it is algebraic. Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\FinGrp$ as well.' unsatisfied_properties: - property_id: normal @@ -81,7 +81,7 @@ special_objects: special_morphisms: isomorphisms: description: bijective homomorphisms - reason: This follows exactly as for groups. + reason: This follows exactly as for $\Grp$. monomorphisms: description: injective homomorphisms reason: 'Let $f : A \to B$ be a monomorphism of finite groups. Let $a \in A$ be in the kernel of $a$, say of order $n$. Then we may view $a$ as a morphism $a : C_n \to A$ with $f \circ a = 1$ (the trivial homomorphism), and $C_n$ is finite. Hence, $a = 1$.' diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index fba6dc72..a0b9e21c 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/databases/catdat/data/categories/FinOrd.yaml @@ -26,7 +26,7 @@ satisfied_properties: reason: Take the singleton set with the unique ordering. - property_id: cogenerator - reason: The ordered set $\{0 < 1\}$ is a cogenerator, even for the category of posets, see there for a proof. + reason: The ordered set $\{0 < 1\}$ is a cogenerator, even for $\Pos$. - property_id: strict initial object reason: The empty ordered set is initial and is clearly strict. @@ -91,7 +91,7 @@ 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 order-preserving maps - reason: 'The proof is similar to the one for $\Set$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphisms $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^*(A) = f^*(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^*(A) \setminus f^*(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.' + reason: 'The proof is similar to the one for $\Set$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphisms $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^*(A) = f^*(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^*(A) \setminus f^*(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.' regular monomorphisms: description: same as monomorphisms reason: This is because the category is mono-regular. diff --git a/databases/catdat/data/categories/FreeAb.yaml b/databases/catdat/data/categories/FreeAb.yaml index 1ebfacff..1087b637 100644 --- a/databases/catdat/data/categories/FreeAb.yaml +++ b/databases/catdat/data/categories/FreeAb.yaml @@ -18,7 +18,7 @@ satisfied_properties: reason: There is a forgetful functor $\FreeAb \to \Set$ and $\Set$ is locally small. - property_id: additive - reason: This follows easily from the fact for abelian groups. + reason: The embedding $\FreeAb \hookrightarrow \Ab$ is closed under (finite) direct sums, and $\Ab$ is additive. - property_id: coproducts reason: This is is because free abelian groups are closed under direct sums of abelian groups. @@ -30,14 +30,14 @@ satisfied_properties: reason: See MSE/5025660. - property_id: generator - reason: As for $\Ab$, the group $\IZ$ is a generator. + reason: As for $\Ab$, the group $\IZ$ is a generator. - property_id: cogenerator reason: It is easy to check that $\IZ$ is a cogenerator for free abelian groups. - property_id: regular reason: |- - This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup, hence free, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms. + This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup, hence free, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms. (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian, $f$ is also an coequalizer in $\FreeAb$. (2) If $f : A \to B$ is a regular epimorphism in $\FreeAb$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective. diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index ad78e13e..42c9696e 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -73,7 +73,7 @@ unsatisfied_properties: reason: The canonical homomorphism $\coprod_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is not surjective because its domain is countable and its codomain is uncountable. Hence it is no epimorphism. - property_id: cofiltered-limit-stable epimorphisms - reason: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. + reason: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. special_objects: initial object: diff --git a/databases/catdat/data/categories/Haus.yaml b/databases/catdat/data/categories/Haus.yaml index 1c8c7e7c..7045a1fc 100644 --- a/databases/catdat/data/categories/Haus.yaml +++ b/databases/catdat/data/categories/Haus.yaml @@ -15,20 +15,20 @@ related_categories: satisfied_properties: - property_id: locally small - reason: It is a full subcategory of $\Top$, which is locally small. + reason: It is a full subcategory of $\Top$, which is locally small. - property_id: equalizers - reason: This follows from the corresponding fact for $\Top$ since subspaces of Hausdorff spaces are again Hausdorff. + reason: This follows from the corresponding fact for $\Top$ since subspaces of Hausdorff spaces are again Hausdorff. - property_id: products - reason: This follows from the corresponding fact for $\Top$ since products of Hausdorff spaces are again Hausdorff. + reason: This follows from the corresponding fact for $\Top$ since products of Hausdorff spaces are again Hausdorff. - property_id: cocomplete - reason: This follows since $\Haus$ is a reflective subcategory of $\Top$, which is cocomplete. For the reflector, see e.g. the nLab. Explicitly, we construct the colimit of Hausdorff spaces by applying the reflector to the colimit of the underlying topological spaces. + reason: This follows since $\Haus$ is a reflective subcategory of $\Top$, which is cocomplete. For the reflector, see e.g. the nLab. Explicitly, we construct the colimit of Hausdorff spaces by applying the reflector to the colimit of the underlying topological spaces. check_redundancy: false - property_id: infinitary extensive - reason: This follows exactly as for $\Top$ since Hausdorff spaces are closed under taking subspaces and coproducts in $\Top$. + reason: This follows exactly as for $\Top$ since Hausdorff spaces are closed under taking subspaces and coproducts in $\Top$. - property_id: well-powered reason: This is clear from the classification of monomorphisms as injective continuous maps. @@ -62,7 +62,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff). + reason: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff). - property_id: regular subobject classifier reason: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$). diff --git a/databases/catdat/data/categories/LRS.yaml b/databases/catdat/data/categories/LRS.yaml index 47c6ce44..4ab414ce 100644 --- a/databases/catdat/data/categories/LRS.yaml +++ b/databases/catdat/data/categories/LRS.yaml @@ -29,7 +29,7 @@ satisfied_properties: 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_id: 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 =: 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_id: balanced @@ -39,10 +39,10 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: This is because the category of schemes already is not Malcev. + reason: This is because already $\Sch$ is not Malcev. - property_id: semi-strongly connected - reason: This is because already the full subcategory of affine schemes is not semi-strongly connected, see the entry for $\CRing$. Specifically, there is no morphism between $\Spec(\IF_2)$ and $\Spec(\IF_3)$. + reason: This is because already the full subcategory $\Sch$ of schemes is not semi-strongly connected. - property_id: co-Malcev reason: 'We can adjust the proof for $\Top$ (see MO/509548) as follows: Let $k$ be a field, $X$ be a singleton and $Y = \{u,v\}$ be the Sierpinski space where $\{u\}$ is open, but $\{v\}$ is not. Endow both with the sheaf of locally constant functions to $k$. Thus, $\O_X(X) = k$, $\O_Y(Y) = \O_Y(\{u\}) = k$. There is a canonical morphism $p : X + X \to Y$. It is a coreflexive corelation that is not cosymmetric.' diff --git a/databases/catdat/data/categories/M-Set.yaml b/databases/catdat/data/categories/M-Set.yaml index 9383b3dd..a3fb57ce 100644 --- a/databases/catdat/data/categories/M-Set.yaml +++ b/databases/catdat/data/categories/M-Set.yaml @@ -3,7 +3,7 @@ name: category of M-sets notation: $M{-}\Set$ objects: sets with a left action of a monoid $M$ morphisms: maps that are compatible with the $M$-action, meaning $f(m \cdot x)=m \cdot f(x)$, also called $M$-maps -description: Here, $M$ can be any monoid. But the most important special case is that of a group. To settle (future) non-properties, we assume that $M$ is non-trivial, since otherwise we just get the category of sets. +description: Here, $M$ can be any monoid. But the most important special case is that of a group. To settle (future) non-properties, we assume that $M$ is non-trivial, since otherwise we just get the category $\Set$. nlab_link: https://ncatlab.org/nlab/show/MSet tags: diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index f4ca2c8b..1417f7dc 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -29,11 +29,11 @@ satisfied_properties: reason: 'The manifold $\IR$ is a cogenerator, since for every smooth manifold $M$ and points $p \neq q$ in $M$ there is a smooth function $f : M \to \IR$ with $f(p) = 1$ and $f(q) = 0$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25).' - property_id: extensive - reason: '[Sketch] Since $\Top$ is infinitary extensive, a continuous map $f : M \to \coprod_i N_i$ corresponds to a decomposition $M = \coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \to N_i$. Endow the open subset $M_i \subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth.' + reason: '[Sketch] Since $\Top$ is infinitary extensive, a continuous map $f : M \to \coprod_i N_i$ corresponds to a decomposition $M = \coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \to N_i$. Endow the open subset $M_i \subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth.' - property_id: countably distributive # TODO: maybe add "countably extensive" to make this more conceptual - reason: To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\Top$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth. + reason: To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\Top$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth. - property_id: Cauchy complete reason: See Theorem 2.1 at the nLab. @@ -72,7 +72,7 @@ unsatisfied_properties: reason: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction. - property_id: ℵ₁-accessible - reason: 'We already know that the category of countable sets $\Set_\c$ does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.' + reason: 'We already know that $\Set_\c$ does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.' - property_id: quotients of congruences reason: If $\Man$ had quotients of congruences, then by this lemma, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$. This contradicts MO/19916. diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index b33faba5..aadf0083 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -32,7 +32,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_id: 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 =: 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_id: generator reason: The one-point measurable space (with the unique $\sigma$-algebra) is a generator since it represents the forgetful functor $\Meas \to \Set$. @@ -60,10 +60,10 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: Use that $\Set$ is not Malcev and endow sets with the trivial $\sigma$-algebra. + reason: Use that $\Set$ is not Malcev and endow sets with the trivial $\sigma$-algebra. - property_id: 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 \Meas$ which equips a set with the trivial $\sigma$-algebra. + 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 \Meas$ which equips a set with the trivial $\sigma$-algebra. - property_id: effective cocongruences reason: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' @@ -90,4 +90,4 @@ special_morphisms: reason: Use the same proof as for sets, where $2 = \{0,1\}$ is endowed with the trivial $\sigma$-algebra. regular monomorphisms: description: embeddings - reason: '(This is the same proof as for $\Top$.) Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the trivial $\sigma$-algebra.' + reason: '(This is the same proof as for $\Top$.) Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the trivial $\sigma$-algebra.' diff --git a/databases/catdat/data/categories/Met.yaml b/databases/catdat/data/categories/Met.yaml index 72631f2d..ab6afd75 100644 --- a/databases/catdat/data/categories/Met.yaml +++ b/databases/catdat/data/categories/Met.yaml @@ -34,10 +34,10 @@ satisfied_properties: check_redundancy: false - property_id: coequalizers - reason: This is because the category of pseudo-metric spaces has coequalizers and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the coequalizer in the category of pseudo-metric spaces and then identify points with distance zero. + reason: This is because the category of pseudo-metric spaces $\PMet$ has coequalizers and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the coequalizer in the category of pseudo-metric spaces and then identify points with distance zero. - property_id: filtered colimits - reason: This is because the category of pseudo-metric spaces has filtered colimits and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the filtered colimit in the category of pseudo-metric spaces and then identify points with distance zero. + reason: This is because the category of pseudo-metric spaces $\PMet$ has filtered colimits and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the filtered colimit in the category of pseudo-metric spaces and then identify points with distance zero. check_redundancy: false - property_id: cartesian filtered colimits @@ -66,7 +66,7 @@ unsatisfied_properties: reason: 'Assume that the power $P = \IR^{\IN}$ exists, where $\IR$ has the usual metric. Since the forgetful functor $\Met \to \Set$ is representable, it preserves limits, powers in particular. Thus, we may assume that $P$ is the set of sequences of numbers and that the projections $p_n : P \to \IR$ are given by $p_n(x) = x_n$. Now consider the sequences $x = (n)_n$ and $y = (0)_n$. Since each $p_n$ is non-expansive, we get $d(x,y) \geq d(p_n(x),p_n(y)) = d(n,0) = n$. But then $d(x,y) = \infty$, a contradiction.' - property_id: binary copowers - reason: The coproduct of two non-empty metric spaces does not exist, see MSE/1778408. For example, the copower $\IR \sqcup \IR$ does not exist. We only get coproducts when allowing $\infty$ as a distance, as in $\Met_{\infty}$. + reason: The coproduct of two non-empty metric spaces does not exist, see MSE/1778408. For example, the copower $\IR \sqcup \IR$ does not exist. We only get coproducts when allowing $\infty$ as a distance, as in $\Met_{\infty}$. - property_id: strict terminal object reason: This is trivial. @@ -81,7 +81,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: filtered-colimit-stable monomorphisms - reason: 'The following example is taken from Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_0 \to X_n$, $x \mapsto x$ is the non-injective map $X_0 \to \{0\}$.' + reason: 'The following example is taken from Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_0 \to X_n$, $x \mapsto x$ is the non-injective map $X_0 \to \{0\}$.' - property_id: skeletal reason: This is trivial. diff --git a/databases/catdat/data/categories/Met_c.yaml b/databases/catdat/data/categories/Met_c.yaml index c3936636..dd24511b 100644 --- a/databases/catdat/data/categories/Met_c.yaml +++ b/databases/catdat/data/categories/Met_c.yaml @@ -30,7 +30,7 @@ satisfied_properties: check_redundancy: false - property_id: infinitary extensive - reason: This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive. + reason: This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive. - property_id: well-powered reason: This follows easily from the fact that monomorphisms are injective in this category. @@ -39,7 +39,7 @@ satisfied_properties: reason: The one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$. - property_id: cogenerator - reason: The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator. + reason: The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator. - property_id: well-copowered reason: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' @@ -64,7 +64,7 @@ unsatisfied_properties: reason: 'Consider the metric subspace $\{(a,b) \in \IR^2 : a \leq b\}$ of $\IR^2$.' - property_id: regular subobject classifier - reason: 'We recycle the proof from the category of Hausdorff spaces: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' + reason: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' - property_id: sequential colimits reason: See MO/510316. diff --git a/databases/catdat/data/categories/Met_oo.yaml b/databases/catdat/data/categories/Met_oo.yaml index 14edc2c9..5f6c2eab 100644 --- a/databases/catdat/data/categories/Met_oo.yaml +++ b/databases/catdat/data/categories/Met_oo.yaml @@ -21,16 +21,16 @@ satisfied_properties: reason: The singleton metric space $1$ is a generator, since morphisms $1 \to X$ correspond to the elements of $X$. - property_id: locally ℵ₁-presentable - reason: Example 4.5 in this preprint + reason: This is Example 4.5 in Metric abstract elementary classes as accessible categories. - property_id: cartesian filtered colimits - reason: We can use the same proof as for the category of metric spaces 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\}$. + 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_id: 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 =: 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.' - property_id: cogenerator - reason: 'The proof is similar to $\Met$, a cogenerator is given by $\IR \cup \{\infty\}$ with the metric in which $d(a,\infty)=\infty$ for $a \in \IR$. Then one checks that the maps $d(a,-) : X \to \IR \cup \{\infty\}$ are non-expansive and finishes as for $\Met$.' + reason: 'The proof is similar to $\Met$, a cogenerator is given by $\IR \cup \{\infty\}$ with the metric in which $d(a,\infty)=\infty$ for $a \in \IR$. Then one checks that the maps $d(a,-) : X \to \IR \cup \{\infty\}$ are non-expansive and finishes as for $\Met$.' - property_id: semi-strongly connected reason: Every non-empty metric space is weakly terminal (by using constant maps). @@ -43,7 +43,7 @@ unsatisfied_properties: reason: This is proven in MSE/5131457. - property_id: filtered-colimit-stable monomorphisms - reason: We can copy the proof from the category of metric spaces. + reason: We can copy the proof from $\Met$. - property_id: skeletal reason: This is trivial. @@ -55,7 +55,7 @@ unsatisfied_properties: 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.' - property_id: 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 \Met_{\infty}$ that equips a set with the discrete topology. + 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 \Met_{\infty}$ that equips a set with the discrete topology. - property_id: effective cocongruences reason: The same counterexample as for $\Met$ works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$. diff --git a/databases/catdat/data/categories/Mon.yaml b/databases/catdat/data/categories/Mon.yaml index e0d3f623..988a3555 100644 --- a/databases/catdat/data/categories/Mon.yaml +++ b/databases/catdat/data/categories/Mon.yaml @@ -56,13 +56,13 @@ unsatisfied_properties: 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$.' - property_id: regular quotient object classifier - reason: We can just copy the proof for the category of commutative monoids. Alternatively, we may use this lemma (dualized). + reason: We can just copy the proof for $\CMon$. Alternatively, we may use this lemma (dualized). - property_id: cofiltered-limit-stable epimorphisms - reason: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. + reason: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. - property_id: cocartesian cofiltered limits - reason: 'We know that the category of groups fails to satisfy this property. The same counterexample works here since the inclusion $\Grp \hookrightarrow \Mon$ preserves limits and colimits (it has a left and a right adjoint) and is conservative. A similar counterexample is given by the free monoids $N_n = \langle x_1,\dotsc,x_n \rangle$ and the Boolean monoid $M = \langle e : e^2=e \rangle$ with the maps $N_{n+1} \to N_n$, $x_{n+1} \mapsto 1$. Then the element $(x_1 e \cdots x_n e) \in \lim_n (M \sqcup N_n)$ does not come from $M \sqcup \lim_n N_n$ because its components have unbounded free product length.' + reason: 'We know that $\Grp$ fails to satisfy this property. The same counterexample works here since the inclusion $\Grp \hookrightarrow \Mon$ preserves limits and colimits (it has a left and a right adjoint) and is conservative. A similar counterexample is given by the free monoids $N_n = \langle x_1,\dotsc,x_n \rangle$ and the Boolean monoid $M = \langle e : e^2=e \rangle$ with the maps $N_{n+1} \to N_n$, $x_{n+1} \mapsto 1$. Then the element $(x_1 e \cdots x_n e) \in \lim_n (M \sqcup N_n)$ does not come from $M \sqcup \lim_n N_n$ because its components have unbounded free product length.' - property_id: CSP 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. diff --git a/databases/catdat/data/categories/PMet.yaml b/databases/catdat/data/categories/PMet.yaml index 72a570f8..2b82bc3a 100644 --- a/databases/catdat/data/categories/PMet.yaml +++ b/databases/catdat/data/categories/PMet.yaml @@ -36,7 +36,7 @@ satisfied_properties: check_redundancy: false - property_id: exact filtered colimits - reason: 'We already saw that finite limits and filtered colimits exist. Now let $\I$ be a finite category and $\J$ be a small filtered category, w.l.o.g. a directed poset. Let $X : \I \times \J \to \PMet$ be a diagram. We need to show that the canonical map $\colim_{j \in \J} \lim_{i \in \I} X(i,j) \to \lim_{i \in \I} \colim_{j \in \J} X(i,j)$ is an isomorphism. It is bijective since the forgetful functor to $\Set$ preserves finite limits and filtered colimits and since $\Set$ has exact filtered colimits. That the map is isometric can easily be reduced to the following lemma: If $d_{i,j} \in \IR_{\geq 0}$ are numbers for $i \in \I$, $j \in \J$ with $j \leq k \implies d_{i,k} \leq d_{i,j}$, then $\inf_j \sup_i d_{i,j} = \sup_i \inf_j d_{i,j}$. This can be proven directly. Alternatively, use that the thin category $(\IR_{\geq 0} \cup \{\infty\},\leq)$ is isomorphic to $([0,1],\leq)$, and we already know that it has exact filtered colimits.' + reason: 'We already saw that finite limits and filtered colimits exist. Now let $\I$ be a finite category and $\J$ be a small filtered category, w.l.o.g. a directed poset. Let $X : \I \times \J \to \PMet$ be a diagram. We need to show that the canonical map $\colim_{j \in \J} \lim_{i \in \I} X(i,j) \to \lim_{i \in \I} \colim_{j \in \J} X(i,j)$ is an isomorphism. It is bijective since the forgetful functor to $\Set$ preserves finite limits and filtered colimits and since $\Set$ has exact filtered colimits. That the map is isometric can easily be reduced to the following lemma: If $d_{i,j} \in \IR_{\geq 0}$ are numbers for $i \in \I$, $j \in \J$ with $j \leq k \implies d_{i,k} \leq d_{i,j}$, then $\inf_j \sup_i d_{i,j} = \sup_i \inf_j d_{i,j}$. This can be proven directly. Alternatively, use that the thin category $(\IR_{\geq 0} \cup \{\infty\},\leq)$ is isomorphic to $([0,1],\leq)$, and we already know that it has exact filtered colimits.' - property_id: strict initial object reason: The empty (pseudo-)metric space is initial and clearly strict. @@ -79,7 +79,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: Take any counterexample in $\Set$ and equip it with the zero pseudo-metric. + reason: Take any counterexample in $\Set$ and equip it with the zero pseudo-metric. - property_id: natural numbers object reason: >- diff --git a/databases/catdat/data/categories/Pos.yaml b/databases/catdat/data/categories/Pos.yaml index 4e24fdc0..3c855700 100644 --- a/databases/catdat/data/categories/Pos.yaml +++ b/databases/catdat/data/categories/Pos.yaml @@ -30,7 +30,7 @@ satisfied_properties: reason: 'We prove that the poset $\{0 < 1\}$ is a cogenerator: Let $P$ be a poset and $a,b \in P$ be two elements such that $f(a) = f(b)$ for all order-preserving maps $f : P \to \{0 < 1 \}$. This means that $a$ and $b$ lie in the same upper sets. In particular, $b$ lies in the upper set generated by $a$, meaning $a \leq b$, and similarly we deduce $b \leq a$. Thus, $a = b$.' - property_id: infinitary extensive - reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.' + reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.' - property_id: semi-strongly connected reason: Every non-empty poset is weakly terminal (by using constant maps). @@ -81,7 +81,7 @@ special_morphisms: reason: This is easy. monomorphisms: description: injective order-preserving functions - reason: The same proof as for $\Set$ can be used. + reason: The same proof as for $\Set$ can be used. epimorphisms: description: surjective order-preserving functions 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.' diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index a54b64eb..6672afb3 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -17,7 +17,7 @@ satisfied_properties: reason: There is a forgetful functor $\Pos \to \Set$ and $\Set$ is locally small. - property_id: locally finitely presentable - reason: The same proof as for $\Pos$ works, cf. Adamek-Rosicky, Example 1.10. + reason: The same proof as for $\Pos$ works, cf. Adamek-Rosicky, Example 1.10. - property_id: generator reason: The singleton proset $1$ is a generator, since morphisms $1 \to P$ correspond to the elements of $P$. @@ -29,7 +29,7 @@ satisfied_properties: reason: Endow the set $\{ 0,1 \}$ with the preorder $0 \leq 1$, $1 \leq 0$ (which is not a partial order). Then every map $P \to \{0,1\}$ is order-preserving. Now the claim follows since the set $\{ 0,1 \}$ is a cogenerator in $\Set$. - property_id: infinitary extensive - reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as prosets, and each $f_i$ is order-preserving.' + reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as prosets, and each $f_i$ is order-preserving.' - property_id: semi-strongly connected reason: Every non-empty proset is weakly terminal (by using constant maps). @@ -57,7 +57,7 @@ unsatisfied_properties: 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.' - property_id: 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. + 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_id: 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.' @@ -78,7 +78,7 @@ special_morphisms: reason: This is easy. monomorphisms: description: injective order-preserving functions - reason: The same proof as for $\Set$ can be used. + reason: The same proof as for $\Set$ can be used. epimorphisms: description: surjective order-preserving functions 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. diff --git a/databases/catdat/data/categories/R-Mod_div.yaml b/databases/catdat/data/categories/R-Mod_div.yaml index 66dc6c40..4854507b 100644 --- a/databases/catdat/data/categories/R-Mod_div.yaml +++ b/databases/catdat/data/categories/R-Mod_div.yaml @@ -18,7 +18,7 @@ satisfied_properties: reason: There is a forgetful functor $R{-}\Mod \to \Set$ and $\Set$ is locally small. - property_id: split abelian - reason: It is a standard fact that the category of $R$-modules is abelian for any ring $R$. If $R$ is a division ring, then by linear algebra every $R$-module has a basis, hence is projective, so that every short exact sequence splits. + reason: It is a standard fact that the category of $R$-modules is abelian for any ring $R$, see Mac Lane, Ch. VIII. If $R$ is a division ring, then by linear algebra every $R$-module has a basis, hence is projective, so that every short exact sequence splits. - property_id: finitary algebraic reason: Take the algebraic theory of an $R$-module (given by the algebraic theory of an abelian group and for each $r \in R$ a unary operation). diff --git a/databases/catdat/data/categories/Rel.yaml b/databases/catdat/data/categories/Rel.yaml index a54bf6a7..1c5f8a80 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_id: 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^o \subseteq Y \times X$ defined by $R^o := \{(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} := \{(y,x) : (x,y) \in R \}$.' - property_id: 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 859378ad..4f58698a 100644 --- a/databases/catdat/data/categories/Ring.yaml +++ b/databases/catdat/data/categories/Ring.yaml @@ -15,7 +15,7 @@ related_categories: - Rng comments: - - It is likely that the epimorphisms can be described as in the commutative case. + - It is likely that the epimorphisms can be described as for $\CRing$. satisfied_properties: - property_id: locally small @@ -28,7 +28,7 @@ satisfied_properties: reason: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.' - property_id: Malcev - reason: This follows in the same way as for groups, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + 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_id: disjoint finite products reason: 'To show that $A \sqcup_{A \times B} B$ is trivial, let $R$ be a ring which admits homomorphisms $f : A \to R$, $g : B \to R$ with $f(p_1(a,b))=g(p_2(a,b))$ for all $(a,b) \in A \times B$, i.e. $f(a)=g(b)$. Applying this to $a=0$, $b=1$ yields $1=0$ in $R$.' @@ -47,7 +47,7 @@ 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_id: semi-strongly connected - reason: There is no homomorphism between $\IF_2$ and $\IF_3$. + reason: This is because already the full subcategory $\CRing$ does not have this property. - property_id: 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.' @@ -56,7 +56,7 @@ unsatisfied_properties: 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.' - property_id: regular quotient object classifier - reason: We may copy the proof for the category of commutative rings (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). + 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). - property_id: cocartesian cofiltered limits reason: >- @@ -65,7 +65,7 @@ unsatisfied_properties: Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded. - property_id: cofiltered-limit-stable epimorphisms - reason: We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488. + reason: We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488. - property_id: effective cocongruences reason: See MO/510744. diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index 9ad84066..31c7f895 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -14,7 +14,7 @@ related_categories: - Ring comments: - - It is likely that the epimorphisms can be described as in the commutative, unital case. + - It is likely that the epimorphisms can be described as for $\CRing$. satisfied_properties: - property_id: locally small @@ -27,7 +27,7 @@ satisfied_properties: reason: The zero ring is a zero object. - property_id: Malcev - reason: This follows in the same way as for groups, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + reason: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. unsatisfied_properties: - property_id: balanced @@ -40,20 +40,26 @@ unsatisfied_properties: reason: This is trivial. - property_id: counital - reason: If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$ is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative. + reason: >- + If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism + $$\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$$ + is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative. - property_id: CIP # TODO: remove code duplication with "counital" proof - reason: If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$ is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative. + reason: >- + If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism + $$\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$$ + is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative. - property_id: regular subobject classifier reason: 'Assume that $\Rng$ has a subobject classifier $\Omega$. Since $0$ is a zero object, every regular subobject $R \subseteq S$ would be the kernel of some homomorphism $S \to \Omega$. In particular, it would be an ideal. Now take any pair of homomorphisms $f,g : S \rightrightarrows T$ in $\Ring$. Their equalizer $R \subseteq S$ is also the equalizer in $\Rng$, and it contains $1 \in S$. If it was an ideal, then $R = S$, and hence $f = g$, which is absurd.' - property_id: coregular - reason: 'We can copy the proof for the category of rings. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.' + reason: 'We can copy the proof for $\Ring$. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.' - property_id: regular quotient object classifier - reason: 'Assume that $\Rng$ has a regular quotient object classifier $P$. Consider the functor $N : \Ab \to \Rng$ that equips an abelian group with zero multiplication. It is fully faithful and has a left adjoint mapping a rng $R$ to the abelian group $R/R^2$. If $R$ is a rng with zero multiplication and $R \to S$ is a surjective homomorphism, then $S$ has zero multiplication. Therefore, the assumptions of this lemma (dualized) apply and we conclude that $P/P^2$ is a regular quotient object classifier of $\Ab$. But we already know that this category has no such object (in fact, the only additive categories with such an object are trivial by MSE/4086192).' + reason: 'Assume that $\Rng$ has a regular quotient object classifier $P$. Consider the functor $N : \Ab \to \Rng$ that equips an abelian group with zero multiplication. It is fully faithful and has a left adjoint mapping a rng $R$ to the abelian group $R/R^2$. If $R$ is a rng with zero multiplication and $R \to S$ is a surjective homomorphism, then $S$ has zero multiplication. Therefore, the assumptions of this lemma (dualized) apply and we conclude that $P/P^2$ is a regular quotient object classifier of $\Ab$. But we already know that $\Ab$ has no such object (in fact, the only additive categories with such an object are trivial by MSE/4086192).' - property_id: cocartesian cofiltered limits reason: >- @@ -65,7 +71,7 @@ unsatisfied_properties: reason: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by SP/04W0. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction. - property_id: cofiltered-limit-stable epimorphisms - reason: 'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' + reason: 'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' - property_id: effective cocongruences reason: >- @@ -75,7 +81,7 @@ unsatisfied_properties: $$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}$$ 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$. + From here, the rest of the proof is similar to the one for $\Ring$. special_objects: initial object: diff --git a/databases/catdat/data/categories/Sch.yaml b/databases/catdat/data/categories/Sch.yaml index 3a7b5923..3566e937 100644 --- a/databases/catdat/data/categories/Sch.yaml +++ b/databases/catdat/data/categories/Sch.yaml @@ -48,10 +48,10 @@ unsatisfied_properties: reason: Consider the subscheme $V(x-y) \cup V(y) \subseteq \IA^2$. It contains the diagonal but it is not symmetric. - property_id: semi-strongly connected - reason: This is because already the full subcategory of affine schemes is not semi-strongly connected, see the entry for $\CRing$. Specifically, there is no morphism between $\Spec(\IF_2)$ and $\Spec(\IF_3)$. + reason: This is because already the full subcategory of affine schemes is not semi-strongly connected, because $\CRing$ is not semi-strongly connected. Specifically, there is no morphism between $\Spec(\IF_2)$ and $\Spec(\IF_3)$. - property_id: generating set - reason: If $S$ is a generating set of schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine schemes, corresponding to a cogenerating set in the category of commutative rings, which we know does not exist (see there for the proof). + reason: If $S$ is a generating set of schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine schemes, corresponding to a cogenerating set in $\CRing$, which we know does not exist. - property_id: quotients of congruences reason: If $\Sch$ had quotients of congruences, then by this lemma it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1 \leftarrow \Spec(k(t)) \rightarrow \IA^1$ has no pushout - see MO/9961. diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index cdb7f9da..8939aa85 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/databases/catdat/data/categories/Set_c.yaml @@ -32,31 +32,31 @@ satisfied_properties: reason: The one-point set is clearly a generator. - property_id: cogenerator - reason: The two-point set is a cogenerator in $\Set$, hence also in $\Set_\c$. + reason: The two-point set is a cogenerator in $\Set$, hence also in $\Set_\c$. - property_id: semi-strongly connected - reason: This is because the larger category $\Set$ has this property. + reason: This is because the larger category $\Set$ has this property. - property_id: extensive - reason: The same proof as for $\Set$ applies. Actually, the category is "countably extensive". + reason: The same proof as for $\Set$ applies. Actually, the category is "countably extensive". - property_id: countably distributive - reason: By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts. + reason: By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts. - property_id: epi-regular reason: If $X \to Y$ is an epimorphism in $\Set_\c$, i.e. a surjective map, it is coequalizer of the two maps $X \times_Y X \rightrightarrows X$ in $\Set$ and hence also in $\Set_\c$. - property_id: subobject classifier - reason: This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide. + reason: This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide. - property_id: effective congruences - reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' + reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' - property_id: regular - reason: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. + reason: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. - property_id: coregular - reason: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. + reason: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. unsatisfied_properties: - property_id: small diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index dfe39e71..54db28d3 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/databases/catdat/data/categories/Set_f.yaml @@ -24,10 +24,10 @@ satisfied_properties: reason: 'The set $\{0,1\}$ is a cogenerator in $\Set_\f$: Assume that $f,g : X \rightrightarrows Y$ are two finite-to-one maps such that $h \circ f = h \circ g$ for all finite-to-one maps $h : Y \to \{0,1\}$. This exactly means $f^*(A)=g^*(A)$ for all finite subsets $A \subseteq Y$. Applying this to $A = \{f(x)\}$ for $x \in X$ we get $x \in f^*(\{f(x)\}) = g^*(\{f(x)\})$, so that $g(x) = f(x)$.' - property_id: extensive - reason: 'We first show that finite coproducts exist. The empty set is clearly initial. The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite. Hence, finite coproducts exist. A map $A \to X + Y$ yields a decomposition $A = A_X + A_Y$ with maps $A_X \to X$, $A_Y \to Y$ (since $\Set$ is extensive). Here, $A \to X + Y$ is finite-to-one iff $A_X \to X$ and $A_Y \to Y$ are finite-to-one.' + reason: 'We first show that finite coproducts exist. The empty set is clearly initial. The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite. Hence, finite coproducts exist. A map $A \to X + Y$ yields a decomposition $A = A_X + A_Y$ with maps $A_X \to X$, $A_Y \to Y$ (since $\Set$ is extensive). Here, $A \to X + Y$ is finite-to-one iff $A_X \to X$ and $A_Y \to Y$ are finite-to-one.' - property_id: equalizers - reason: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' + reason: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' - property_id: quotients of congruences reason: 'A congruence on a set $X$ in $\Set_\f$ is the same as an equivalence relation $R$ on $X$ whose equivalence classes are finite. In that case, the usual quotient map $p : X \to X/R$ is finite-to-one. Moreover, if $h : X/R \to Y$ is a map such that $h \circ p : X \to Y$ is finite-to-one, then $h$ is finite-to-one as well because $h^*(\{y\}) \subseteq p^*((h \circ p)^*(\{y\}))$ for all $y \in Y$. Therefore, $p$ is also the quotient in $\Set_\f$.' @@ -36,10 +36,10 @@ satisfied_properties: reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\f$. From the proof on quotients of congruences in $\Set_\f$, we have a quotient map $p : X \to X/E$ in $\Set_\f$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_f$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.' - property_id: effective cocongruences - reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' + reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' - property_id: locally cartesian closed - reason: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\f / X \simeq \FinSet^X$. This category is cartesian closed since the category $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. + reason: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\f / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. - property_id: epi-regular reason: 'If $f : X \to Y$ is an epimorphism in $\Set_\f$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one since $p_i^*(\{y\}) \cong f^*(\{y\})$ for $i=1,2$, and their coequalizer is also $f$ in $\Set_\f$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' diff --git a/databases/catdat/data/categories/Set_op.yaml b/databases/catdat/data/categories/Set_op.yaml index a7fa9eb8..ab8c4082 100644 --- a/databases/catdat/data/categories/Set_op.yaml +++ b/databases/catdat/data/categories/Set_op.yaml @@ -3,7 +3,7 @@ name: dual of the category of sets notation: $\Set^{\op}$ objects: sets morphisms: 'A morphism $f : X \to Y$ is a map of sets $Y \to X$.' -description: By definition, this category is the dual (or opposite) of the category of sets. +description: By definition, this category is the dual (or opposite) of the category $\Set$. nlab_link: https://ncatlab.org/nlab/show/opposite+category dual_category_id: Set diff --git a/databases/catdat/data/categories/Set_pointed.yaml b/databases/catdat/data/categories/Set_pointed.yaml index 1a484854..7bae64f1 100644 --- a/databases/catdat/data/categories/Set_pointed.yaml +++ b/databases/catdat/data/categories/Set_pointed.yaml @@ -34,10 +34,10 @@ satisfied_properties: reason: Every epimorphism is surjective for this category, and in an algebraic category every surjective homomorphism is a regular epimorphism. - property_id: coregular - reason: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for the category of sets and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts. + reason: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for $\Set$ and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts. - property_id: co-Malcev - reason: Malcev categories are closed under slice categories by Prop. 2.2.14 in Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of $\Set$, which is co-Malcev since every elementary topos is co-Malcev. + reason: Malcev categories are closed under slice categories by Prop. 2.2.14 in Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of $\Set$, which is co-Malcev since every elementary topos is co-Malcev. - property_id: cocartesian cofiltered limits reason: |- @@ -67,7 +67,7 @@ unsatisfied_properties: reason: 'Every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\Set_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\IN,0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.' - property_id: 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 \Set_*$ that freely adds a base point. + 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 \Set_*$ that freely adds a base point. special_objects: initial object: diff --git a/databases/catdat/data/categories/Setne.yaml b/databases/catdat/data/categories/Setne.yaml index 9b0f6114..7144444a 100644 --- a/databases/catdat/data/categories/Setne.yaml +++ b/databases/catdat/data/categories/Setne.yaml @@ -20,22 +20,22 @@ satisfied_properties: reason: The one-point set is clearly a generator. - property_id: cogenerator - reason: The two-point set is a cogenerator, this follows as for $\Set$. + reason: The two-point set is a cogenerator, this follows as for $\Set$. - property_id: products - reason: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. + reason: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. - property_id: binary coproducts reason: The disjoint union of two non-empty sets is non-empty. - property_id: cartesian closed - reason: This follows as for $\Set$, since for non-empty sets $X,Y$ there is at least one function $X \to Y$. + reason: This follows as for $\Set$, since for non-empty sets $X,Y$ there is at least one function $X \to Y$. - property_id: mono-regular - reason: This follows as for $\Set$. + reason: This follows as for $\Set$. - property_id: epi-regular - reason: This follows as for $\Set$. + reason: This follows as for $\Set$. - property_id: strongly connected reason: Use constant maps. diff --git a/databases/catdat/data/categories/Sh(X,Ab).yaml b/databases/catdat/data/categories/Sh(X,Ab).yaml index b1dd6e8a..665e94bd 100644 --- a/databases/catdat/data/categories/Sh(X,Ab).yaml +++ b/databases/catdat/data/categories/Sh(X,Ab).yaml @@ -29,7 +29,7 @@ unsatisfied_properties: reason: Consider constant sheaves for isomorphic but non-equal abelian groups. - property_id: split abelian - reason: 'Choose a point $x \in X$. The functor $x_* : \Ab \to \Sh(X,\Ab)$ (skyscraper sheaf) is exact, and its left adjoint $x^* : \Sh(X,\Ab) \to \Ab$ (stalk) satisfies $x^* x_* \cong \id_{\Ab}$. Now, since $\Ab$ is not split abelian (see here), there is a short exact sequence of abelian groups $0 \to A \to B \to C \to 0$ that does not split. Then $0 \to x_* A \to x_* B \to x_* C \to 0$ is also exact, but it does not split: Otherwise it would also be split after applying $x^*$, which however gives the original sequence in $\Ab$.' + reason: 'Choose a point $x \in X$. The functor $x_* : \Ab \to \Sh(X,\Ab)$ (skyscraper sheaf) is exact, and its left adjoint $x^* : \Sh(X,\Ab) \to \Ab$ (stalk) satisfies $x^* x_* \cong \id_{\Ab}$. Now, since $\Ab$ is not split abelian, there is a short exact sequence of abelian groups $0 \to A \to B \to C \to 0$ that does not split. Then $0 \to x_* A \to x_* B \to x_* C \to 0$ is also exact, but it does not split: Otherwise it would also be split after applying $x^*$, which however gives the original sequence in $\Ab$.' special_objects: initial object: diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 799d7ac4..b6597966 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -3,7 +3,7 @@ name: category of combinatorial species notation: $\Sp$ objects: combinatorial species, defined as functors $\IB \to \FinSet$, where $\IB$ is the category of finite sets and bijections morphisms: natural transformations -description: Most categorical properties are immediately inferred from $\FinSet$. Notice that this category is not locally small; it is just equivalent to a locally small category. +description: Most categorical properties are immediately inferred from $\FinSet$. Notice that this category is not locally small; it is just equivalent to a locally small category. nlab_link: https://ncatlab.org/nlab/show/species tags: @@ -15,10 +15,10 @@ related_categories: satisfied_properties: - property_id: essentially small - reason: This holds because $\FinSet$ and $\IB$ are essentially small. + reason: This holds because $\FinSet$ and $\IB$ are essentially small. - property_id: elementary topos - reason: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of order $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since $\FinSet$ is and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18. + reason: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of order $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since is $\FinSet$ an elementary topos and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18. - property_id: cogenerator reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' @@ -28,7 +28,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_id: 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 (see here). + 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. - property_id: skeletal reason: This is trivial. diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index 59eb2b8d..e9af74ff 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -32,7 +32,7 @@ satisfied_properties: reason: This is clear from the classification of epimorphisms as surjective continuous maps. - property_id: infinitary extensive - reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ 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 subspace topology. If $f$ is continuous, each $Y_i = f^{-1}(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' + reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ 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 subspace topology. If $f$ is continuous, each $Y_i = f^{-1}(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' - property_id: generator reason: The one-point space is a generator since it represents the forgetful functor $\Top \to \Set$. @@ -69,16 +69,16 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces. + reason: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces. - property_id: 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.' - property_id: 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\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. - property_id: 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. + 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. - property_id: effective cocongruences reason: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index 7972d31a..07fbb0e4 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/databases/catdat/data/categories/Top_pointed.yaml @@ -22,15 +22,15 @@ satisfied_properties: check_redundancy: false - property_id: complete - reason: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ is complete. Concretely, the limit of pointed spaces $(X_i,x_i)$ is the limit of the underlying spaces $X_i$ equipped with the base point that projects down to each $x_i$. + reason: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ is complete. Concretely, the limit of pointed spaces $(X_i,x_i)$ is the limit of the underlying spaces $X_i$ equipped with the base point that projects down to each $x_i$. check_redundancy: false - property_id: coequalizers - reason: This follows immediately from the fact that $\Top$ has coequalizers. + reason: This follows immediately from the fact that $\Top$ has coequalizers. check_redundancy: false - property_id: coproducts - reason: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ has wide pushouts. + reason: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ has wide pushouts. check_redundancy: false - property_id: well-powered @@ -52,7 +52,7 @@ satisfied_properties: reason: Since embeddings are regular monomorphisms in this category (see below) and hence strong monomorphisms, it suffices to prove that the canonical morphism $X \vee Y \hookrightarrow X \times Y$ is an embedding. For a proof, see MSE/4055988. - property_id: CIP - reason: This follows since $\Set_*$ has this property and the forgetful functor preserves products and coproducts. + reason: This follows since $\Set_*$ has this property and the forgetful functor preserves products and coproducts. - property_id: cocartesian cofiltered limits reason: >- @@ -64,7 +64,7 @@ satisfied_properties: reason: This follows from this lemma applied to the forgetful functor to $\Set$. - property_id: coregular - reason: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. + reason: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. unsatisfied_properties: - property_id: regular @@ -83,7 +83,7 @@ unsatisfied_properties: reason: This is trivial. - property_id: 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) := \{(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_id: 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.' @@ -93,19 +93,19 @@ unsatisfied_properties: reason: 'The image of $X \vee Y$ in $X \times 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 when both $X,Y$ are non-trivial.' - property_id: regular quotient object classifier - reason: We can recycle the proof for the category of pointed sets using discrete topological spaces. + reason: We can recycle the proof for $\Set_*$ using discrete topological spaces. - property_id: 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\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.' - property_id: 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. + 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. - property_id: effective congruences - reason: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case (see here). + 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_id: 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 := \{ *, 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/TorsAb.yaml b/databases/catdat/data/categories/TorsAb.yaml index 68af30f5..94bfee59 100644 --- a/databases/catdat/data/categories/TorsAb.yaml +++ b/databases/catdat/data/categories/TorsAb.yaml @@ -19,21 +19,21 @@ satisfied_properties: reason: There is a forgetful functor $\TorsAb \to \Ab$ and $\Ab$ is locally small. - property_id: cocomplete - reason: The embedding $\TorsAb \hookrightarrow \Ab$ is closed under colimits and $\Ab$ is cocomplete. + reason: The embedding $\TorsAb \hookrightarrow \Ab$ is closed under colimits and $\Ab$ is cocomplete. check_redundancy: false - property_id: complete - reason: The embedding $\TorsAb \hookrightarrow \Ab$ has a right adjoint, sending an abelian group $A$ to its torsion subgroup $T(A)$. Since $\Ab$ is complete, $\TorsAb$ is complete as well. The limit of a diagram of torsion abelian groups is the torsion subgroup of the limit of the underlying abelian groups. Notice that the torsion subgroup is not required in the case of equalizers, since a subgroup of a torsion abelian group is already torsion. Also, a finite product of torsion abelian groups is already torsion. + reason: The embedding $\TorsAb \hookrightarrow \Ab$ has a right adjoint, sending an abelian group $A$ to its torsion subgroup $T(A)$. Since $\Ab$ is complete, $\TorsAb$ is complete as well. The limit of a diagram of torsion abelian groups is the torsion subgroup of the limit of the underlying abelian groups. Notice that the torsion subgroup is not required in the case of equalizers, since a subgroup of a torsion abelian group is already torsion. Also, a finite product of torsion abelian groups is already torsion. check_redundancy: false - property_id: preadditive - reason: It is a full subcategory of the preadditive category $\Ab$. + reason: It is a full subcategory of the preadditive category $\Ab$. - property_id: normal - reason: 'If $f : A \to B$ is a monomorphism, it is injective (see below). In $\Ab$ it is then the kernel of $B \to B/f(A)$. Since $B/f(A)$ is torsion, it is also the kernel in $\TorsAb$.' + reason: 'If $f : A \to B$ is a monomorphism, it is injective (see below). In $\Ab$ it is then the kernel of $B \to B/f(A)$. Since $B/f(A)$ is torsion, it is also the kernel in $\TorsAb$.' - property_id: conormal - reason: 'If $f : A \to B$ is an epimorphism, it is surjective (see below). In $\Ab$ it is then the cokernel of its kernel $K \hookrightarrow A$. Since $K$ is torsion, it is also the cokernel in $\TorsAb$.' + reason: 'If $f : A \to B$ is an epimorphism, it is surjective (see below). In $\Ab$ it is then the cokernel of its kernel $K \hookrightarrow A$. Since $K$ is torsion, it is also the cokernel in $\TorsAb$.' - property_id: finitely accessible reason: We already know that (filtered) colimits exist and are preserved by the forgetful functor to $\Ab$. Every torsion abelian group is the filtered colimit of its finitely generated subgroups (which are finite). These are finitely presentable in $\Ab$, hence also in $\TorsAb$. diff --git a/databases/catdat/data/categories/TorsFreeAb.yaml b/databases/catdat/data/categories/TorsFreeAb.yaml index a3e6fa4b..1d3981b8 100644 --- a/databases/catdat/data/categories/TorsFreeAb.yaml +++ b/databases/catdat/data/categories/TorsFreeAb.yaml @@ -19,18 +19,18 @@ satisfied_properties: reason: There is a forgetful functor $\TorsFreeAb \to \Ab$ and $\Ab$ is locally small. - property_id: complete - reason: The embedding $\TorsFreeAb \hookrightarrow \Ab$ is closed under limits and $\Ab$ is complete. + reason: The embedding $\TorsFreeAb \hookrightarrow \Ab$ is closed under limits and $\Ab$ is complete. check_redundancy: false - property_id: cocomplete - reason: 'The embedding $\TorsFreeAb \hookrightarrow \Ab$ has a left adjoint, sending an abelian group $A$ to its torsion-free reflection $A/T(A)$, where $T(A)$ is the torsion subgroup of $A$. Since $\Ab$ is cocomplete, $\TorsFreeAb$ is cocomplete as well. The colimit of a diagram of torsion-free abelian groups is the torsion-free reflection of the colimit of the underlying abelian groups. Notice that the reflection is not required in the case of coproducts: the direct sum of torsion-free abelian groups is again torsion-free. It is also not required for filtered colimits.' + reason: 'The embedding $\TorsFreeAb \hookrightarrow \Ab$ has a left adjoint, sending an abelian group $A$ to its torsion-free reflection $A/T(A)$, where $T(A)$ is the torsion subgroup of $A$. Since $\Ab$ is cocomplete, $\TorsFreeAb$ is cocomplete as well. The colimit of a diagram of torsion-free abelian groups is the torsion-free reflection of the colimit of the underlying abelian groups. Notice that the reflection is not required in the case of coproducts: the direct sum of torsion-free abelian groups is again torsion-free. It is also not required for filtered colimits.' check_redundancy: false - property_id: finitely accessible reason: We already saw that filtered colimits exist and are preserved by the forgetful functor to $\Ab$. Every torsion-free abelian group is the filtered colimit of its finitely generated subgroups, which are in fact free. Finitely generated free abelian groups are finitely presentable in $\Ab$ and therefore also in $\TorsFreeAb$. - property_id: preadditive - reason: It is a full subcategory of the preadditive category $\Ab$. + reason: It is a full subcategory of the preadditive category $\Ab$. - property_id: cogenerator reason: The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. @@ -42,7 +42,7 @@ satisfied_properties: reason: >- It suffices to prove that regular monomorphisms (which are classified below) are stable under pushouts. Let $i : A \to B$ be a regular monomorphism in $\TorsFreeAb$, i.e. $i$ is injective and its $\Ab$-cokernel $B/i(A)$ is torsion-free, and let $f : B \to C$ be any morphism in $\TorsFreeAb$. Their $\Ab$-pushout is $$P = (B \times C)/\{(i(a),-f(a)): a \in A\}.$$ - It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. + It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. unsatisfied_properties: - property_id: skeletal diff --git a/databases/catdat/data/categories/Vect.yaml b/databases/catdat/data/categories/Vect.yaml index 4a724045..438c19dc 100644 --- a/databases/catdat/data/categories/Vect.yaml +++ b/databases/catdat/data/categories/Vect.yaml @@ -18,7 +18,7 @@ satisfied_properties: reason: There is a forgetful functor $\Vect \to \Set$ and $\Set$ is locally small. - property_id: split abelian - reason: It is a fact from linear algebra that every subspace has a complement. + reason: That $\Vect$ is abelian is a standard fact, see Mac Lane, Ch. VIII. Furthermore, it is a fact from linear algebra that every subspace has a complement, which is why every short exact sequence splits. - property_id: finitary algebraic reason: Take the algebraic theory of a vector space. diff --git a/databases/catdat/data/categories/Z.yaml b/databases/catdat/data/categories/Z.yaml index 7d32ea9f..f27a2a17 100644 --- a/databases/catdat/data/categories/Z.yaml +++ b/databases/catdat/data/categories/Z.yaml @@ -16,30 +16,34 @@ related_categories: satisfied_properties: - property_id: complete - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. - property_id: cocomplete - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. check_redundancy: false - property_id: infinitary extensive - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. - property_id: exact filtered colimits - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. - property_id: mono-regular - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. check_redundancy: false - property_id: epi-regular - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. - property_id: regular - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. - property_id: coregular - reason: This follows immediately from the fact for $\Set$. + reason: This follows immediately from the fact for $\Set$. + + - property_id: co-Malcev + reason: This follows immediately from the fact for $\Set$. + check_redundancy: false - property_id: effective congruences reason: 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.' @@ -48,10 +52,6 @@ satisfied_properties: reason: 'If we have a cocongruence $X\rightrightarrows E$ in $[\CRing, \Set]$, then evaluating at any commutative gives a cocongruence in $\Set$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$, and by the dual of this result applied pointwise, the cokernel pair of $h$ is $E$.' check_redundancy: false - - property_id: co-Malcev - reason: This is true because the category of sets is co-Malcev. - check_redundancy: false - unsatisfied_properties: - property_id: locally essentially small reason: See MO/390611 for example. @@ -60,19 +60,19 @@ unsatisfied_properties: reason: This is trivial. - property_id: Malcev - reason: Any counterexample for $\Set$ (i.e., any non-symmetric reflexive relation) yields one for this category by taking constant functors. + reason: Any counterexample for $\Set$ (i.e., any non-symmetric reflexive relation) yields one for this category by taking constant functors. - property_id: semi-strongly connected - reason: This is because already the full subcategory of representable functors is not semi-strongly connected, see the entry for $\CRing$. Specifically, there is no morphism between $\Hom(\IF_2,-)$ and $\Hom(\IF_3,-)$. + reason: This is because already the full subcategory of representable functors is not semi-strongly connected, because $\CRing$ is not semi-strongly connected. Specifically, there is no morphism between $\Hom(\IF_2,-)$ and $\Hom(\IF_3,-)$. - property_id: cartesian closed - reason: 'There are functors $F,G : \CRing \to \Set$ such that $\Hom(F,G)$ is not essentially small, see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda, which simplifies to $\Hom(1,[F,G]) \cong \Hom(1 \times F,G) \cong \Hom(F,G)$, a contradiction.' + reason: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small, see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda, which simplifies to $\Hom(1,[F,G]) \cong \Hom(1 \times F,G) \cong \Hom(F,G)$, a contradiction.' - property_id: well-powered reason: 'Consider the functor $F$ from MO/390611 for example. The collection of subobjects of $F$ is not isomorphic to a set: for each infinite cardinal $\kappa$, simply cut off the construction of $F$ at $\kappa$. This yields a different subobject for each $\kappa$.' - property_id: 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 [\CRing, \Set]$ that maps a set to its constant functor. + 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 [\CRing, \Set]$ that maps a set to its constant functor. special_objects: initial object: diff --git a/databases/catdat/data/categories/sSet.yaml b/databases/catdat/data/categories/sSet.yaml index d193ccdc..f2082f73 100644 --- a/databases/catdat/data/categories/sSet.yaml +++ b/databases/catdat/data/categories/sSet.yaml @@ -1,7 +1,7 @@ id: sSet name: category of simplicial sets notation: $\sSet$ -objects: simplicial sets, i.e. functors $\Delta^{\op} \to \Set$ where $\Delta$ is the simplex category +objects: simplicial sets, i.e. functors $\Delta^{\op} \to \Set$ where $\Delta$ denotes the simplex category. morphisms: natural transformations description: null nlab_link: https://ncatlab.org/nlab/show/SimpSet diff --git a/databases/catdat/data/categories/walking_coreflexive_pair.yaml b/databases/catdat/data/categories/walking_coreflexive_pair.yaml index 7a0de494..335f7fd9 100644 --- a/databases/catdat/data/categories/walking_coreflexive_pair.yaml +++ b/databases/catdat/data/categories/walking_coreflexive_pair.yaml @@ -31,7 +31,7 @@ satisfied_properties: reason: This is obvious. - property_id: terminal object - reason: The object $[0]$ is terminal since it is already terminal in $\Delta$. + reason: The object $[0]$ is terminal since it is already terminal in $\Delta$. - property_id: epi-regular reason: 'The only non-identity epimorphism is $p$, which is the coequalizer of $\id, ip : [1] \rightrightarrows [1]$ (since $pi = \id$).' @@ -40,16 +40,16 @@ satisfied_properties: reason: 'The only non-identity monomorphisms are $i$ and $j$. The morphism $i$ is the equalizer of $\id, ip : [1] \rightrightarrows [1]$ (since $pi = \id$), and for $j$ it is the same argument.' - property_id: coequalizers - reason: 'We already know that the simplex category $\Delta$ has coequalizers, and the proof has shown that the cardinality does not increase, so we are done. But a direct proof is also possible: There are four non-equal parallel pairs: $(i,j)$, $(ip,jp)$, $(\id,ip)$, and $(\id,jp)$. The first two have the same coequalizer (if it exists) since $p$ is an epimorphism, the last two are symmetric, and we already remarked that $p$ is a coequalizer of $(\id,ip)$. So it suffices to check that $p$ is a coequalizer of $i,j$, which is easy.' + reason: 'We already know that the $\Delta$ has coequalizers, and the proof has shown that the cardinality does not increase, so we are done. But a direct proof is also possible: There are four non-equal parallel pairs: $(i,j)$, $(ip,jp)$, $(\id,ip)$, and $(\id,jp)$. The first two have the same coequalizer (if it exists) since $p$ is an epimorphism, the last two are symmetric, and we already remarked that $p$ is a coequalizer of $(\id,ip)$. So it suffices to check that $p$ is a coequalizer of $i,j$, which is easy.' - property_id: generator - reason: The object $[0]$ is generator since this is already true in $\Delta$. A direct proof is also possible. + reason: The object $[0]$ is generator since this is already true in $\Delta$. A direct proof is also possible. - property_id: cogenerator - reason: The object $[1]$ is cogenerator since this is already true in $\Delta$. A direct proof is also possible. + reason: The object $[1]$ is cogenerator since this is already true in $\Delta$. A direct proof is also possible. - property_id: cosifted - reason: Our proof that the simplex category $\Delta$ is cosifted has only used $[0],[1]$ as auxiliary objects and therefore also shows that $\Delta^{\leq 1}$ is cosifted. + reason: Our proof that the $\Delta$ is cosifted has only used $[0],[1]$ as auxiliary objects and therefore also shows that $\Delta^{\leq 1}$ is cosifted. - property_id: generalized variety reason: This actually holds for every truncated simplex category $\Delta^{\leq n}$. See MO/510760 for a proof that sifted colimits exist. See MO/510827 for a proof that every object is strongly finitely presentable. diff --git a/databases/catdat/data/categories/walking_span.yaml b/databases/catdat/data/categories/walking_span.yaml index c5dcfb3d..a37f4fb3 100644 --- a/databases/catdat/data/categories/walking_span.yaml +++ b/databases/catdat/data/categories/walking_span.yaml @@ -35,7 +35,7 @@ satisfied_properties: reason: We have $0 \times x = 0$ for all $x$, $x \times x = x$, and $1 \times 2 = 0$. - property_id: locally cartesian closed - reason: The slice category over $0$ is the trivial category, and the slice category over $1$ is the interval category, which is cartesian closed (see there). The same holds for $2$ by symmetry. + 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_id: 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. diff --git a/databases/catdat/data/categories/walking_splitting.yaml b/databases/catdat/data/categories/walking_splitting.yaml index a0708a9e..a8df1229 100644 --- a/databases/catdat/data/categories/walking_splitting.yaml +++ b/databases/catdat/data/categories/walking_splitting.yaml @@ -42,11 +42,11 @@ 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_id: 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 := 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_id: sifted colimits reason: |- - We work with the representation of the category as $\Vect^{\leq 1}_{\IF_2}$, the category of vector spaces over $\IF_2$ of dimension $\leq 1$. It suffices to show that it is closed under sifted colimits in $\Vect_{\IF_2}$. More generally, we show this for $\Vect^{\leq d}_K \subseteq \Vect_K$, where $d \in \IN$ and $K$ is a field. So let $X : \I \to \Vect_K$ be a sifted diagram with colimit $(u_i : X_i \to X_\infty)_{i \in \I}$. Since $\I$ is sifted, for finitely many objects $i_1,\dotsc,i_n \in \I$ there is an object $k$ that admits morphisms $i_1 \to k, \dotsc, i_n \to k$; this is all we need to know about $\I$. Assume that each $X_i$ is of dimension $\leq d$, we need to show this for $X_\infty$ as well. + We work with the representation of the category as $\Vect^{\leq 1}_{\IF_2}$, the category of vector spaces over $\IF_2$ of dimension $\leq 1$. It suffices to show that it is closed under sifted colimits in $\Vect_{\IF_2}$. More generally, we show this for $\Vect^{\leq d}_K \subseteq \Vect_K$, where $d \in \IN$ and $K$ is a field. So let $X : \I \to \Vect_K$ be a sifted diagram with colimit $(u_i : X_i \to X_\infty)_{i \in \I}$. Since $\I$ is sifted, for finitely many objects $i_1,\dotsc,i_n \in \I$ there is an object $k$ that admits morphisms $i_1 \to k, \dotsc, i_n \to k$; this is all we need to know about $\I$. Assume that each $X_i$ is of dimension $\leq d$, we need to show this for $X_\infty$ as well. Every element in $X_\infty$ is a finite sum of elements of the form $u_i(x_i)$ with $x_i \in X_i$. Choose an object $k$ with morphisms $i \to k$ for every occurring $i$. If $y_i \in X_k$ denotes the image of $x_i$, we get $\sum_i u_i(x_i) = \sum_i u_k(y_i) = u_k(\sum_i y_i)$. Therefore, every element of $X_\infty$ has the form $u_i(x_i)$ for some $i \in \I$ and $x_i \in X_i$. Moreover, for finitely many elements in $X_\infty$ the index $i$ may be chosen uniformly. Now, if $X_\infty$ has dimension $> d$, it would have linearly independent vectors $v_0,\dotsc,v_d$, all of which have a preimage in $X_i$ for some $i \in \I$. But then these preimages would be linearly independent as well, which contradicts $\dim(X_i) \leq d$. check_redundancy: false diff --git a/databases/catdat/data/functors/forget_vector.yaml b/databases/catdat/data/functors/forget_vector.yaml index 0e2cc005..54004565 100644 --- a/databases/catdat/data/functors/forget_vector.yaml +++ b/databases/catdat/data/functors/forget_vector.yaml @@ -9,7 +9,7 @@ satisfied_properties: - property_id: conservative reason: It is standard that the inverse of a bijective linear map is also linear. - property_id: epimorphism-preserving - reason: This follows from the classifications of epimorphisms in the category of vector spaces and in the category of sets. + reason: This follows from the classifications of epimorphisms in $\Vect$ and in $\Set$. - property_id: finitary reason: For every algebraic category the forgetful functor to the category of sets preserves filtered colimits. - property_id: monadic From 574447367a719279296504918e03e50d6642f8cd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 08:24:47 +0200 Subject: [PATCH 3/3] mention links in guidelines --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a182811e..9a001b41 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -122,7 +122,7 @@ When contributing new data (categories, functors, properties, implications), ple - **Special Objects and Morphisms**: For each new category, try to specify its special objects (terminal object, initial object, etc.) in the corresponding table. Also try to specify its special morphisms (isomorphisms, monomorphisms, epimorphisms). -- **Proofs for New Properties**: For every new property, for each existing category or functor, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically via some implication. Use the property detail page to check unknown categories. As mentioned in the section on tests, for a list of selected categories it is actually mandatory to decide their properties. +- **Proofs for New Properties**: For every new property, for each existing category or functor, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically via some implication. Use the property detail page to check unknown categories. These proofs may also refer to other categories, in which case you may add links to their corresponding pages. As mentioned in the section on tests, for a list of selected categories it is actually mandatory to decide their properties. - **Counterexamples**: Ensure that at least one category does not satisfy any new property of categories that is added. If no existing category fits, add a new category that does not have the new property. The same remarks apply to properties of functors.