Add proof references

.cspell.json

@@ -62,6 +62,7 @@
 		"cocartesian",
 		"coclosed",
 		"cocomplete",
+		"cocompleteness",
 		"cocompletion",
 		"cocone",
 		"cocones",
@@ -163,6 +164,7 @@
 		"freyd",
 		"Freyd",
 		"Frobenius",
+		"functionals",
 		"functor",
 		"functorial",
 		"functors",

database/data/categories/Ab.yaml

@@ -25,6 +25,7 @@ satisfied_properties:
 
   - property: abelian
     proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.
+    label: ab_abelian
 
   - property: finitary algebraic
     proof: Take the algebraic theory of a commutative group.

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 <a href="/category/Ring">$\Ring$</a>.
+    references:
+      - ring_disjoint_finite_products
 
   - property: Malcev
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+    references:
+      - grp_malcev
 
 unsatisfied_properties:
   - property: skeletal
@@ -51,9 +55,13 @@ unsatisfied_properties:
 
   - property: coregular
     proof: 'We just need to tweak the proof for <a href="/category/Ring">$\Ring$</a>. 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 (<a href="https://math.stackexchange.com/questions/22629" target="_blank">proof</a>) or via a direct calculation with elementary matrices.'
+    references:
+      - ring_not_coregular
 
   - property: regular quotient object classifier
-    proof: We may copy the proof for <a href="/category/CAlg(R)">$\CRing$</a> (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 <a href="/content/subcategories">here</a> (dualized).
+    proof: We may copy the proof for <a href="/category/CAlg(R)">$\CAlg(R)$</a> (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 <a href="/content/subcategories">here</a> (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 <a href="/category/Ring">$\Ring$</a>: 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:

database/data/categories/Ban.yaml

@@ -122,6 +122,8 @@ unsatisfied_properties:
 
   - property: filtered-colimit-stable monomorphisms
     proof: 'The proof is similar to <a href="/category/Met">$\Met$</a>. 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$ <i>and</i> $\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.'

database/data/categories/CAlg(R).yaml

@@ -27,9 +27,13 @@ satisfied_properties:
 
   - property: Malcev
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+    references:
+      - grp_malcev
 
   - property: coextensive
     proof: One can use the same proof as for <a href="/category/CRing">$\CRing$</a>.
+    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 <a href="/category/CRing">$\CRing$</a>: 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 <a href="https://math.stackexchange.com/questions/2391187" target="_blank">MSE/2391187</a>.

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 <a href="/category/Mon">$\Mon$</a>.
+    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 <a href="https://mathoverflow.net/questions/510431/" target="_blank">MO/510431</a>). 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.

database/data/categories/CRing.yaml

@@ -30,6 +30,8 @@ satisfied_properties:
 
   - property: Malcev
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+    references:
+      - grp_malcev
 
   - property: coextensive
     proof: >-
@@ -47,13 +49,15 @@ 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 <a href="/category/LRS_R">$\LRS$</a>, which is infinitary extensive. It follows that the category of affine schemes is extensive by Lemma 11 <a href="/content/subcategories">here</a>, 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
     proof: This is trivial.
 
   - 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 <a href="https://stacks.math.columbia.edu/tag/04W0" target="_blank">SP/04W0</a> to conclude that it is no epimorphism in $\CRing$.'

database/data/categories/Cat.yaml

@@ -51,13 +51,15 @@ unsatisfied_properties:
     proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.
 
   - property: coregular
-    proof: 'We already know that <a href="/category/Mon">$\Mon$</a> 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 (<a href="https://math.stackexchange.com/questions/574745" target="_blank">MSE/574745</a>), hence it preserves regular monomorphisms. It also preserves pushouts (<a href="https://math.stackexchange.com/questions/5130854" target="_blank">MSE/5130854</a>), 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 <a href="/category/Mon">$\Mon$</a> 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 (<a href="https://math.stackexchange.com/questions/574745" target="_blank">MSE/574745</a>), hence it preserves regular monomorphisms. It also preserves pushouts (<a href="https://math.stackexchange.com/questions/5130854" target="_blank">MSE/5130854</a>), 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 <a href="/category/Mon">$\Mon$</a> 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. <a href="https://mathoverflow.net/questions/509552">MO/509552</a>) 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 <a href="/category/Set">$\Set$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> 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 <a href="/category/Mon">$\Mon$</a>: Let $X$ be the <a href="/category/walking_idempotent">walking idempotent</a>, 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: >-

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 <a href="/category/Haus">$\Haus$</a>.
+    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 <a href="/category/Haus">$\Haus$</a>. 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: |-