diff --git a/.cspell.json b/.cspell.json index 8d092b13..a62b95f9 100644 --- a/.cspell.json +++ b/.cspell.json @@ -62,6 +62,7 @@ "cocartesian", "coclosed", "cocomplete", + "cocompleteness", "cocompletion", "cocone", "cocones", @@ -163,6 +164,7 @@ "freyd", "Freyd", "Frobenius", + "functionals", "functor", "functorial", "functors", diff --git a/database/data/categories/Ab.yaml b/database/data/categories/Ab.yaml index 6564f3d1..6ce6a016 100644 --- a/database/data/categories/Ab.yaml +++ b/database/data/categories/Ab.yaml @@ -25,6 +25,7 @@ satisfied_properties: - property: abelian proof: This is standard, see Mac Lane, Ch. VIII. + label: ab_abelian - property: finitary algebraic proof: Take the algebraic theory of a commutative group. diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index e8d409bc..41b81a5d 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -26,9 +26,13 @@ satisfied_properties: - property: disjoint finite products proof: One can take the same proof as for $\Ring$. + references: + - ring_disjoint_finite_products - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + references: + - grp_malcev unsatisfied_properties: - property: skeletal @@ -51,9 +55,13 @@ unsatisfied_properties: - property: coregular proof: 'We just need to tweak the proof for $\Ring$. Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B \coloneqq M_2(K)$ and $A \coloneqq K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' + references: + - ring_not_coregular - property: regular quotient object classifier - proof: 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 the reflective subcategory $\CAlg(R)$ by Lemma 1 here (dualized). + proof: We may copy the proof for $\CAlg(R)$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in the reflective subcategory $\CAlg(R)$ by Lemma 1 here (dualized). + references: + - calg_no_regular_quotient_object_classifier - property: cocartesian cofiltered limits proof: >- @@ -66,6 +74,8 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The counterexample is similar to the one for $\Ring$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.' + references: + - ring_no_effective_cocongruences special_objects: initial object: diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml index 4105d503..3895bd54 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -122,6 +122,8 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: 'The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the Banach space with underlying vector space $\IC$ and the norm $|x|_n \coloneqq \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $X_n \to X_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $X$ be the colimit of all $X_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| \coloneqq \inf \{|x|_m : n \leq m \}$ for $x \in X_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, which is also $0$. Thus, the monomorphisms $X_1 \hookrightarrow X_n$ become the zero map $X_1 \to 0$ in the colimit, which is not a monomorphism.' + references: + - met_no_filtered_colimit_stable_monos - property: cofiltered-limit-stable epimorphisms proof: 'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$, equipped with the usual norm. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ and $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.' diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml index 04313c46..9a4d1984 100644 --- a/database/data/categories/CAlg(R).yaml +++ b/database/data/categories/CAlg(R).yaml @@ -27,9 +27,13 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + references: + - grp_malcev - property: coextensive proof: One can use the same proof as for $\CRing$. + references: + - cring_coextensive unsatisfied_properties: - property: skeletal @@ -55,6 +59,9 @@ unsatisfied_properties: - property: regular quotient object classifier proof: '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.' + label: calg_no_regular_quotient_object_classifier + references: + - cring_no_regular_quotient_object_classifier - property: cofiltered-limit-stable epimorphisms proof: 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. diff --git a/database/data/categories/CMon.yaml b/database/data/categories/CMon.yaml index e0a67e53..5a861ffb 100644 --- a/database/data/categories/CMon.yaml +++ b/database/data/categories/CMon.yaml @@ -49,9 +49,12 @@ unsatisfied_properties: - property: regular subobject classifier proof: We can use exactly the same proof as for $\Mon$. + references: + - mon_no_regular_subobject_classifier - property: regular quotient object classifier proof: 'If $P \in \CMon$ is a regular quotient object classifier, this means that every surjective homomorphism of commutative monoids $A \to B$ is the cokernel of a unique homomorphism $P \to A$. But there are many surjective homomorphisms which are no cokernels at all: Consider the Boolean monoid $(\{0,1\},\vee)$ with $1 \vee 1 = 1$ and the surjective homomorphism $f : (\IN,+) \to (\{0,1\},\vee)$ defined by $f(0)=0$ and $f(n)=1$ for $n \geq 1$. It has trivial kernel, but is no isomorphism, so it cannot be a cokernel.' + label: cmon_no_regular_quotient_object_classifier - property: CSP proof: First of all, epimorphisms in $\CMon$ are preserved and reflected by the forgetful functor to $\Mon$ (see below). Furthermore, 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 $\CMon$ the canonical homomorphism $\bigoplus_{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/database/data/categories/CRing.yaml b/database/data/categories/CRing.yaml index 4470485e..dc2f9b31 100644 --- a/database/data/categories/CRing.yaml +++ b/database/data/categories/CRing.yaml @@ -30,6 +30,8 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + references: + - grp_malcev - property: coextensive proof: >- @@ -47,6 +49,7 @@ satisfied_properties: is an isomorphism. Since $p_1 : A \times B \to A$ is surjective with kernel $0 \times B = \langle (0,1) \rangle$, we have $T_A = T/\langle f(1,0)\rangle$, and likewise, $T_B = T/\langle f(0,1) \rangle$. The elements $f(1,0)$ and $f(0,1)$ are orthogonal idempotents in $T$. Therefore, the claim follows from the well-known result in commutative algebra that if $R$ is a commutative ring and $e \in R$ is an idempotent, then $R \to R/\langle e \rangle \times R/\langle 1-e \rangle$ is an isomorphism. One can also deduce this from the Chinese Remainder Theorem. An alternative proof, which we only sketch, uses the category of locally ringed spaces $\LRS$, which is infinitary extensive. It follows that the category of affine schemes is extensive by Lemma 11 here, and this category is anti-equivalent to $\CRing$. This argument is not circular since our proof of extensivity of $\LRS$ does not use coextensivity of $\CRing$. + label: cring_coextensive unsatisfied_properties: - property: skeletal @@ -54,6 +57,7 @@ unsatisfied_properties: - property: semi-strongly connected proof: There is no homomorphism between $\IF_2$ and $\IF_3$. + label: cring_no_semi_strongly_connected - property: balanced proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. @@ -72,6 +76,7 @@ unsatisfied_properties: - property: regular quotient object classifier proof: 'Assume that $P \to \IZ$ is a regular quotient object classifier. If $J$ denotes its kernel, this means that every ideal $I \subseteq A$ of any commutative ring has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed ring of $\sigma$. But then $I$ is generated by elements in the fixed ring. This fails for $A = \IZ[X]$, $I = \langle X \rangle$, $\sigma(X)=-X$. The fixed ring is $\IZ[X^2]$, and if $I$ was generated by elements $f \in \IZ[X^2] \cap I$, they would be multiples of $X^2$, but $X$ is not a multiple of $X^2$.' + label: cring_no_regular_quotient_object_classifier - property: cofiltered-limit-stable epimorphisms proof: 'For a prime $p$ consider the sequence of projections $\cdots \to \IZ/p^2 \to \IZ/p$ and the constant sequence $\cdots \to \IZ \to \IZ$. The surjective homomorphisms $\IZ \to \IZ/p^n$ induce the homomorphism $\IZ \to \IZ_p$ in the limit, where $\IZ_p$ is the ring of $p$-adic integers. It is not surjective since $\IZ_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use SP/04W0 to conclude that it is no epimorphism in $\CRing$.' diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 61dfb8ae..11fd7d2c 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -51,13 +51,15 @@ unsatisfied_properties: proof: See Example 3.14 at the nLab. - property: coregular - proof: '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.' + proof: 'We already know that $\Mon$ is not coregular; in fact we have shown that 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.' + references: + - mon_not_coregular - property: Malcev proof: Use that $\Set$ is not Malcev and consider sets as discrete categories. - property: co-Malcev - proof: '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.' + proof: 'We can adapt the counterexample for monoids (cf. MO/509552) 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: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Cat$ that maps a set to its discrete category. @@ -67,6 +69,8 @@ unsatisfied_properties: The counterexample is similar to the one for $\Mon$: Let $X$ be the walking idempotent, and let $E$ be the delooping of the monoid with presentation $$\langle p, q \mid p^2=p,\, q^2=q,\, pq=q,\, qp=p \rangle.$$ The induced relation on functors in $[X, \C]$ is that $F \sim G$ if and only if $F$ and $G$ send the object of $X$ to the same object of $\C$, and they send the idempotent of $X$ to idempotent morphisms $a, b$ in $\C$ satisfying $ab=b$, $ba=a$. From here, the proof that this gives a cocongruence on $\Cat$ which is not effective is similar to the one in $\Mon$. + references: + - mon_no_effective_cocongruences - property: regular subobject classifier proof: >- diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index 187dcf1c..c1ecb7d6 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -70,6 +70,8 @@ unsatisfied_properties: - property: regular subobject classifier proof: The proof is almost identical to the one for $\Haus$. + references: + - haus_no_regular_subobject_classifier - property: natural numbers object proof: >- @@ -82,6 +84,8 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: 'The proof is similar to $\Haus$. For $n \geq 1$ let $X_n$ be the pushout of $[1/n, 1] \hookrightarrow [0, 1]$ with itself. That is, $X_n$ is the union of two unit intervals $[0, 1] \times \{ 1 \}$ and $[0, 1] \times \{ 2 \}$ where we identify $(x,1) \equiv (x,2)$ when $x \geq 1/n$. As in the construction for $\Haus$, we see that the colimit in $\Haus$ is $[0, 1]$ where all corresponding points of both unit intervals are identified. Since this is compact Hausdorff, it also provides the colimit in $\CompHaus$. Again, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to [0,1]$ in the colimit, which is not a monomorphism.' + references: + - haus_no_filtered-colimit-stable_monos - property: exact cofiltered limits proof: |- diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index fb79a8b1..2ccb85b7 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -29,30 +29,42 @@ satisfied_properties: - property: terminal object proof: The ordered set $[0] = \{0\}$ is terminal. + label: delta_terminal_object - property: strongly connected proof: For all $n,m$ there are morphisms $[n] \to [0] \to [m]$. - property: extremal generator proof: The ordered set $[1] = \{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. + label: delta_extremal_generator + references: + - preord_extremal_generator - property: extremal cogenerator proof: The ordered set $[1] = \{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. + label: delta_extremal_cogenerator + references: + - pos_extremal_cogenerator - property: skeletal proof: 'If $f : [n] \to [m]$ is an isomorphism, then $n + 1 = m + 1$ by comparing the cardinalities, hence $n = m$.' - property: coequalizers proof: 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\}$. + label: delta_coequalizers - property: core-thin proof: The category $\FinOrd \setminus \{\varnothing\}$ is core-thin because already $\FinOrd$ is core-thin. - property: mono-regular proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + references: + - finord_mono-regular - property: epi-regular proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + references: + - finord_epi-regular - property: cosifted proof: >- @@ -61,9 +73,12 @@ satisfied_properties: It remains to show that all point spans are connected to each other. Assume $x_0,x_1 \in X$ and $y \in Y$, w.l.o.g. $x_0 \leq x_1$. Define the map $f : [1] \to X$ by $f(0) = x_0$, $f(1) = x_1$, and the map $g : [1] \to Y$ by $g(0)=g(1)=y$. They are order-preserving and fit into a zig-zag of spans: $$\begin{CD} X @<{x_0}<< [0] @>{y}>> Y \\ @| @V{0}VV @| \\ X @<{f}<< [1] @>{g}>> Y \\ @| @A{1}AA @| \\ X @<{x_1}<< [0] @>{y}>> Y \end{CD}$$ This shows that the choice of $x \in X$ does not matter, and for $y \in Y$ the proof is the same. + label: delta_cosifted - property: ℵ₁-cofiltered limits proof: We already know that $\FinOrd$ has $\aleph_1$-cofiltered limits and that the forgetful functors to $\FinSet$ and $\Set$ preserve them. Therefore, it suffices to prove that a $\aleph_1$-cofiltered limit of non-empty finite sets is also non-empty. While a direct proof is possible, we can conveniently derive this from Lemma 1 here by regarding finite sets as discrete compact Hausdorff spaces. + references: + - finset_aleph1-cofiltered-limits unsatisfied_properties: - property: strict terminal object @@ -77,9 +92,13 @@ unsatisfied_properties: - property: sequential colimits proof: 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. + references: + - finord_no_sequential_colimits - property: sequential limits proof: 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. + references: + - finord_no_sequential_limits - property: pushouts proof: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index 7defa5b1..374cce9d 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -41,7 +41,7 @@ satisfied_properties: proof: >- We prove that $\{0,1\}$ is an extremal cogenerator. First, to prove it 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\}$. - Now, suppose we have a surjective map $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty proper subsets, and it certainly also maps $\varnothing \mapsto \varnothing$ and $Y \mapsto X$. Therefore, since the contravariant powerset functor is conservative, that implies $f$ is an isomorphism. + Now, suppose we have a surjective map $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty proper subsets, and it certainly also maps $\varnothing \mapsto \varnothing$ and $Y \mapsto X$. Therefore, since the contravariant power set functor is conservative, that implies $f$ is an isomorphism. - property: multi-complete proof: >- diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 8eef9bf8..e819c4ed 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -75,6 +75,7 @@ satisfied_properties: Second, every filtered vector space $(V,F)$ is the filtered colimit of the spaces $(V,F_{< N})$ for $N \in \IN$, where $$F_{< N}^n(V) \coloneqq \begin{cases} F^n(V) & n < N \\ 0 & n \geq N. \end{cases}$$ Indeed, we have $F_{< N} \subseteq F_{< N+1}$, so that $\id_V : (V,F_{- It remains to prove that regular epimorphisms are stable under pullbacks. This follows immediately from their classification below, from the fact that $F^n$ preserves limits, and from the regularity of $\Vect$. @@ -83,6 +84,7 @@ satisfied_properties: In more detail, if $(V,F) \to (W,F)$ is a regular epimorphism and $(U,F) \to (W,F)$ is any morphism, then $(V,F) \times_{(W,F)} (U,F) \to (U,F)$ is a regular epimorphism, since $V \times_W U \to U$ is surjective and, for every $n \in \IZ$, the restricted map $$F^n(V \times_W U) = F^n(V) \times_{F^n(W)} F^n(U) \to F^n(U)$$ is surjective. + - property: coregular proof: >- It remains to prove that regular monomorphisms (as classified below) are stable under pushouts. Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective, since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ is abelian, and hence coregular. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. diff --git a/database/data/categories/FinGrp.yaml b/database/data/categories/FinGrp.yaml index f3a3f45a..2e3b8fa8 100644 --- a/database/data/categories/FinGrp.yaml +++ b/database/data/categories/FinGrp.yaml @@ -52,6 +52,8 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: For $\FinSet$ know that the embedding $\FinSet \hookrightarrow \Set$ is closed under $\aleph_1$-cofiltered limits. From this and the fact that the forgetful functor $\Grp \to \Set$ preserves limits it follows that $\FinGrp \hookrightarrow \Grp$ is closed under $\aleph_1$-cofiltered limits. + references: + - finset_aleph1-cofiltered-limits unsatisfied_properties: - property: small diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index 20626dd9..edd57786 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -36,21 +36,27 @@ satisfied_properties: - property: extremal generator proof: The ordered set $\{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. + references: + - preord_extremal_generator - property: extremal cogenerator proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. + references: + - pos_extremal_cogenerator - property: equalizers - proof: Take the equalizer in $\FinSet$ and restrict the order. + proof: Take the equalizer in $\FinSet$ and restrict the order. - property: coequalizers proof: It suffices to construct quotients by equivalence relations. Let $\sim$ be an equivalence relation on $X$, where $(X,\leq)$ is a finite ordered set. Since $X$ is finite, by induction we may assume that $\sim$ is generated by a single relation $(a,b)$. If $a=b$, there is nothing to prove. If $a < b$ and $X = \{0,1,\dotsc,n-1\}$ with the usual order, the quotient is $\{0,1,\dotsc,a,b+1,\dotsc,n-1\}$ with the usual order. - property: mono-regular proof: 'Let $i : A \to B$ be a monomorphism of finite ordered sets. If $A$ is empty, then $i$ is clearly regular, so assume it is not. The map $i$ is injective (see below), hence order-reflecting. Define maps $u,v : B \to A$ by $u(b) \coloneqq \max \{a \in A : i(a) \leq b \}$ and $v(b) \coloneqq \min \{a \in A : b \leq i(a) \}$. These are order-preserving and satisfy $u \circ i = v \circ i$, both sides are $\id_A$. Conversely, if $b \in B$ satisfies $u(b) = v(b) \eqqcolon a$, then $i(a) \leq b$ and $b \leq i(a)$, hence $b = i(a)$. This shows that $i$ is the equalizer of $u,v$.' + label: finord_mono-regular - property: epi-regular proof: 'Let $f : A \to B$ be an epimorphism of finite ordered sets. It is surjective (see below). Define $u,v : B \to A$ by $u(b) \coloneqq \min(f^{-1}(b))$ and $v(b) \coloneqq \max(f^{-1}(b))$. One can easily check that $u,v$ are order-preserving maps with $f \circ u = f \circ v$ (both sides are $\id_B$). Let $h : A \to T$ be an order-preserving map with $h \circ u = h \circ v$. Then $h(a)$ only depends on $b \coloneqq f(a)$: We have $u(b) \leq a \leq v(b)$, hence $h(u(b)) \leq h(a) \leq h(v(b)) = h(u(b))$. Therefore, there is a unique map $\tilde{h} : B \to T$ with $\tilde{h}(f(a)) = h(a)$, and one easily checks that it is order-preserving. This shows that $f$ is the coequalizer of $u,v$.' + label: finord_epi-regular - property: core-thin proof: 'Let $f : \{1 < \cdots < n \} \to \{1 < \cdots < n \}$ be an automorphism. Then $f(i)$ is the smallest element not contained in $\{f(j) : j < i\}$. From this one can deduce $f(i)=i$ by induction.' @@ -76,9 +82,11 @@ unsatisfied_properties: - property: sequential limits proof: Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable, hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\FinOrd$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But this is not a finite set. + label: finord_no_sequential_limits - property: sequential colimits proof: 'Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. Assume the sequence of inclusion maps $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has a colimit $(f_n : [n] \to X)$ in $\FinOrd$. Let $n_0 \geq 0$ be fixed. I claim that $f_{n_0}$ is injective, which will then yield a contradiction by taking $n_0 \geq \card(X)$. For $n \geq 0$ define $g_n : [n] \to [n_0]$ as follows. For $n \leq n_0$ it is the inclusion, and for $n \geq n_0$ it is the surjection which keeps all elements of $[n_0]$ and maps all other elements to $n_0$. Observe that $g_n$ preserves the order and $g_{n+1} |_{[n]} = g_n$. Hence, there is a unique order-preserving map $g : X \to [n_0]$ with $g \circ f_n = g_n$ for all $n$. For $n = n_0$ this shows $g \circ f_{n_0} = \id_{[n_0]}$, and $f_{n_0}$ is injective.' + label: finord_no_sequential_colimits special_objects: initial object: diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index ca27d0a4..a981bf27 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -42,6 +42,7 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: 'Let $D : \I \to \FinSet$ be a $\aleph_1$-cofiltered diagram. Let $(p_i : P \to D(i))_{i \in \I}$ be a limit cone of the corresponding diagram in $\Set$. We only need to show that $P$ is finite. If not, then it contains a sequence of pairwise distinct elements $x_1,x_2,\dotsc$. For all $n \neq m$ there is some $i_{n,m} \in I$ with $p_{i_{n,m}}(x_n) \neq p_{i_{n,m}}(x_m)$. Since $\I$ is $\aleph_1$-cofiltered, it contains a cone $(j \to i_{m,n})$. Then $p_j(x_n) \neq p_j(x_m)$ for all $n \neq m$. This is not possible since $D(j)$ is a finite set.' + label: finset_aleph1-cofiltered-limits unsatisfied_properties: - property: small diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 98cb1cb4..763d15a3 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -25,6 +25,8 @@ satisfied_properties: - property: extremal generator proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. + references: + - vect_extremal_generator - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_f.yaml b/database/data/categories/FinVect_f.yaml index 7fa859c9..c994ef71 100644 --- a/database/data/categories/FinVect_f.yaml +++ b/database/data/categories/FinVect_f.yaml @@ -28,6 +28,8 @@ satisfied_properties: - property: extremal generator proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. + references: + - vect_extremal_generator - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index 49fb75b9..0329565e 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -25,6 +25,8 @@ satisfied_properties: - property: extremal generator proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. + references: + - vect_extremal_generator - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 0ccd93d6..13dc27f8 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -25,6 +25,8 @@ satisfied_properties: - property: extremal generator proof: The group $\IZ$ is an extremal generator even in $\Grp$. Now apply Lemma 10 here. + references: + - grp_extremal_generator - property: cogenerator proof: It is easy to check that $\IZ$ is a cogenerator for free abelian groups. diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 0ffee152..180e139f 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -34,7 +34,10 @@ satisfied_properties: proof: Since epimorphisms are surjective (see below), this is the first isomorphism theorem for groups. - property: Malcev - proof: See Example 2.2.4 in Malcev, protomodular, homological and semi-abelian categories. + proof: >- + See Example 2.2.4 in Malcev, protomodular, homological and semi-abelian categories. + Alternatively, here is a direct proof: let $G$ be a group and let $U \subseteq G^2$ be a subgroup containing the diagonal. Then $N := \{g \in G : (g,1) \in U\}$ is clearly a subgroup of $G$. It is a normal subgroup because, if $g \in N$ and $h \in G$, then $U$ contains $(h,h) (g,1) (h,h)^{-1} = (h g h^{-1},1)$, i.e. $h g h^{-1} \in N$. Moreover, $U$ contains $(g,g')$ if and only if it contains $(g,g') (g',g')^{-1} = (g g'^{-1},1)$, i.e. $g g'^{-1} \in N$. This means that $U$ is the congruence induced by the normal subgroup $N \subseteq G$ and is therefore transitive and symmetric. + label: grp_malcev - property: effective cocongruences proof: A proof can be found here. @@ -42,6 +45,7 @@ satisfied_properties: - property: extremal generator proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor $\Grp \to \Set$, which is faithful and conservative. check_redundancy: false + label: grp_extremal_generator unsatisfied_properties: - property: skeletal @@ -52,6 +56,7 @@ unsatisfied_properties: - property: cogenerator proof: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism from a simple group to a group must be injective, and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' + label: grp_no_cogenerator - property: coregular proof: This is because injective group homomorphisms are not stable under pushouts, see e.g. MSE/601463 or MSE/5088032. @@ -68,6 +73,7 @@ unsatisfied_properties: - property: regular quotient object classifier proof: 'Assume that $\Grp$ has a (regular) quotient object classifier, i.e. a group $P$ such that every surjective homomorphism $G \to H$ is the cokernel of a unique homomorphism $\varphi : P \to G$. Equivalently, every normal subgroup $N \subseteq G$ is $\langle \langle \varphi(P) \rangle \rangle$ for a unique homomorphism $\varphi : P \to G$, where $\langle \langle - \rangle \rangle$ denotes the normal closure. If $c_g : G \to G$ denotes the conjugation with $g \in G$, then the images of $\varphi$ and $c_g \circ \varphi$ have the same normal closures, so the homomorphisms must be equal. In other words, $\varphi$ factors through the center $Z(G)$. But then every normal subgroup of $G$, in particular $G$ itself, would be contained in $Z(G)$, which is wrong for every non-abelian group $G$.' + label: grp_no_regular_quotient_object_classifier - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. @@ -79,6 +85,7 @@ unsatisfied_properties: is injective, but often fails to be surjective because the components of an element in the image have bounded free product length (the number of factors appearing in the reduced form). Specifically, consider the free groups $G = \langle y \rangle$ and $H_n = \langle x_1,\dotsc,x_n \rangle$ for $n \in \IN$ with the truncation maps $H_{n+1} \to H_n$, $x_{n+1} \mapsto 1$. Define $$p_n \coloneqq x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n.$$ If we substitute $x_{n+1}=1$ in $p_{n+1}$, we get $p_n$. Thus, we have $p = (p_n) \in \lim_n (G \sqcup H_n)$. This element does not lie in the image of $\alpha$ since the free product length of $p_n$ (which is well-defined) is $2n$, which is unbounded. + label: grp_no_cocartesian_cofiltered_limits special_objects: initial object: diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index da6d60f2..3837e698 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -27,6 +27,8 @@ satisfied_properties: - property: extremal generator proof: The countable group $\IZ$ is an extremal generator even in $\Grp$. Now use Lemma 10 here. + references: + - grp_extremal_generator - property: finite products proof: This is because $\Grp$ has finite (in fact, all) products, and $\Grp_\c \hookrightarrow \Grp$ is closed under finite products. This is because a finite product of countable sets is again countable. @@ -50,6 +52,8 @@ satisfied_properties: - property: Malcev proof: We can use the same proof as for $\Grp$. + references: + - grp_malcev - property: regular proof: We already know that the category is finitely complete, and that it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. @@ -81,6 +85,8 @@ unsatisfied_properties: - property: regular quotient object classifier proof: We can copy the proof from $\Grp$. + references: + - grp_no_regular_quotient_object_classifier - property: coregular proof: Pushouts of injective homomorphisms between countable groups do not need to be injective, see MSE/5088032. @@ -96,6 +102,8 @@ unsatisfied_properties: For $r \in R$ we define $\varepsilon(r) \in \lim(X)$ by $$\varepsilon(r)_C = \begin{cases} r & r \in C \\ 0 & r \notin C \end{cases}$$ It is easily checked that this indeed lies in the limit. Moreover, $\varepsilon(r) = \varepsilon(r')$ implies $r=r'$, since evaluating at $C \coloneqq \{r\}$ yields $r = r'$. Hence, $\lim(X)$ is uncountable. + references: + - setc_no_aleph1-cofiltered_limits special_objects: initial object: diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 469ae238..328fb032 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -59,18 +59,22 @@ unsatisfied_properties: - property: regular subobject classifier proof: 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]$). + label: haus_no_regular_subobject_classifier - property: cartesian filtered colimits proof: 'It is shown in MSE/1255678 that $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits (so that it cannot be a left adjoint). The same example also works in $\Haus$: Surely $\IQ$ is Hausdorff, $X_n$ is Hausdorff, as is their colimit $X$, and the colimit (taken in $\Top$) of the $X_n \times \IQ$ admits a bijective continuous map to a Hausdorff space, therefore is also Hausdorff, meaning it is also the colimit taken in $\Haus$.' - property: cofiltered-limit-stable epimorphisms - proof: 'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' + proof: 'The following is a basic counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' - property: filtered-colimit-stable monomorphisms proof: |- The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of $$(-\infty, -1/n] \cup [1/n, \infty) \hookrightarrow \IR$$ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \IR$ in the colimit, which is not a monomorphism. + label: haus_no_filtered-colimit-stable_monos + references: + - met_no_filtered_colimit_stable_monos - property: cogenerator proof: 'Assume that $Q$ is a cogenerator. Since $Q$ is Hausdorff, $Q$ is $T_1$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X$ with $\geq 2$ points such that every continuous map $X \to Q$ is constant. (The author only states that $X$ is regular, but actually, $X$ is regular and $T_1$, hence Hausdorff.) But since $Q$ is a cogenerator, this implies that all maps $1 \rightrightarrows X$ are equal, i.e. that $X$ has just one point. This is a contradiction.' @@ -87,6 +91,8 @@ unsatisfied_properties: - property: extremal generating set proof: The proof is the same as the one for $\Top$; there the test spaces we use are of the form $\kappa \sqcup \{ \kappa \}$ and $\kappa + 1$, which are both Hausdorff spaces. + references: + - top_no_extremal_generating_set special_objects: initial object: diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index a52ac054..7b30bedb 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -61,6 +61,8 @@ unsatisfied_properties: - property: co-Malcev proof: 'We can adjust the proof for $\Top$ (see MO/509548) as follows: Let $K$ be a residue field of $R$, let $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.' + references: + - top_not_co-malcev - property: generating set proof: >- diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index dc724e40..d7ef4356 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -43,9 +43,12 @@ satisfied_properties: proof: |- Let $p : X + X \twoheadrightarrow E$ be a cocongruence with coreflexivity morphism $r : E \to X$, so that $r \circ p : X + X \to X$ is the codiagonal. Since $p$ is an epimorphism, it has dense image (see below). We first claim that in fact $p$ also has closed image and therefore is surjective. Because $r \circ (p \circ i_1) : X \to X$ is the identity, the image of $p \circ i_1$ is the equalizer of $\id_E$ and $(p \circ i_1) \circ r$, hence closed. Likewise, the image of $p \circ i_2$ is closed. Thus, the image of $p$, which is the union of these images, is closed. Now, since the pushforward maps of tangent spaces compose to the identity, we see that $p$ must be a local immersion and $r$ must be a submersion. Also, since the fibers of $r$ have one or two points each, we see that the dimension of $E$ must locally be the same as the dimension of $X$. This implies that in fact $p$ and $r$ are local diffeomorphisms. Therefore, the cardinality of the fiber of $r$ is locally constant. Thus, if $U$ is the subset of $X$ where $r$ has fiber of a single point, with the subspace topology, then $U$ is a clopen submanifold of $X$ which serves as the equalizer of $p \circ i_1$ and $p \circ i_2$. + label: man_coquotients_congruences - property: effective cocongruences proof: 'From the proof that $\Man$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.' + references: + - man_coquotients_congruences - property: extremal generator proof: >- @@ -94,6 +97,8 @@ unsatisfied_properties: Assume that there exists a limit cone $(\pi_C : M \to C \sqcup \{\ast\})$ in $\Man$. Since the forgetful functor $\Man \to \Set$ is representable, it preserves limits. In particular, the underlying set of $M$ is the limit of the underlying sets and is therefore uncountable. Since the codomain of $\pi_C$ is discrete, the map $\pi_C$ is locally constant. Thus, for every connected component $K \subseteq M$, the map $\pi_C$ is constant on $K$. Since the maps $\pi_C$ are jointly injective, it follows that every connected component of $M$ consists of a single point. Hence, $M$ is totally disconnected. Since $M$ is a smooth manifold, it follows that $M$ has dimension $0$. Since $M$ is also second-countable, it follows that the underlying set of $M$ is countable, contradicting our previous observation. + references: + - setc_no_aleph1-cofiltered_limits - property: quotients of congruences proof: 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/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index a6677367..e5ca2c5d 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -46,6 +46,8 @@ satisfied_properties: is again an embedding. It is certainly injective, since $\Set$ is coregular. More precisely, the underlying set of $Y \sqcup_A X$ can be identified with $Y \sqcup (X \setminus \im(i))$. Now let $T \subseteq Y$ be a measurable subset. Then its preimage $f^*(T) \subseteq A$ is measurable. Since $i$ is an embedding, there exists a measurable subset $S \subseteq X$ such that $i^*(S) = f^*(T)$. Let $u : X \to Y \sqcup_A X$ denote the canonical map, so that $u \circ i = j \circ f$, and consider the subset $$M := j_*(T) \cup u_*(S \setminus \im(i))$$ of the pushout. It is straightforward to verify that $j^*(M) = T$ and $u^*(M) = S$. Since both $T$ and $S$ are measurable, it follows that $M$ is measurable. Finally, the equality $j^*(M) = T$ shows that every measurable subset of $Y$ is the preimage of a measurable subset of the pushout. Hence $j$ is an embedding, as claimed. + references: + - top_coregular - property: countably extensive proof: >- @@ -68,6 +70,8 @@ satisfied_properties: Now, we claim that adding the two-element set $2$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating set. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that $f \circ {-} : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $2$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $2$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces. Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$. + references: + - set_extremal_cogenerator - property: co-Malcev proof: >- @@ -118,6 +122,8 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' + references: + - top_no_effective_cocongruences - property: regular proof: A proof can be found here. @@ -131,6 +137,8 @@ unsatisfied_properties: which is not an isomorphism, induces a bijection $$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$ for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. + references: + - top_no_extremal_generating_set - property: infinitary distributive proof: >- @@ -146,6 +154,8 @@ unsatisfied_properties: - property: coaccessible proof: 'The proof is very similar to the proof for $\Top$. Assume $\Meas$ is coaccessible. Let $p : D \to I$ be the identity map from the two-element discrete space to the two-element indiscrete space. Then, a measurable space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete measurable 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.' + references: + - top_not_coaccessible special_objects: initial object: diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 6c6e548a..8120e40b 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -48,6 +48,7 @@ satisfied_properties: We already saw that filtered colimits and finite products exist. The canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is an isomorphism for filtered diagrams $(Y_i)$: It is surjective by the concrete description of filtered colimits. It is isometric because of the elementary observation $$\textstyle\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$$ for $r, s_i \in \IR$, where $i \leq j \implies s_i \geq s_j$. + label: met_cartesian_filtered_colimits - property: ℵ₁-cofiltered limits proof: >- @@ -55,6 +56,7 @@ satisfied_properties: Suppose otherwise. Then for every $n \in \IN$ there exists an object $i_n \in \I$ such that $d(x_{i_n},y_{i_n}) \geq n$. Since $\I$ is $\aleph_1$-cofiltered, there exists a cone $(j \to i_n)_{n \in \IN}$. Since the maps $D(j) \to D(i_n)$ are non-expansive, we have $$d(x_j,y_j) \geq d(x_{i_n},y_{i_n}) \geq n$$ for every $n \in \IN$. This is impossible since the metric on $D(j)$ takes only finite values. + label: met_aleph1_cofiltered_limits - property: well-copowered proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' @@ -74,6 +76,7 @@ satisfied_properties: & \le d(x_1, x_2). \end{align*}$$ This shows that $f$ is isometric. + label: met_extremal_generator - property: extremal cogenerator proof: >- @@ -97,6 +100,7 @@ satisfied_properties: Note: $\IR$ is not an extremal cogenerator. This is because for example the non-isomorphism $(0, 1) \hookrightarrow [0, 1]$ induces a bijection $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$. To see this, suppose we have a non-expansive map $f : (0, 1) \to \IR$. Then since $f$ is uniformly continuous in particular, it is well known that $\lim_{x\to 0^+} f(x)$ and $\lim_{x\to 1^-} f(x)$ both exist and are finite. If we extend $f$ with these values at 0 and 1 respectively, then it is straightforward to check that the resulting function is still non-expansive. This shows that $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is surjective; and since $(0, 1) \hookrightarrow [0, 1]$ is an epimorphism, $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is also injective. (The same proof also shows that $\IR_{\ge 0}$ is not an extremal cogenerator.) + label: met_extremal_cogenerator - property: ℵ₁-accessible proof: >- @@ -108,6 +112,7 @@ satisfied_properties: Then, countable metric spaces in $\Met$ are $\aleph_1$-presentable not only in $\Met_\infty$, but also in $\Met$. On the other hand, every object in $\Met_\infty$ is an $\aleph_1$-filtered colimit of its countable isometric subspaces, and the same is true in $\Met$. Hence, $\Met$ is $\aleph_1$-accessible. + unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -140,6 +145,7 @@ unsatisfied_properties: proof: >- The following example is taken from Rem. 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_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. + label: met_no_filtered_colimit_stable_monos - property: natural numbers object proof: >- @@ -158,9 +164,12 @@ unsatisfied_properties: $$d(f(x), h(y)) \le d(f(x), g(\varepsilon)) + d(g(\varepsilon), h(y)) \le (x + \varepsilon) + (y + \varepsilon).$$ Since this holds for every $\varepsilon > 0$, we conclude $d(f(x), h(y)) \le x+y$. On the other hand, if this cocongruence were effective, then by the dual of this result, it would be the cokernel pair of the equalizer of the two inclusion maps. However, that equalizer is empty, so $E$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$. + label: met_no_effective_cocongruences - property: regular proof: We can take the same counterexample as for $\PMet$. + references: + - pmet_not_regular special_objects: initial object: diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index eddcfa80..31301903 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -83,6 +83,8 @@ unsatisfied_properties: - property: regular subobject classifier proof: '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]$).' + references: + - haus_no_regular_subobject_classifier - property: sequential colimits proof: See MO/510316 for a proof that the diagram $\IN \to \Met_c$, $n \mapsto \IR^n$ does not have a colimit. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index 10a7611a..7367cbd3 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -25,15 +25,21 @@ satisfied_properties: - property: cartesian filtered colimits proof: 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\}$. + references: + - met_cartesian_filtered_colimits - property: infinitary extensive proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets equipped with the metric that extends the given metrics and assigns distance $\infty$ to points in different summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique metric, it follows immediately that coproducts are disjoint in $\Met_\infty$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of metric spaces and let $f : T \to \coprod_{i \in I} X_i$ be a non-expansive map. Consider the pullbacks $T_i := f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the metric induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical non-expansive map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is isometric. Since each $T_i \to T$ is isometric, it suffices to prove that for $a \in T_i$ and $b \in T_j$, where $i \neq j$, we have $d_T(a,b) = \infty$. Indeed, since $f(a) \in X_i$ and $f(b) \in X_j$, we have $\infty = d_{\coprod_i X_i}(f(a),f(b)) \leq d_T(a,b)$.' - property: extremal generator proof: A similar proof to the one for $\Met$ shows that $[0, \infty]$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\Met_{\infty}$. + references: + - met_extremal_generator - property: extremal cogenerator proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric extending the usual metric on $\IR_+$ by defining $d(a,\infty) \coloneqq \infty$ for $a \in \IR_+$. Then one checks that the maps $1 + d(a,{-}) : X \to \IR_+ \cup \{\infty\}$ (assigning the value $\infty$ if $d(a,x) = \infty$) are non-expansive and finishes as for $\Met$.' + references: + - met_extremal_cogenerator unsatisfied_properties: - property: skeletal @@ -53,15 +59,21 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: We can copy the proof from $\Met$. + references: + - met_no_filtered_colimit_stable_monos - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Met_{\infty}$ that equips a set with the discrete topology. - property: effective cocongruences proof: 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)$. + references: + - met_no_effective_cocongruences - property: regular proof: We can take the same counterexample as for $\PMet$. + references: + - pmet_not_regular special_objects: initial object: diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index c5d730c8..d6b61c38 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -54,18 +54,24 @@ unsatisfied_properties: - property: coregular proof: 'Consider the monoid $M \coloneqq \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not stable under pushouts. Consider $N \coloneqq \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' + label: mon_not_coregular - property: regular subobject classifier proof: '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$.' + label: mon_no_regular_subobject_classifier - property: regular quotient object classifier proof: We can just copy the proof for $\CMon$. Alternatively, we may use Lemma 1 here (dualized) applied to the forgetful functor $\CMon \to \Mon$. + references: + - cmon_no_regular_quotient_object_classifier - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. - property: cocartesian cofiltered limits proof: '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.' + references: + - grp_no_cocartesian_cofiltered_limits - property: effective cocongruences proof: >- @@ -75,6 +81,7 @@ unsatisfied_properties: On the other hand, using the multiplicative map $$E \to M_{2\times 2}(\IZ), \quad p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},\quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix},$$ we can see that $p \ne q$ in $E$, so the equalizer of the two maps $X \rightrightarrows E$ is the trivial submonoid $\{ 1 \}$. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$. + label: mon_no_effective_cocongruences special_objects: initial object: diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 2045bdaf..772327f0 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -52,6 +52,8 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: The proof is identical to the one for $\Met$. + references: + - met_aleph1_cofiltered_limits - property: extremal generator proof: >- @@ -68,6 +70,8 @@ satisfied_properties: & \le d(x_1, x_2). \end{align*}$$ This shows that $f$ is isometric. + references: + - met_extremal_generator - property: extremal cogenerator proof: >- @@ -77,7 +81,9 @@ satisfied_properties: To see $Q$ is in fact an extremal cogenerator, suppose we have a non-expansive map $f : X \to Y$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection. First of all, any function $Y \to Q$ which factors through $\{ 0, 0' \}$ is automatically non-expansive; and the injectivity of $f^*$ on such maps implies that $f$ is surjective on underlying sets, since $\{ 0, 0' \}$ is a cogenerator of $\Set$. From this, we can conclude that $f^*$ in fact induces a bijection on the functions $Y\to Q$ and $X\to Q$, respectively, which factor through $\{ 0, 0' \}$. Since $\{ 0, 0' \}$ is in fact an extremal cogenerator of $\Set$, we conclude that in fact, $f$ is a bijection on underlying sets. - From here, the proof that $f$ is isometric is similar to the one for $\Met$, using the fact that $d(x, {-}) : X \to \IR_{\ge 0} \hookrightarrow Q$ induces a non-expansive map $Y \to Q$. + From here, the proof that $f$ is isometric is similar to the one for $\Met$, using the fact that $d(x, {-}) : X \to \IR_{\ge 0} \hookrightarrow Q$ induces a non-expansive map $Y \to Q$. + references: + - met_extremal_cogenerator unsatisfied_properties: - property: skeletal @@ -115,9 +121,12 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$, which does not exist.' + references: + - top_no_effective_cocongruences - property: regular proof: 'We can adapt Example 3.14 at the nLab (which disproves regularity for $\Pos$ and related categories) as follows: Consider the subspaces $X = \{0,1,2,3\}$ and $Y = \{0,1,2\}$ of $\IR$ with the usual metric. Define a surjective map $p : X \to Y$ by $p(0)=0$, $p(1)=p(2)=1$, and $p(3)=2$. Clearly, $p$ is non-expansive. Moreover, one can check that $p$ satisfies the universal property in $\PMet$ of a coequalizer of the two maps $1,2 : \{\ast\} \rightrightarrows X$. Thus, $p$ is a regular epimorphism. Now consider the subspace $Z = \{0,2\}$ of $Y$. As a set, the pullback $X \times_Y Z$ is $p^*(Z) = \{0,3\}$. Using the definition of the product metric, one can verify that $d(0,3) = 3$ in this pullback. The projection $X \times_Y Z \to Z$ identifies with the evident bijective and non-expansive map $\{0,3\} \to \{0,2\}$. It is a monomorphism and not an isomorphism (the distances do not match), hence cannot be a regular epimorphism.' + label: pmet_not_regular special_objects: initial object: diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index 90fe7af4..8353be37 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -20,6 +20,7 @@ satisfied_properties: - property: locally finitely presentable proof: See Adamek-Rosicky, Example 1.10. + label: pos_lfp - property: cartesian closed proof: For posets $P,Q$ we endow $\Hom(P,Q)$ with the partial order in which $f \leq g$ holds iff $f(p) \leq g(p)$ for all $p \in P$. The universal evaluation map is $\Hom(P,Q) \times P \to Q$, $(f,p) \mapsto f(p)$, it is order-preserving, and it satisfies the universal property. @@ -35,12 +36,15 @@ satisfied_properties: - property: extremal generator proof: We have that $\{0<1\}$ is an extremal generator even in $\PreOrd$. Now apply Lemma 10 here. + references: + - preord_extremal_generator - property: extremal cogenerator proof: >- We prove that the poset $\{0 < 1\}$ is an extremal cogenerator. First, to prove it 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$. Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that $f$ induces a bijection of upper sets implies that $f$ is also injective on the underlying sets, and also that $f(a_1) \le f(a_2)$ implies $a_1 \le a_2$. Therefore, $f$ is an isomorphism. + label: pos_extremal_cogenerator unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index aed4b6f0..03b9a73b 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -20,6 +20,8 @@ satisfied_properties: - property: locally finitely presentable proof: The same proof as for $\Pos$ works, cf. Adamek-Rosicky, Example 1.10. + references: + - pos_lfp - property: cartesian closed proof: For preordered sets $P,Q$ we endow $\Hom(P,Q)$ with the preorder in which $f \leq g$ holds iff $f(p) \leq g(p)$ for all $p \in P$. The universal evaluation map is $\Hom(P,Q) \times P \to Q$, $(f,p) \mapsto f(p)$, it is order-preserving, and it satisfies the universal property. @@ -38,6 +40,7 @@ satisfied_properties: - property: extremal generator proof: 'We claim that $\{ 0 < 1 \}$ is an extremal generator. First, the singleton preordered set $1$ is a generator, since it represents the forgetful functor $\PreOrd \to \Set$ which is faithful. Since we have an epimorphism $\{ 0 < 1 \} \to 1$, it follows that $\{ 0 < 1 \}$ is also a generator. Now, suppose we have a morphism $f : P \to Q$ such that $f \circ {-} : \Hom(\{0<1\}, P) \to \Hom(\{0<1\}, Q)$ is a bijection. Then considering constant functions, we can see that $f$ must be a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then that induces a morphism $\{0,1\} \to Q$ with $0 \mapsto f(p_1), 1 \mapsto f(p_2)$. The corresponding morphism $\{0<1\}\to P$ must send $0\mapsto p_1, 1 \mapsto p_2$, showing that $p_1 \le p_2$. It follows that $f$ is an isomorphism.' + label: preord_extremal_generator - property: extremal cogenerator proof: >- diff --git a/database/data/categories/Ring.yaml b/database/data/categories/Ring.yaml index 3e074365..7da17e06 100644 --- a/database/data/categories/Ring.yaml +++ b/database/data/categories/Ring.yaml @@ -29,16 +29,20 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + references: + - grp_malcev - property: disjoint finite products proof: '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$.' + label: ring_disjoint_finite_products unsatisfied_properties: - property: skeletal proof: This is trivial. - property: balanced - proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. + proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample; see also here. + label: ring_not_balanced - property: semi-strongly connected proof: This is because already the full subcategory $\CRing$ does not have this property. @@ -54,9 +58,12 @@ unsatisfied_properties: - property: coregular proof: 'Let $B \coloneqq M_2(\IQ)$ and $A \coloneqq \IQ^2$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & 2 \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' + label: ring_not_coregular - property: regular quotient object classifier proof: 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 Lemma 1 here (dualized). + references: + - cring_no_regular_quotient_object_classifier - property: cocartesian cofiltered limits proof: >- @@ -69,6 +76,7 @@ unsatisfied_properties: - property: effective cocongruences proof: See MO/510744. + label: ring_no_effective_cocongruences special_objects: initial object: diff --git a/database/data/categories/Rng.yaml b/database/data/categories/Rng.yaml index 502efbe1..f27986ca 100644 --- a/database/data/categories/Rng.yaml +++ b/database/data/categories/Rng.yaml @@ -29,13 +29,17 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + references: + - grp_malcev unsatisfied_properties: - property: skeletal proof: This is trivial. - property: balanced - proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. (The proof can be reduced to the unital case.) + proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample; the proof can be reduced to the unital case. + references: + - ring_not_balanced - property: cogenerator proof: 'We apply this lemma to the collection of fields: Any non-zero rng homomorphism from a field to a rng must be injective, and for every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$.' @@ -58,6 +62,8 @@ unsatisfied_properties: - property: coregular proof: '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.' + references: + - ring_not_coregular - property: regular quotient object classifier proof: '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 Lemma 1 here (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).' @@ -80,6 +86,8 @@ unsatisfied_properties: 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$. + references: + - ring_no_effective_cocongruences special_objects: initial object: diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index d7c90468..022420ac 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -54,13 +54,15 @@ unsatisfied_properties: Let us first remark that every non-empty finite semigroup $A$ has an idempotent element $e$, and then $B \to A$, $x \mapsto e$ does define a semigroup homomorphism for any $B$. Therefore, counterexamples need to be infinite and also without idempotent elements. Let $A$ be the set of positive rational numbers of the form $m/2^n$ (with $m > 0$, $n \geq 0$), and let $B$ be the set of positive rational numbers of the form $m/3^n$ (with $m > 0$, $n \geq 0$). Both are semigroups under addition. The element $1 \in A$ is $2^\infty$-divisible, meaning that for every $n \geq 0$ there is some $a \in A$ with $1 = 2^n \cdot a$. But $B$ has no $2^\infty$-divisible element. Hence, there is no semigroup homomorphism $A \to B$. Likewise, there is no semigroup homomorphism $B \to A$. - - property: cogenerating set + - property: cogenerator # TODO: find a variant of the lemma missing_cogenerating_sets # (or missing_cogenerator) which handles this. proof: >- - The proof is similar to the proof for $\Grp$. Assume that there is a cogenerating set $S$. There is an infinite simple group $G$ larger than all the semigroups in $S$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a semigroup $H \in S$ and a homomorphism of semigroups $f : G \to H$ with $f \neq f \circ 1$. Then + The proof is similar to the proof for $\Grp$. Assume that there is a cogenerator $Q$. There is an infinite simple group $G$ larger than $Q$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a homomorphism of semigroups $f : G \to Q$ with $f \neq f \circ 1$. Then $$N \coloneqq \{g \in G : f(g) = f(1)\}$$ is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction. + references: + - grp_no_cogenerator - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. @@ -70,6 +72,8 @@ unsatisfied_properties: The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$ whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$. + references: + - mon_no_effective_cocongruences - property: natural numbers object proof: >- @@ -95,6 +99,8 @@ unsatisfied_properties: There is a canonical homomorphism $\iota : F \to M$, which is the equalizer of the two canonical homomorphisms $M \rightrightarrows N$ defined by $s \mapsto s_i$. We define $F \to K$ by $a \mapsto x$, $b \mapsto x$, $c \mapsto c$, $d \mapsto d$. Then $$K \sqcup_F M \cong \langle x,c,d,s : x s = c,\, x s = d \rangle$$ shows that $c,d \in K$ have the same image in the pushout. + references: + - mon_not_coregular - property: regular subobject classifier proof: 'Assume that a regular subobject classifier $\Omega$ exists in $\SemiGrp$. The universal regular monomorphism $\top : 1 \to \Omega$ corresponds to an idempotent element $e \in \Omega$. It follows that $e \Omega e$ is a monoid with neutral element $e$. We claim that it is a regular subobject classifier in $\Mon$, which we know does not exist. Indeed, let $\iota : A \to B$ be a regular monomorphism of monoids. Since the forgetful functor $\Mon \to \SemiGrp$ preserves limits, we can also see $\iota$ as a regular monomorphism of semigroups. Hence, there is a unique homomorphism of semigroups $f : B \to \Omega$ with $\iota(A) = \{b \in B : f(b) = e\}$. Since $1 \in \iota(A)$, we have $f(1) = e$. Then $f$ corresponds to a homomorphism of monoids $f : B \to e \Omega e$ with kernel $\iota$, which proves our claim.' diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 1368ab0c..59e7c067 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -35,10 +35,12 @@ satisfied_properties: - property: extremal generator proof: The one-point set is an extremal generator since it represents the identity functor $\id_{\Set}$ which is certainly faithful and conservative. check_redundancy: false + label: set_extremal_generator - property: extremal cogenerator proof: The two-point set is an extremal cogenerator since it represents the contravariant power set functor $\Set^{\op} \to \Set$ which is faithful and conservative (see contravariant power set functor). check_redundancy: false + label: set_extremal_cogenerator unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index 51cac78e..4dfc07bc 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -34,9 +34,13 @@ satisfied_properties: - property: extremal generator proof: The one-point set is an extremal generator even in $\Set$. Now apply Lemma 10 here. + references: + - set_extremal_generator - property: extremal cogenerator proof: The two-point set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. + references: + - set_extremal_cogenerator - property: semi-strongly connected proof: This is because the larger category $\Set$ has this property. @@ -74,6 +78,7 @@ unsatisfied_properties: For $r \in R$ we define $\varepsilon(r) \in \lim(X)$ by $$\varepsilon(r)_C = \begin{cases} r & r \in C \\ \ast & r \notin C \end{cases}$$ It is easily checked that this indeed lies in the limit. Moreover, $\varepsilon(r) = \varepsilon(r')$ implies $r=r'$, since evaluating at $C \coloneqq \{r\}$ yields $r = r'$. Hence, $\lim(X)$ is uncountable. + label: setc_no_aleph1-cofiltered_limits special_objects: initial object: diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index 3163cb59..24c936e3 100644 --- a/database/data/categories/Set_ff.yaml +++ b/database/data/categories/Set_ff.yaml @@ -44,9 +44,12 @@ satisfied_properties: - property: quotients of congruences proof: 'A congruence on a set $X$ in $\Set_\ff$ 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_\ff$.' + label: set_ff_quotients_congruences - property: effective congruences proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\ff$. From the proof on quotients of congruences in $\Set_\ff$, we have a quotient map $p : X \to X/E$ in $\Set_\ff$, 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_\ff$. 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.' + references: + - set_ff_quotients_congruences - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_\ff$. 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_\ff$ 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.' @@ -56,6 +59,8 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: 'We derive this from the fact that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$. Let $D : \I \to \Set_\ff$ be an $\aleph_1$-cofiltered diagram. Let $(p_i : L \to D(i))_{i \in \I}$ be the limit cone in $\Set$. Each $p_i$ is finite-to-one, because the fiber over $d \in D(i)$ is the limit of the $\aleph_1$-cofiltered diagram $\tilde{D} : I/i \to \FinSet$ which maps $j \to i$ to $D(j \to i)^*(\{d\})$. To verify the universal property, let $(f_i : T \to D(i))_{i \in \I}$ be a cone in $\Set_\ff$. There is a unique map $f : T \to L$ such that $p_i f = f_i$ for every $i \in \I$, and it remains to prove that $f$ is finite-to-one. Choose any $i \in \I$. Then for every $x \in L$ we have $f^*(\{x\}) \subseteq f_i^*(\{p_i(x)\})$, and the latter set is finite.' + references: + - finset_aleph1-cofiltered-limits unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Set_pointed.yaml b/database/data/categories/Set_pointed.yaml index ee2c327e..c7f8a07a 100644 --- a/database/data/categories/Set_pointed.yaml +++ b/database/data/categories/Set_pointed.yaml @@ -30,6 +30,7 @@ satisfied_properties: - property: cogenerator proof: The pointed set $(\{0,1\},1)$ is a cogenerator. + label: set_*_cogenerator - property: coregular proof: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for $\Set$ and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts. @@ -43,6 +44,7 @@ satisfied_properties: Let $X$ be a pointed set and $(Y_i)$ be a filtered diagram of pointed sets. Base points will be denoted by $0$. The canonical map $X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$ is injective since the wedge sum naturally embeds into the product and the natural map $X \vee \prod_i Y_i \to \prod_i (X \times Y_i)$ is injective. Now let $z = (z_i) \in \lim_i (X \vee Y_i)$. Case 1: There is some index $i$ with $z_i \in X \setminus \{0\}$. We claim $z_j \in X$ for any index $j$ and $z_j = z_i$ in $X$, so that $z$ has a preimage in $X$. To see this, choose an index $k \geq i,j$. Since $X \vee Y_i \to X \vee Y_k$ maps $z_i \mapsto z_k$ and is the identity on $X$, we see that $z_k \in X$ and $z_k = z_i$ in $X$. Since $X \vee Y_j \to X \vee Y_k$ maps $z_j \mapsto z_k$, we see that $z_j \notin Y_j$, since otherwise $z_k \in Y_k \cap X = \{0\}$. Hence, $z_j \in X \setminus \{0\}$, and then $z_j = z_k = z_i$. Case 2: We have $z_i \in Y_i$ for all $i$. Then clearly $(z_i) \in \lim_i Y_i$ is a preimage. + label: set_*_cocartesian_cofiltered_limits - property: CIP proof: The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index. @@ -63,6 +65,7 @@ unsatisfied_properties: - property: conormal proof: '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$.' + label: set_*_not_conormal - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Set_*$ that freely adds a base point. diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 3d88de7a..612b6a9b 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -19,24 +19,28 @@ satisfied_properties: - property: extremal generator proof: The one-point set is an extremal generator even in $\Set$. Now use Lemma 10 here. check_redundancy: false + references: + - set_extremal_generator - property: extremal cogenerator proof: The two-point set is an extremal cogenerator even in $\Set$. Now use Lemma 10 here. + references: + - set_extremal_cogenerator - property: products proof: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. - property: cartesian closed - proof: This follows as for $\Set$, since for non-empty sets $X,Y$ there is at least one function $X \to Y$. + proof: This is because $\Set$ is cartesian closed and since for non-empty sets $X,Y$ there is at least one function $X \to Y$. - property: binary coproducts proof: The disjoint union of two non-empty sets is non-empty. - property: mono-regular - proof: This follows as for $\Set$. + proof: This follows easily from the fact that $\Set$ is mono-regular. - property: epi-regular - proof: This follows as for $\Set$. + proof: This follows easily from the fact that $\Set$ is epi-regular. - property: strongly connected proof: Use constant maps. @@ -76,7 +80,7 @@ unsatisfied_properties: proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square. - property: coaccessible - proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in loc. cit.). + proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in op. cit.). special_objects: terminal object: diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml index 56aa819f..1ddd9e40 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -25,10 +25,12 @@ satisfied_properties: proof: '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)$.' - property: ℵ₁-accessible - proof: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible. + proof: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable; see here. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible. - property: ℵ₁-cofiltered limits proof: Since $\FinSet$ has $\aleph_1$-cofiltered limits, also $\Sigma_n{-}\FinSet$ has $\aleph_1$-cofiltered limits for every $n \geq 0$. Hence, $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ has $\aleph_1$-cofiltered limits. + references: + - finset_aleph1-cofiltered-limits unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 59494526..d86852e3 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -49,6 +49,8 @@ satisfied_properties: Using the dual of Lemma 9 here with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of $\Set$, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective. Now, by this result, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$. + references: + - set_extremal_cogenerator - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -58,6 +60,7 @@ satisfied_properties: - property: coregular proof: The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab. Another proof can be found in MSE/2016945. + label: top_coregular unsatisfied_properties: - property: skeletal @@ -78,18 +81,22 @@ unsatisfied_properties: - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' + label: top_not_coaccessible - property: co-Malcev proof: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' + label: top_not_co-malcev - property: effective cocongruences proof: '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.' + label: top_no_effective_cocongruences - property: extremal generating set proof: >- Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating set. To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $T := \im(f) \cap \kappa$. Then $T \subseteq \kappa$ and $\card(T) \leq \card(G) < \kappa$. Since $\kappa$ is regular, this implies $\alpha := \sup(T) < \kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$. + label: top_no_extremal_generating_set special_objects: initial object: diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index 92efe3b0..30afa0aa 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -56,6 +56,8 @@ satisfied_properties: We continue the proof for $\Set_*$ by showing that the natural bijective map $$\textstyle \alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$$ is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^*(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^*(V_i) \cap \lim_i Y_i)$ is $p_i^*(X \vee V_i)$, hence open. + references: + - set_*_cocartesian_cofiltered_limits - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. @@ -68,6 +70,8 @@ satisfied_properties: It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator, using the fact that the pointed set $\{0,1\}$ with base point $1$ is a cogenerator of $\Set_*$. If $S$ is the Sierpinski space on $\{0,1\}$, we claim that adding $(S, 0)$ and $(S, 1)$ gives an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. Then $f$ inducing a bijection on maps to $(\{0,1\},1)$ implies that the underlying function of $f$ is bijective. In particular, because $f$ is injective, we see that for $V$ an open subset of $Y$, $f^*(V)$ contains the base point of $X$ if and only if $V$ contains the base point of $Y$. Also, $f$ inducing a bijection on maps to $(S, 1)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets containing the base points, and $f$ inducing a bijection on maps to $(S, 0)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets not containing the base points. From these observations, we can conclude that $f$ is a homeomorphism. Now, by this result, we get that the product of these three pointed topological spaces is an extremal cogenerator of $\Top_*$. + references: + - set_*_cogenerator unsatisfied_properties: - property: skeletal @@ -81,6 +85,8 @@ unsatisfied_properties: - property: co-Malcev proof: 'We can adjust the proof for $\Top$ as follows: Consider the forgetful functor $U : \Top_* \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the discrete space $\{0,1\}$ with base point $0$ and $R$ by the Sierpinski space with an isolated base point added. It is clear that $R$ is reflexive, but not symmetric.' + references: + - top_not_co-malcev - property: unital proof: '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.' @@ -91,9 +97,13 @@ unsatisfied_properties: - property: regular quotient object classifier proof: 'If there were a regular quotient object classifier, every regular epimorphism would be a cokernel. By considering discrete spaces, it would follow that every surjective pointed map between pointed sets is a cokernel, i.e. that $\Set_*$ is conormal. But we already know that this is not the case, since cokernels are "injective away from the base point".' + references: + - set_*_not_conormal - property: coaccessible proof: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' + references: + - top_not_coaccessible - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. @@ -103,9 +113,13 @@ unsatisfied_properties: - property: effective cocongruences proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' + references: + - top_no_effective_cocongruences - property: extremal generating set proof: 'The proof is similar to the one for $\Top$: if $S$ is a set of pointed topological spaces and $\kappa$ is an infinite regular cardinal greater than $\card(G)$ for every $G\in S$, we show as before that morphisms from $S$ cannot detect the failure of $(\kappa \sqcup \{ \kappa \}, 0) \to (\kappa + 1, 0)$ to be an isomorphism (where as before, we use the standard order topology on both $\kappa$ and $\kappa + 1$).' + references: + - top_no_extremal_generating_set special_objects: initial object: diff --git a/database/data/categories/TorsAb.yaml b/database/data/categories/TorsAb.yaml index a2ce9462..f65fcd95 100644 --- a/database/data/categories/TorsAb.yaml +++ b/database/data/categories/TorsAb.yaml @@ -31,9 +31,13 @@ satisfied_properties: - property: normal proof: '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$.' + references: + - ab_abelian - property: conormal proof: '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$.' + references: + - ab_abelian - property: finitely accessible proof: 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/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 3e90d4fb..56130f69 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -25,6 +25,7 @@ satisfied_properties: - property: cocomplete proof: '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 + label: torsfreeab_cocomplete - property: finitely accessible proof: 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$. diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 89b64dcc..8e71730d 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -40,6 +40,8 @@ satisfied_properties: - property: cogenerator proof: The indiscrete (aka trivial) uniform space $\{0,1\}$ (i.e. $\{0,1\} \times \{0,1\}$ is the only entourage) is a cogenerator because every map into $\{0,1\}$ is automatically uniform and because $\{0,1\}$ is a cogenerator in $\Set$. + references: + - set_extremal_cogenerator - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -115,6 +117,8 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The proof is very similar to $\Top$. Consider the indiscrete uniform space $I$ on two points whose only entourage is $I \times I$. This represents the functor which maps a uniform space $X$ to the set of pairs of points $(x,y) \in X$ that are indistinguishable, i.e. every entourage of $X$ contains $(x,y)$. This is an equivalence relation on $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: If a uniform map $h : Z \to 1$ equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete uniform space on two points.' + references: + - top_no_effective_cocongruences - property: natural numbers object proof: >- @@ -133,6 +137,8 @@ unsatisfied_properties: is uniform, but not a uniform isomorphism (not even a topological isomorphism). However, we claim that for every $G \in S$ the induced map $$\Hom(G,\kappa \sqcup \{\kappa\}) \to \Hom(G,\kappa + 1),$$ which is clearly injective, is even bijective. To this end, let $f : G \to \kappa + 1$ be a uniform map. Since $\card(G) < \kappa$ and $\kappa$ is regular, $\im(f) \cap \kappa$ is bounded above by some ordinal $\alpha < \kappa$. Therefore, $f$ factors through the uniform subspace $X := [0,\alpha] \cup \{\kappa\}$ of $\kappa + 1$. The underlying topological space of $X$ is compact Hausdorff and decomposes as a coproduct of $[0,\alpha]$ and $\{\kappa\}$. Because of the uniqueness of uniform structures, $X$ itself also decomposes as a coproduct of these spaces. In particular, $X$ is a uniform subspace of $\kappa \sqcup \{\kappa\}$. Hence, $f : G \to \kappa \sqcup \{\kappa\}$ is also a uniform map. + references: + - top_no_extremal_generating_set - property: extremal cogenerating set proof: >- diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index d043f0ec..ff2e0869 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -31,6 +31,7 @@ satisfied_properties: - property: extremal generator proof: The one-dimensional vector space $K$ is an extremal generator since it represents the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. check_redundancy: false + label: vect_extremal_generator - property: extremal cogenerator proof: 'The one-dimensional vector space $K$ is an extremal cogenerator. To show this, using this result, since $\Vect_K$ is balanced, it suffices to show that $K$ is a cogenerator. For this, suppose we have two unequal vectors $x, y \in V$. Then $x - y \ne 0$, so there exists a functional $\varphi : V \to K$ such that $\varphi(x - y) \ne 0$. It follows that $\varphi(x) \ne \varphi(y)$.' diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index 81cac005..7af46d84 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -54,6 +54,8 @@ unsatisfied_properties: - property: semi-strongly connected proof: 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,-)$. + references: + - cring_no_semi_strongly_connected - property: locally essentially small proof: See MO/390611 for example. diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index a652f7c0..777f7be3 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -31,12 +31,18 @@ satisfied_properties: - property: terminal object proof: The object $[0]$ is terminal since it is already terminal in $\Delta$. + references: + - delta_terminal_object - property: extremal generator proof: The object $[1]$ is an extremal generator even in $\Delta$; now use Lemma 10 here. A direct proof is also possible. + references: + - delta_extremal_generator - property: extremal cogenerator proof: The object $[1]$ is an extremal cogenerator even in $\Delta$; now use Lemma 10 here. A direct proof is also possible. + references: + - delta_extremal_cogenerator - property: epi-regular proof: 'The only non-identity epimorphism is $p$, which is the coequalizer of $\id, ip : [1] \rightrightarrows [1]$ (since $pi = \id$).' @@ -46,9 +52,13 @@ satisfied_properties: - property: coequalizers proof: '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.' + references: + - delta_coequalizers - property: cosifted - proof: 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. + proof: Our proof that the simplex category is cosifted has only used $[0],[1]$ as auxiliary objects and therefore also shows that $\Delta^{\leq 1}$ is cosifted. + references: + - delta_cosifted - property: generalized variety proof: 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/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml index c11819ef..7dc83505 100644 --- a/database/data/functors/forget_finite.yaml +++ b/database/data/functors/forget_finite.yaml @@ -24,6 +24,8 @@ satisfied_properties: - property: cocontinuous proof: This follows from Lemma 1 here since $\Set$ has an extremal cogenerator $\{0,1\}$ which is contained in $\FinSet$. + references: + - set_extremal_cogenerator unsatisfied_properties: - property: left-invertible diff --git a/database/data/functors/forget_finite_abelian_group.yaml b/database/data/functors/forget_finite_abelian_group.yaml index 198dadf5..4afaac99 100644 --- a/database/data/functors/forget_finite_abelian_group.yaml +++ b/database/data/functors/forget_finite_abelian_group.yaml @@ -24,6 +24,8 @@ satisfied_properties: - property: preserves products proof: The proof is identical to the proof that the inclusion functor $\FinGrp \hookrightarrow \Grp$ preserves products. + references: + - forget_finite_group_preserves_products - property: preserves coproducts proof: The proof is a minor variation of the proof that products are preserved, using the fact that finite coproducts and finite products coincide. Namely, one can show that a family of finite abelian groups has a coproduct in $\FinAb$ if and only if almost all groups are trivial. @@ -34,9 +36,15 @@ unsatisfied_properties: - property: finitary proof: We can take the same counterexample as for the inclusion functor $\FinGrp \hookrightarrow \Grp$, which only involves abelian groups. + references: + - forget_finite_group_not_finitary - property: cofinitary proof: We can take the same counterexample as for the inclusion functor $\FinGrp \hookrightarrow \Grp$, which only involves abelian groups. + references: + - forget_finite_group_not_cofinitary - property: left-invertible proof: We can use the same proof as for the inclusion functor $\FinGrp \hookrightarrow \Grp$. + references: + - forget_finite_group_not_left-invertible diff --git a/database/data/functors/forget_finite_group.yaml b/database/data/functors/forget_finite_group.yaml index 4c65846b..db634056 100644 --- a/database/data/functors/forget_finite_group.yaml +++ b/database/data/functors/forget_finite_group.yaml @@ -33,6 +33,7 @@ satisfied_properties: Assume that there are infinitely many indices $i_1,i_2,\dotsc$ for which $G_{i_n}$ is non-trivial. Let $N \geq 1$. There is a canonical homomorphism $P \to \prod_{n=1}^{N} G_{i_n}$ to the finite product (which definitely exists), and by using trivial homomorphisms, we see that it is actually a split epimorphism. Therefore, $$\textstyle\card(P) \geq \prod_{i=1}^{N} \card(G_{i_n}) \geq \prod_{i=1}^{N} 2 = 2^N.$$ Since this holds for all $N$, we obtain a contradiction to the finiteness of $P$. + label: forget_finite_group_preserves_products - property: preserves coproducts proof: >- @@ -47,6 +48,7 @@ unsatisfied_properties: - property: left-invertible proof: 'Assume that there is a functor $F : \Grp \to \FinGrp$ with natural isomorphisms $F(G) \cong G$ for finite groups $G$. Consider the group $A := F(\prod_{n \geq 1} \IZ/n)$. For every $n \geq 1$ there is a split monomorphism from $\IZ/n$ to $\prod_{n \geq 1} \IZ/n$. It induces a split monomorphism from $F(\IZ/n) \cong \IZ/n$ to $A$, so that $\card(A) \geq n$. But then $A$ cannot be finite.' + label: forget_finite_group_not_left-invertible - property: finitary proof: >- @@ -55,12 +57,14 @@ unsatisfied_properties: But every homomorphism $Q \to U(G)$ is trivial because its image is a finite divisible abelian group. Thus, $\Hom(Q,U(G)) \cong \Hom(1,G)$, proving that $1$ is a colimit of $D$. This shows that the colimit of $D$ is not preserved by $U$. For example, when $Q = \IQ / \IZ$, the diagram is isomorphic to $(\IN_{>0},\mid)^{\op} \to \FinGrp$, mapping $n$ to the cyclic group $\IZ/n$, and its (trivial) colimit is not preserved by $U$. + label: forget_finite_group_not_finitary - property: cofinitary proof: >- Let $p$ be a prime, and consider the sequence of projection homomorphisms $$\cdots \to \IZ/p^3 \to \IZ/p^2 \to \IZ/p.$$ Its limit in $\Grp$ is the additive group $\IZ_p$ of $p$-adic integers. However, its limit in $\FinGrp$ exists and is the trivial group. This is because a cone in $\FinGrp$ over that sequence with vertex $G \in \FinGrp$ can be identified with a homomorphism $G \to \IZ_p$ in $\Grp$, which must be trivial since its image is a finite torsion-free group. + label: forget_finite_group_not_cofinitary - property: right exact proof: See MO/513646. diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml index cde307a1..5c4a3e61 100644 --- a/database/data/functors/forget_torsion_free.yaml +++ b/database/data/functors/forget_torsion_free.yaml @@ -25,6 +25,8 @@ satisfied_properties: - property: finitary proof: This comes out of the construction of filtered colimits in $\TorsFreeAb$. + references: + - torsfreeab_cocomplete - property: preserves regular epimorphisms proof: In both $\Ab$ and $\TorsFreeAb$, regular epimorphisms are exactly the surjective group homomorphisms. diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index fab1a896..d751a682 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -46,6 +46,7 @@ CREATE TABLE property_assignments ( CHECK (is_deduced in (TRUE, FALSE)), check_redundancy INTEGER NOT NULL DEFAULT TRUE CHECK (check_redundancy in (TRUE, FALSE)), + label TEXT UNIQUE, UNIQUE (structure_id, property_id), FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, @@ -70,4 +71,17 @@ CREATE TABLE property_tag_assignments ( PRIMARY KEY (property_id, type, tag), FOREIGN KEY (property_id, type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (tag, type) REFERENCES property_tags (tag, type) ON DELETE CASCADE +); + +CREATE TABLE proof_references ( + structure_id TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + reference TEXT NOT NULL, + PRIMARY KEY (structure_id, property_id), + FOREIGN KEY (structure_id, type) + REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE, + FOREIGN KEY (reference) REFERENCES property_assignments (label) ON DELETE CASCADE ); \ No newline at end of file diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 23cd445b..bba87c08 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -221,8 +221,15 @@ function seed_structures({ const property_assignment_insert = db.prepare( `INSERT INTO property_assignments ( - structure_id, property_id, type, is_satisfied, proof, check_redundancy - ) VALUES (?, ?, ?, ?, ?, ?)` + structure_id, property_id, type, is_satisfied, + proof, check_redundancy, label + ) VALUES (?, ?, ?, ?, ?, ?, ?)` + ) + + const proof_reference_insert = db.prepare( + `INSERT INTO proof_references ( + structure_id, property_id, type, reference + ) VALUES (?, ?, ?, ?)` ) function insert_property_assignments( @@ -237,8 +244,13 @@ function seed_structures({ type, is_satisfied, entry.proof, - entry.check_redundancy === false ? 0 : 1 + entry.check_redundancy === false ? 0 : 1, + entry.label || null ) + + for (const ref of entry.references ?? []) { + proof_reference_insert.run(structure_id, entry.property, type, ref) + } } } diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index fe33f69b..1bf2830e 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -32,6 +32,8 @@ export type PropertyEntry = { property: string proof: string check_redundancy?: boolean + label?: string + references?: string[] } type ObjectEntry = {