diff --git a/content/Grp_total_explicit_proof.md b/content/Grp_total_explicit_proof.md
new file mode 100644
index 00000000..2149442f
--- /dev/null
+++ b/content/Grp_total_explicit_proof.md
@@ -0,0 +1,37 @@
+---
+title: Explicit Proof that the Category of Groups is Total
+description: An explicit construction of the left adjoint to the covariant Yoneda embedding on the category of groups
+author: Daniel Schepler
+---
+
+## Explicit Proof that the Category of Groups is Total
+
+We will fix a functor $T : \Grp^{\op} \to \Set$. Based on this, we need to construct a group $L(T)$. The construction will work as follows: we start with a set of generators $e_x$, one for each element $x \in T\IZ$. Now let $\mu : \IZ \to \IZ * \IZ'$ be the comultiplication homomorphism, $1 \mapsto 1 \cdot 1'$, and $i_1, i_2 : \IZ \rightrightarrows \IZ * \IZ'$ the two coprojections. We now add a relation $e_{T\mu(x)} = e_{Ti_1(x)} \cdot e_{Ti_2(x)}$ for each element $x \in T(\IZ * \IZ')$. Similarly, letting $\iota : \IZ \to \IZ$ be the coinverse homomorphism, we add a relation $e_{T\iota(x)} = e_x^{-1}$ for each element $x \in T\IZ$; and letting $\varepsilon : \IZ \to 0$ be the coidentity homomorphism, we add a relation $e_{T\varepsilon(x)} = 1$ for each element $x \in T0$.
+
+We first need to define the natural transformation $\eta_T : T \to \Hom({-}, L(T))$. To start, for each group $H$ we need a function $TH \to \Hom(H, L(T))$. We will define this function to send $x \in TH$ to $h \mapsto e_{Th(x)}$, where we abuse notation to identify $h \in H$ with the corresponding morphism $\IZ \to H$, so that $Th : TH \to T\IZ$. To see that this defines a group homomorphism from $H$ to $L(T)$, note that for $h, h' \in H$ we have three commutative diagrams of the form
+$$\begin{CD}
+T(H) @> = >> T(H)\\
+@V T(h * h') VV @VVV\\
+T(\IZ * \IZ') @>>> T(\IZ)
+\end{CD}$$
+where on the bottom we use $T\mu, Ti_1, Ti_2$. Applying this to $x\in TH$, we get $Th(x)$, $Th'(x)$, and $T(h h')(x)$, respectively. Thus, the relation $e_{T\mu(y)} = e_{Ti_1(y)} \cdot e_{Ti_2(y)}$ with $y \coloneqq T(h * h')(x)$ implies
+$$e_{T(hh')(x)} = e_{Th(x)} e_{Th'(x)},$$
+as required. Similar proofs show that the map $H \to G$ respects inverses and the identity. We leave it as an exercise for the reader to show this is natural in $H$.
+
+We now need to show that for each group $G$ and natural transformation $\alpha : T \to y_G$, there exists a unique group homomorphism $\varphi : L(T) \to G$ such that $\alpha = y_{\varphi} \circ \eta_T : T \to \Hom({-}, L(T)) \to \Hom({-}, G)$. We start with uniqueness: suppose $x \in T\IZ$. Then by hypothesis, $\alpha_{\IZ} = y_{\varphi} \circ (\eta_T)_{\alpha} : T\IZ \to \Hom(\IZ, L(T)) \to \Hom(\IZ, G)$. For each $x \in T\IZ$, the first step on the right hand side maps $x \mapsto (1 \mapsto e_x)$, and the second step then maps this to $1 \mapsto \varphi(e_x)$. Therefore, $\varphi(e_x) = \alpha_{\IZ}(x)(1)$ for each $x$, which establishes the uniqueness of $\varphi$.
+
+For the existence part, the first step is to show there is a gruop homomorphism $L(T) \to G$ with the images of $e_x$ required by the previous part, i.e. $e_x \mapsto \alpha_{\IZ}(x)(1)$. To prove this, we need to check that the relations in $L(T)$ are collapsed in $G$. Now, for each $x \in T(\IZ * \IZ')$, we have three commutative diagrams of the form
+$$\begin{CD}
+T(\IZ * \IZ') @> \alpha_{\IZ * \IZ'} >> \Hom(\IZ * \IZ', G) @> \simeq >> UG \times UG\\
+@VVV @VVV @VVV\\
+T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> UG
+\end{CD}$$
+applying naturality to $\mu, i_1, i_2 : \IZ \to \IZ * \IZ'$. On the right hand side, we get multiplication, first projection, and second projection respectively. From this, we conclude that the images of $e_{T\mu(x)}$ and $e_{Ti_1(x)} \cdot e_{Ti_2(x)}$ in $UG$ agree for any element $x \in T(\IZ * \IZ')$. Similar proofs show that the other relations are also collapsed.
+
+Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$. It suffices to show $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H : TH \to \Hom(H, L(T)) \to \Hom(H, G)$ for each group $H$. By definition, for each $x \in TH$, the first step gives the homomorphism $h \mapsto e_{Th(x)}$; then the second step is formed by composition with $\varphi$. By the specification of $\varphi$, this gives the homorphism $h \mapsto \alpha_{\IZ}(Th(x))(1)$. However, by the assumption that $\alpha$ is a natural transformation, for each $h \in H$ we have a commutative diagram
+$$\begin{CD}
+TH @> \alpha_H >> \Hom(H, G) \\
+@V Th VV @VV {-} \circ h V \\
+T\IZ @> \alpha_{\IZ} >> \Hom(\IZ, G).
+\end{CD}$$
+Applying this to $x \in TH$ gives exactly that $\alpha_{\IZ}(Th(x))(1) = \alpha_H(x)(h)$. $\square$
diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md
index a59d81f7..ffcf9dfc 100644
--- a/content/missing_cogenerator.md
+++ b/content/missing_cogenerator.md
@@ -13,8 +13,10 @@ Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume
1. For any $X \in \F$ and any $Y \in \C$, every non-zero morphism $f: X \to Y$ is injective on underlying sets.
2. For every $Y \in \C$ there is some object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$.
-Then $\C$ does not have a cogenerator.
+Then $\C$ does not have a cogenerator. Moreover, if $\C$ is locally essentially small, then $\C$ is not cototal.
:::
_Proof._
-Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. $\square$
+Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$.
+
+Now assume that $\C$ is locally essentially small and cocotal. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. Treating $\F$ as a discrete diagram in $\C$, assumption (1) implies that for any object $Y$ of $\C$, the collection of cocones $\F \to Y$ is bijective with a set, since the maps $X \to Y$ with $\card(U(X)) > \card(U(Y))$ must all be zero in such a cocone. Therefore, by Kelly, Thm. 5.6, $\C$ must have a coproduct $Y$ of all elements of $\F$. But then by assumption (2), there exists $X \in \F$ such that $\card(U(X)) > \card(U(Y))$; and since $\C$ is pointed, the coprojection $X \to Y$ must be split monic and therefore non-zero. Using assumption (1), we get a contradiction. $\square$
diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml
index e8d409bc..7e188757 100644
--- a/database/data/categories/Alg(R).yaml
+++ b/database/data/categories/Alg(R).yaml
@@ -40,8 +40,8 @@ unsatisfied_properties:
- property: semi-strongly connected
proof: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected.
- - property: cogenerating set
- proof: 'We apply this lemma to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+ - property: cototal
+ proof: Essentially the same proof as for $\CAlg(R)$ works here.
- property: codistributive
proof: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see MSE/625874 for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually no isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative, it has the algebra presentation $\langle X,E : E^2=E \rangle$.'
diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml
index 04313c46..782b31d4 100644
--- a/database/data/categories/CAlg(R).yaml
+++ b/database/data/categories/CAlg(R).yaml
@@ -19,7 +19,7 @@ satisfied_properties:
proof: There is a forgetful functor $\CAlg(R) \to \Set$ and $\Set$ is locally small.
- property: finitary algebraic
- proof: Take the algebraic theory of a commutative ring.
+ proof: Take the algebraic theory of a commutative $R$-algebra.
- property: strict terminal object
proof: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.'
@@ -38,8 +38,8 @@ unsatisfied_properties:
- property: balanced
proof: Take a prime ideal $P \subseteq R$ and consider the commutative $R$-algebra $A \coloneqq R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample.
- - property: cogenerating set
- proof: 'We apply this lemma to the collection of commutative $R$-algebras which are fields: If $F$ is a commutative $R$-algebra that is also a field and $A$ is a non-trivial commutative $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+ - property: cototal
+ proof: 'Let $\F$ be the family of commutative $R$-algebras of the form $R \times k$ where $k$ is an infinite field including a quotient field of $R$. Then for any commutative $R$-algebra $A$, we have a distinguished morphism $R \times k \to A$ consisting of the projection to $R$ followed by the unique morphism $R \to A$. Moreover, if we have any morphism $\varphi : R \times k \to A$ which is not equal to the distinguished morphism, that implies that $\varphi(0, 1) \ne 0$, so the rng homomorphism $k \to R \times k \to A$ is injective, implying $\card(U(A)) \ge \card(U(k))$. From here, an argument similar to the one here gives a contradiction, using the distinguished morphisms in place of zero morphisms.'
- property: countably codistributive
proof: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A \coloneqq K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.'
diff --git a/database/data/categories/CRing.yaml b/database/data/categories/CRing.yaml
index cd2d74ed..7e53ba6d 100644
--- a/database/data/categories/CRing.yaml
+++ b/database/data/categories/CRing.yaml
@@ -44,8 +44,8 @@ unsatisfied_properties:
- property: balanced
proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample.
- - property: cogenerating set
- proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial commutative ring, any ring homomorphism $F \to R$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+ - property: cototal
+ proof: 'This is a special case of the proof for $\CAlg(R)$ with $R = \IZ$.'
- property: countably codistributive
proof: 'The canonical homomorphism $\IQ \otimes \IZ^{\IN} \to (\IQ \otimes \IZ)^{\IN} = \IQ^{\IN}$ is not an isomorphism: its image consists of those sequences of rational numbers whose denominators can be bounded.'
diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml
index ac10a69c..6495ff23 100644
--- a/database/data/categories/Cat.yaml
+++ b/database/data/categories/Cat.yaml
@@ -43,9 +43,6 @@ unsatisfied_properties:
- property: balanced
proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties.
- - property: cogenerating set
- proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.'
-
- property: regular
proof: See Example 3.14 at the nLab.
@@ -88,6 +85,12 @@ unsatisfied_properties:
$$\Sub_{\reg}(\{ 0 \to 1 \to 2 \}) \to \Sub_{\reg}(\{ 0 \to 1 \}) \times_{\Sub_{\reg}(\{1\})} \Sub_{\reg}(\{ 1 \to 2 \})$$
is not injective. Therefore, $\Sub_{\reg} : \Cat^{\op} \to \Set^+$ does not preserve pullbacks, so it cannot be representable.
+ - property: cototal
+ proof: >-
+ For each infinite cardinal $\kappa$, choose a simple group $S_\kappa$ of cardinality $\kappa$ (for example the group of permutations of $\kappa$ of finite support which are even). Now consider the ultra-wide pushout diagram $1 \rightrightarrows B S_\kappa$. Then for any small category $\C$, the collection of cocones $1 \rightrightarrows B S_\kappa \to \C$ is bijective with a set: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $S_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero.
+
+ On the other hand, we claim that $1 \rightrightarrows B S_\kappa$ does not have a pushout in $\Cat$; by Kelly, Thm. 5.6, this will imply that $\Cat$ is not cototal. To see this, suppose we have a pushout $\C$ of $1 \rightrightarrows B S_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$. Then the coprojection $i_\lambda : B S_\lambda \to \C$ must be split monic, since we can construct a cocone $1 \rightrightarrows B S_\kappa \to B S_\lambda$ in which $B S_\kappa \to B S_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B S_\lambda \to B S_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B S_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $S_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $S_\lambda$ is a simple group.
+
special_objects:
initial object:
description: empty category
diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml
index 0ffee152..fccde1f9 100644
--- a/database/data/categories/Grp.yaml
+++ b/database/data/categories/Grp.yaml
@@ -39,6 +39,10 @@ satisfied_properties:
- property: effective cocongruences
proof: A proof can be found here.
+ - property: total
+ proof: This follows formally from the fact that $\Grp$ is finitary algebraic and therefore locally presentable. For a more explicit proof, see here.
+ check_redundancy: false
+
- 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
@@ -50,7 +54,7 @@ unsatisfied_properties:
- property: normal
proof: Every non-normal subgroup (such as $C_2 \hookrightarrow S_3$) provides a counterexample.
- - property: cogenerator
+ - property: cototal
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).'
- property: coregular
diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml
index 02687dc5..ddbd4541 100644
--- a/database/data/categories/Haus.yaml
+++ b/database/data/categories/Haus.yaml
@@ -26,9 +26,11 @@ satisfied_properties:
- property: equalizers
proof: This follows from the corresponding fact for $\Top$ since subspaces of Hausdorff spaces are again Hausdorff.
+ check_redundancy: false
- property: products
proof: This follows from the corresponding fact for $\Top$ since products of Hausdorff spaces are again Hausdorff.
+ check_redundancy: false
- property: cocomplete
proof: This follows since $\Haus$ is a reflective subcategory of $\Top$, which is cocomplete. For the reflector, see e.g. the nLab. Explicitly, we construct the colimit of Hausdorff spaces by applying the reflector to the colimit of the underlying topological spaces.
@@ -71,10 +73,6 @@ unsatisfied_properties:
$$(-\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.
- - property: cogenerator
- # cspell: disable-next-line
- 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.'
-
- property: regular
proof: 'The regular epimorphisms are precisely the surjective quotient maps of Hausdorff spaces (see below). In a regular category, for every regular epimorphism $X \to Y$ and every object $Z$, the induced morphism $X \times Z \to Y \times Z$ is again a regular epimorphism. This is not the case in $\Haus$ (or $\Top$, for that matter). The standard example is the quotient map $\IR \to \IR / \IZ^+$, for which the induced map $\IR \times \IQ \to \IR/\IZ^+ \times \IQ$ is not a quotient map (MSE/1907972).'
@@ -85,6 +83,13 @@ unsatisfied_properties:
Let $C \coloneqq \{1,2\}$ be the discrete two-point space. The map $f : A \to C$ defined by $f(a)=1$ for $a \in A_1$ and $f(a)=2$ for $a \in A_2$ is continuous, since $A$ is discrete.
The pushout $C \sqcup_A \Gamma$ in $\Haus$ is the Hausdorff reflection of the pushout $Q$ in $\Top$. Notice that $Q$ is the quotient space of $\Gamma$ in which $A_1$ and $A_2$ are each collapsed to a point, denoted by $[A_1]$ and $[A_2]$. The canonical map $C \to Q$ is given by $i \mapsto [A_i]$. Now, $[A_1]$ and $[A_2]$ cannot be separated by disjoint open neighborhoods in $Q$, since such neighborhoods would pull back to disjoint open neighborhoods of $A_1$ and $A_2$ in $\Gamma$. Thus, they are identified in the Hausdorff reflection. This shows that the canonical map $C \to C \sqcup_A \Gamma$ is not injective and hence not a regular monomorphism.
+ - property: cototal
+ # cspell: disable-next-line
+ proof: >-
+ For each small cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. 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_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (The author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form an ultra-wide pushout diagram $1 \rightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \rightrightarrows X_\kappa \to Y$ is bijective to a set: if $Y$ is empty, then the collection of cocones is obviously empty. Otherwise, in order to form a cocone, we must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$.
+
+ On the other hand, we claim that $1 \rightrightarrows X_\kappa$ does not have a pushout in $\Haus$; by Kelly, Thm. 5.6, this will imply that $\Cat$ is not cototal. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \rightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points.
+
- 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.
diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml
index 65355a68..f052d935 100644
--- a/database/data/categories/LRS_R.yaml
+++ b/database/data/categories/LRS_R.yaml
@@ -47,11 +47,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.'
- - property: generating set
- proof: >-
- Out of any small set $S$ of locally ringed spaces, there is only a small set of residue fields at their points. Therefore, if $K$ is a field over $R$ with a strictly larger cardinality than any of these residue fields, then the only possible morphism from an element of $S$ to $\Spec K(X,Y)$ is one with an empty domain. However, that makes it impossible for $S$ to distinguish the two canonical automorphisms of $\Spec K(X,Y)$.
-
- Alternatively, using the usual adjunction between affine schemes and locally ringed spaces (EGA I (1971), Ch. 1, Prop. 1.6.3), a generating set in $\LRS_R$ would induce a generating set in the category of affine $R$-schemes, which contradicts the fact that $\CAlg(R)$ does not have a cogenerating set.
+ - property: total
+ proof: 'The adjunction between the global sections functor and the $\Spec$ functor (EGA I (1971), Ch. 1, Prop. 1.6.3) makes $\CAlg(R)^{\op}$ into a reflective subcategory of $\LRS_R$. Therefore, if $LRS_R$ were total, then \CAlg(R) would be cototal, which we know is not the case.'
- property: cartesian closed
proof: This is Corollary 4(a) here.
diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml
index aa3256ba..373b6f96 100644
--- a/database/data/categories/Meas.yaml
+++ b/database/data/categories/Meas.yaml
@@ -33,9 +33,11 @@ satisfied_properties:
- property: complete
proof: Take the limit of the underlying sets and take the smallest $\sigma$-algebra making all projections measurable.
+ check_redundancy: false
- property: cocomplete
proof: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable.
+ check_redundancy: false
- property: infinitary extensive
proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.'
diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml
index ccff1fea..255e9194 100644
--- a/database/data/categories/Mon.yaml
+++ b/database/data/categories/Mon.yaml
@@ -39,7 +39,7 @@ unsatisfied_properties:
- property: Malcev
proof: 'Consider the submonoid $\{(a,b) : a \leq b \}$ of $\IN^2$.'
- - property: cogenerator
+ - property: cototal
proof: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism $G \to M$ from a simple group $G$ to a monoid $M$ must be injective (as it corestricts to a homomorphism of groups $G \to M^{\times}$), and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).'
- property: counital
diff --git a/database/data/categories/On.yaml b/database/data/categories/On.yaml
index d4323b34..5724cac5 100644
--- a/database/data/categories/On.yaml
+++ b/database/data/categories/On.yaml
@@ -44,6 +44,7 @@ unsatisfied_properties:
- property: well-copowered
proof: The "quotients" of $0$ are all ordinals.
+ check_redundancy: false
- property: inverse
proof: Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$.
diff --git a/database/data/categories/Ring.yaml b/database/data/categories/Ring.yaml
index 3e074365..3435a83e 100644
--- a/database/data/categories/Ring.yaml
+++ b/database/data/categories/Ring.yaml
@@ -43,8 +43,8 @@ unsatisfied_properties:
- property: semi-strongly connected
proof: This is because already the full subcategory $\CRing$ does not have this property.
- - property: cogenerating set
- proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial ring, any ring homomorphism $F \to R$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+ - property: cototal
+ proof: 'This is a special case of the proof for $\Alg(R)$ with $R = \IZ$.'
- property: codistributive
proof: 'If $\sqcup$ denotes the coproduct of rings (see MSE/625874 for their description) and $R$ is a ring, the canonical morphism $R \sqcup \IZ^2 \to (R \sqcup \IZ)^2 = R^2$ is usually no isomorphism. For example, for $R = \IZ[X]$ the coproduct on the LHS is not commutative, it has the ring presentation $\langle X,E : E^2=E \rangle$.'
diff --git a/database/data/categories/Rng.yaml b/database/data/categories/Rng.yaml
index c7b20f43..6b8f47bb 100644
--- a/database/data/categories/Rng.yaml
+++ b/database/data/categories/Rng.yaml
@@ -36,7 +36,7 @@ unsatisfied_properties:
- property: balanced
proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. (The proof can be reduced to the unital case.)
- - property: cogenerator
+ - property: cototal
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$.'
- property: counital
diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml
index d7c90468..9d008990 100644
--- a/database/data/categories/SemiGrp.yaml
+++ b/database/data/categories/SemiGrp.yaml
@@ -54,14 +54,6 @@ 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
- # 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
- $$N \coloneqq \{g \in G : f(g) = f(1)\}$$
- is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction.
-
- property: cofiltered-limit-stable epimorphisms
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$.
@@ -71,6 +63,14 @@ unsatisfied_properties:
$$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$
whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.
+ - property: cototal
+ proof: >-
+ The proof is similar to the proof for $\Grp$. For each infinite cardinal $\kappa$, let $S_\kappa$ be a simple group of cardinality $\kappa$ (such as the alternating group on $\kappa$). We can then form the ultra-wide pushout diagram $1 \rightrightarrows S_\kappa$ in $\SemiGrp$. For every semigroup $A$, the collection of cocones $1 \rightrightarrows S_\kappa \to A$ is bijective to a set: for every such cocone, we must first choose an idempotent $e$ of $A$ corresponding to the map $1 \to A$. Then, whenever $\kappa > \card(U(A))$, then for $f_\kappa : S_\kappa \to A$ in the cocone, we see
+ $$N \coloneqq \{g \in S_\kappa : f_\kappa(g) = e\}$$
+ is a normal subgroup of $G$. It must be non-trivial since otherwise $f_\kappa$ would induce an injective group homomorphism from $G$ to a group contained in $A$. Therefore, $N$ is all of $G$, so $f_\kappa$ is the constant map with image $a$.
+
+ We now claim that $1 \rightrightarrows S_\kappa$ does not have a pushout in $\SemiGrp$; by Kelly, Thm. 5.6, this will imply that $\Cat$ is not cototal. To see this, suppose we had a pushout $A$, and let $\lambda$ be a cardinal strictly greater than $\card(U(A))$. Then the coprojection $S_\lambda\to A$ must be split monic, since we can construct a cocone $1 \rightrightarrows S_\kappa \to S_\lambda$ such that the map $S_\kappa \to S_\lambda$ is the constant map with image 1 if $\kappa \ne \lambda$, while the map $S_\lambda \to S_\lambda$ is the identity. But this contradicts the choice of $\lambda$.
+
- property: natural numbers object
proof: >-
Assume that a natural numbers object exists. Then by this result, for every semigroup $A$ the natural homomorphism
diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml
index a48168fe..f494a763 100644
--- a/database/data/categories/Top.yaml
+++ b/database/data/categories/Top.yaml
@@ -21,6 +21,7 @@ satisfied_properties:
- property: complete
proof: Take the limit of the underlying sets and endow it with the coarsest topology making all projections continuous.
+ check_redundancy: false
- property: cocomplete
proof: Take the colimit of the underlying sets and endow it with the finest topology making all inclusions continuous.
diff --git a/database/data/category-implications/total.yaml b/database/data/category-implications/total.yaml
new file mode 100644
index 00000000..057d6e05
--- /dev/null
+++ b/database/data/category-implications/total.yaml
@@ -0,0 +1,40 @@
+# results on total and cototal categories
+
+- id: total_cocomplete
+ assumptions:
+ - total
+ - locally essentially small
+ conclusions:
+ - cocomplete
+ proof: 'A diagram $X : \I \to \C$ with $\I$ small and $\C$ locally essentially small is easily seen to satisfy the hypotheses of condition (2) in the definition of a total category.'
+ is_equivalence: false
+
+# TODO: If adding a property "has a weak terminal object", that can be added to the conclusions here: The identity functor $\C \to \C$ is also a discrete fibration, and its colimit must certainly at least be a weakly terminal object. It's unclear to me at this time whether it must necessarily be a terminal object in case $\C$ is not locally essentially small.
+- id: total_initial
+ assumptions:
+ - total
+ conclusions:
+ - initial object
+ proof: 'The empty diagram is vacuously a discrete fibration; thus, it has a colimit, which must be an initial object.'
+ is_equivalence: false
+
+- id: total_complete
+ assumptions:
+ - total
+ - locally essentially small
+ conclusions:
+ - complete
+ proof: 'This is proven in Kelly, Thm. 5.6.'
+ is_equivalence: false
+
+# TODO: replace "well-copowered" with "epi-cocomplete" if adding the latter property
+- id: cocomplete_well-copowered_generator_implies_total
+ assumptions:
+ - cocomplete
+ - locally essentially small
+ - well-copowered
+ - generating set
+ conclusions:
+ - total
+ proof: 'Since the category is cocomplete and well-copowered, it is epi-cocomplete (meaning that it has wide pushouts of epimorphisms, even of non-small families of epimorphisms). The result then follows from Day, Thm. 1.'
+ is_equivalence: false
diff --git a/database/data/category-properties/cototal.yaml b/database/data/category-properties/cototal.yaml
new file mode 100644
index 00000000..dd948d96
--- /dev/null
+++ b/database/data/category-properties/cototal.yaml
@@ -0,0 +1,25 @@
+id: cototal
+relation: is
+description: >-
+ Let $\C$ be a category. Then the following are equivalent (Kelly, Thm. 5.5):
+
+ 1. A diagram $X : \I \to \C$ (with $\I$ not necessarily essentially small) is called a discrete op-fibration if for every $i \in \I$ and morphism $f : X_i \to Y$ in $\C$, there exists a unique $\alpha : i\to j$ in $\I$ such that $X_\alpha = f$. This condition is that every discrete op-fibration whose fibers are bijective to sets has a limit in $\C$.
+
+ 2. Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $X \downarrow Y$ is bijective to a set. Then $X$ has a limit in $\C$.
+
+ A general category is cototal if it satisfies one of the above conditions.
+
+ Note that if $\C$ is locally small, $\C$ is total if and only if the contravariant Yoneda embedding $y : \C^{\op} \to [\C, \Set]$ has a left adjoint (Kelly, Thm. 5.2).
+nlab_link: https://ncatlab.org/nlab/show/total+category
+dual: total
+invariant_under_equivalences: true
+
+related:
+ - cocomplete
+ - complete
+ - locally copresentable
+
+tags:
+ - limits
+ - colimits
+ - size
diff --git a/database/data/category-properties/locally copresentable.yaml b/database/data/category-properties/locally copresentable.yaml
index 60978091..7a129824 100644
--- a/database/data/category-properties/locally copresentable.yaml
+++ b/database/data/category-properties/locally copresentable.yaml
@@ -8,6 +8,7 @@ invariant_under_equivalences: true
related:
- coaccessible
- complete
+ - cototal
tags:
- accessibility
diff --git a/database/data/category-properties/locally presentable.yaml b/database/data/category-properties/locally presentable.yaml
index fca891a4..ef2d78df 100644
--- a/database/data/category-properties/locally presentable.yaml
+++ b/database/data/category-properties/locally presentable.yaml
@@ -17,6 +17,7 @@ invariant_under_equivalences: true
related:
- accessible
- cocomplete
+ - total
- locally finitely presentable
- locally multi-presentable
- locally poly-presentable
diff --git a/database/data/category-properties/total.yaml b/database/data/category-properties/total.yaml
new file mode 100644
index 00000000..62fb22bc
--- /dev/null
+++ b/database/data/category-properties/total.yaml
@@ -0,0 +1,25 @@
+id: total
+relation: is
+description: >-
+ Let $\C$ be a category. Then the following are equivalent (Kelly, Thm. 5.5):
+
+ 1. A diagram $X : \I \to \C$ (with $\I$ not necessarily essentially small) is called a discrete fibration if for every $i \in \I$ and morphism $f : Y \to X_i$ in $\C$, there exists a unique $\alpha : j \to i$ in $\I$ such that $X_\alpha = f$. This condition is that every discrete fibration whose fibers are bijective to sets has a colimit in $\C$.
+
+ 2. Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $Y \downarrow X$ is bijective to a set. Then $X$ has a colimit in $\C$.
+
+ A general category is total if it satisfies one of the above conditions.
+
+ Note that if $\C$ is locally small, $\C$ is total if and only if the covariant Yoneda embedding $y : \C \to [\C^{\op}, \Set]$ has a left adjoint (Kelly, Thm. 5.2). For a concrete example of how such a left adjoint could look, see here.
+nlab_link: https://ncatlab.org/nlab/show/total+category
+dual: cototal
+invariant_under_equivalences: true
+
+related:
+ - cocomplete
+ - complete
+ - locally presentable
+
+tags:
+ - limits
+ - colimits
+ - size
diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json
index 4d8ef7c2..6a056762 100644
--- a/database/scripts/expected-data/Ab.json
+++ b/database/scripts/expected-data/Ab.json
@@ -120,6 +120,8 @@
"extremal generating set": true,
"extremal cogenerator": true,
"extremal cogenerating set": true,
+ "total": true,
+ "cototal": true,
"cartesian closed": false,
"locally cartesian closed": false,
diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json
index 5ceebb92..4d7ea47b 100644
--- a/database/scripts/expected-data/Set.json
+++ b/database/scripts/expected-data/Set.json
@@ -117,6 +117,8 @@
"extremal generating set": true,
"extremal cogenerator": true,
"extremal cogenerating set": true,
+ "total": true,
+ "cototal": true,
"Grothendieck abelian": false,
"Malcev": false,
diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json
index f66e00c9..0baa363b 100644
--- a/database/scripts/expected-data/Top.json
+++ b/database/scripts/expected-data/Top.json
@@ -82,6 +82,8 @@
"ℵ₂-small copowers": true,
"extremal cogenerator": true,
"extremal cogenerating set": true,
+ "total": true,
+ "cototal": true,
"abelian": false,
"additive": false,