Fix mistakes on content pages

.claude/skills/check-proofs/SKILL.md

@@ -30,6 +30,7 @@ All other argument text is additional context; consider it without narrowing the
 4. Use relevant repository context when a proof depends on a local definition or referenced CatDat entry. Keep the assessment grounded in available sources; flag context that cannot be checked.
     - Prefer reading a known source file directly, especially when a CatDat link or entry ID identifies it. For content links, check the matching Markdown file under `content/`; for data entries, locate the YAML source under the appropriate `database/data/` directory (use Glob with the entry's ID as filename). Do not rely on generated files under `build/`.
     - When the path is unknown, Grep only the relevant source directory (`content/` or `database/data/`) for one short, distinctive plain-text term or the entry's ID. Avoid long LaTeX expressions, complex regular expressions, and queries combining many alternatives.
+    - Use the size notions (small, essentially small, locally small, ...) as defined in `content/foundations.md`. In particular, an essentially small _collection_ (such as a (co)generating collection) is one that is isomorphic to a set; do not confuse it with an essentially small _category_, which is equivalent to a small category.
     - Treat a search with no matches as inconclusive, not as evidence that the reference is absent. Check the intended source path, then retry with a simpler term or exact filename. Only report that context is unavailable after these checks fail.
 5. This is a read-only review. Do not edit files, apply fixes, or invoke database update workflows. Do not propose rewritten proofs unless the user separately asks.
 

content/Grp_total_explicit_proof.md

@@ -7,62 +7,64 @@ description: An explicit construction of the left adjoint to the covariant Yoned
 
 The definition of a [total](/category-property/total) category is very abstract; furthermore, it is not immediately clear how it is possible for _any_ category which is not essentially small to satisfy the definition, much less a wide variety of the algebraic and topological categories which are considered in practice. Thus, to illustrate the definition, we give an explicit construction of the functor
 $$L : [\Grp^{\op},\Set] \to \Grp$$
-that is left adjoint to the Yoneda embedding $y : \Grp \hookrightarrow [\Grp^{\op},\Set]$.
+that is left adjoint to the Yoneda embedding $y : \Grp \hookrightarrow [\Grp^{\op},\Set]$ and therefore witnesses that $\Grp$ is total.
 
 Fix a functor $T : \Grp^{\op} \to \Set$. To construct the group $L(T)$, we will make use of the usual cogroup structure on $\IZ$ in $\Grp$, which includes
 
 - the comultiplication homomorphism $\mu : \IZ \to \IZ * \IZ'$, $1 \mapsto 1 \cdot 1'$ (where $\IZ'$ denotes a copy of $\IZ$),
 - the coidentity homomorphism $\varepsilon : \IZ \to 0$,
-- the coinverse homomorphism $\iota : \IZ \to \IZ$.
+- the coinverse homomorphism $\sigma : \IZ \to \IZ$.
 
-Also, let $i_1,i_2 : \IZ \rightrightarrows \IZ * \IZ'$ denote the coprojections. We define the group $L(T)$ as the group generated by elements $e(x)$, one for each element $x \in T(\IZ)$, subject to the following relations:
+Also, let $\iota_1, \iota_2 : \IZ \rightrightarrows \IZ * \IZ'$ denote the coprojections. We define the group $L(T)$ as the group generated by elements $e(x)$, one for each element $x \in T(\IZ)$, subject to the following relations:
 
-- $e(T\mu(x)) = e(Ti_1(x)) \cdot e(Ti_2(x))$ for each $x \in T(\IZ * \IZ')$,
-- $e(T\varepsilon(x)) = 1$ for each $x \in T0$,
-- $e(T\iota(x)) = e(x)^{-1}$ for each $x \in T\IZ$.
+- $e(T(\mu)(x)) = e(T(\iota_1)(x)) \cdot e(T(\iota_2)(x))$ for each $x \in T(\IZ * \IZ')$,
+- $e(T(\varepsilon)(x)) = 1$ for each $x \in T(0)$,
+- $e(T(\sigma)(x)) = e(x)^{-1}$ for each $x \in T(\IZ)$.
 
-We first need to define a natural transformation $\eta_T : T \to \Hom({-}, L(T))$. For each group $H$ we define the function $\eta_T(H) : TH \to \Hom(H, L(T))$ by sending $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$ mapping $1 \mapsto 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
+We first need to define a natural transformation
+$$\eta_T : T \to \Hom({-}, L(T)).$$
+For each group $H$ we define the function $\eta_T(H) : T(H) \to \Hom(H, L(T))$ by sending $x \in T(H)$ to the map
+$$H \to L(T), \quad h \mapsto e(T(\widetilde{h})(x)),$$
+where $\widetilde{h} : \IZ \to H$ denotes the homomorphism mapping $1 \mapsto h$, so that $T(\widetilde{h}) : T(H) \to T(\IZ)$. To see that this defines a group homomorphism from $H$ to $L(T)$, for $h,h' \in H$ we define the homomorphism $[h,h'] : \IZ * \IZ' \to H$ by $[h,h'] \circ \iota_1 = \widetilde{h}$ and $[h,h'] \circ \iota_2 = \widetilde{h'}$. Note that $[h,h'] \circ \mu = \widetilde{hh'}$. Hence,
 
 $$
-\begin{CD}
-T(H) @> = >> T(H)\\
-@V T(hh') VV @VVV\\
-T(\IZ * \IZ') @>>> T(\IZ)
-\end{CD}
+\begin{align*}
+e(T(\widetilde{hh'})(x)) &= e(T(\mu)(T([h,h'])(x))) \\
+& = e(T(\iota_1)(T([h,h'])(x))) \cdot e(T(\iota_2)(T([h,h'])(x))) \\
+& = e(T(\widetilde{h})(x)) \cdot e(T(\widetilde{h'})(x)),
+\end{align*}
 $$
 
-where on the bottom we use $T\mu, Ti_1, Ti_2$, and on the right we use $h h', h, h'$. Applying this to $x\in TH$, we get $T(h h')(x)$, $Th(x)$, and $Th'(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)) \cdot e(Th'(x)),$$
-as required. Similar proofs show that the map $H \to L(T)$ respects inverses and the identity. We leave it as an exercise for the reader to show this is natural in $H$.
+as required. Similar proofs show that the map $H \to L(T)$ respects inverses and the identity. We leave it as an exercise to verify that $\eta_T(H)$ 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})_{\IZ} \circ (\eta_T)_{\IZ} : 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,
+We start with uniqueness: suppose that $\varphi$ is such a homomorphism. Then, in particular,
+$$\alpha_{\IZ} = (y_{\varphi})_{\IZ} \circ (\eta_T)_{\IZ} : 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 group 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 satisfied 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\\
+T(\IZ * \IZ') @> \alpha_{\IZ * \IZ'} >> \Hom(\IZ * \IZ', G) @> \simeq >> U(G) \times U(G)\\
 @VVV @VVV @VVV\\
-T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> UG
+T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> U(G)
 \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 satisfied.
+by applying naturality to $\mu, \iota_1, \iota_2 : \IZ \to \IZ * \IZ'$, where $U : \Grp \to \Set$ denotes the forgetful functor. 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(T(\iota_1)(x)) \cdot e(T(\iota_2)(x))$ in $U(G)$ agree for any element $x \in T(\IZ * \IZ')$. Similar proofs show that the other relations are also satisfied.
 
-Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$, i.e. $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H$ 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 homomorphism $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
+Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$, i.e. $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H$ for each group $H$. By definition, for each $x \in T(H)$, the first step gives the homomorphism $h \mapsto e(T(\widetilde{h})(x))$; then the second step is formed by composition with $\varphi$. By the specification of $\varphi$, this gives the homomorphism $h \mapsto \alpha_{\IZ}(T(\widetilde{h})(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).
+T(H) @> \alpha_H >> \Hom(H, G) \\
+@V T(\widetilde{h}) VV @VV {-} \circ \widetilde{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)$. <span class="qed">$\square$</span>
+Applying this to $x \in T(H)$ gives exactly that $\alpha_{\IZ}(T(\widetilde{h})(x))(1) = \alpha_H(x)(h)$. <span class="qed">$\square$</span>

content/cocongruences_of_groups.md

@@ -1,11 +1,11 @@
 ---
-title: Cocongruences on groups are effective
+title: Cocongruences of groups are effective
 description: This result will be proved more generally for categories in which pushouts and monomorphisms interact in a suitable way.
 ---
 
-# Cocongruences on groups are effective
+# Cocongruences of groups are effective
 
-Our goal is to prove that every cocongruence in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way.
+Our goal is to prove that every cocongruence (see definition [here](/category-property/coquotients_of_cocongruences)) in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way.
 
 We shall say that a category $\C$ has _good pushouts of monomorphisms_ if it has pushouts of monomorphisms and if, for every diagram of monomorphisms
 
@@ -105,3 +105,7 @@ Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquel
 ::: Corollary 3
 Every cocongruence in the category $\Grp$ is effective.
 :::
+
+::: Proof
+We know that $\Grp$ is balanced (since it is mono-regular, see [here](/category/Grp) for the proofs) and has equalizers. Moreover, it has good pushouts of monomorphisms by Proposition 1. Thus, the claim follows from Proposition 2.
+:::

content/congruences_in_rel.md

@@ -83,7 +83,7 @@ We can also conclude that $E$ is the kernel pair of this quotient, by the genera
 ::: Lemma
 Suppose we have a congruence $f, g : E \rightrightarrows X$ with a contractible coequalizer
 $$ E \, \overset{f}{\underset{g}{\rightrightarrows}} \, X \overset{e}{\rightarrow} Q $$
-with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a cartesian square
+with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a pullback square
 
 $$
 \begin{CD}

content/constant_morphisms.md

@@ -5,8 +5,10 @@ description: We prove some results that help determine whether a morphism in a c
 
 # Results on constant morphisms
 
+Recall that a map of sets $f : X \to Y$ is called constant if $f(x_1)=f(x_2)$ for all $x_1,x_2 \in X$. There is also another definition, which requires $f$ to factor through a singleton set, but we will not use it here. Hence, the unique map $\varnothing \to \varnothing$ is regarded as constant.
+
 ::: Lemma 1
-A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense.
+A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map.
 :::
 
 ::: Proof

content/effective-congruence-quotients.md

@@ -1,21 +1,25 @@
 ---
-title: Quotients of effective congruences are strict quotients
-description: Quotients by effective congruences are characterized via a pullback
+title: Quotients of effective congruences
+description: If an effective congruence has a quotient, it is the kernel pair of this quotient.
 ---
 
-# Quotients of effective congruences are strict quotients
+# Quotients of effective congruences
+
+Recall that a congruence $E \rightrightarrows X$ is called effective if it is the kernel pair of some morphism with domain $X$. The next result shows that, in many situations, this morphism can be chosen canonically, namely as the quotient of the congruence, provided that it exists.
 
 ::: Lemma
-Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square
-$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E. \end{CD}$$
+An effective congruence whose coequalizer exists is the kernel pair of its coequalizer. More precisely, let $f,g : E \rightrightarrows X$ be an effective congruence. If $f,g$ have a coequalizer $p : X \to X/E$, then $f,g$ is the kernel pair of $p$. That is, the square
+$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E \end{CD}$$
+is a pullback.
 :::
 
 ::: Proof
-Suppose we have $h : X \to Z$ so that we have a cartesian square
-$$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$
-Then by the universal property of the coequalizer, there is a unique morphism
+Let $h : X \to Z$ be a morphism such that $f,g$ is the kernel pair of $h$. By the universal property of the coequalizer, there is a unique morphism
 $$\bar h : X/E \to Z$$
-such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then
-$$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$
-so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic.
+such that $h = \bar h \circ p$. Now suppose we have morphisms $a, b : T \rightrightarrows X$ such that $p \circ a = p \circ b$. Then
+$$h \circ a = \bar h \circ p \circ a = \bar h \circ p \circ b = h \circ b.$$
+Since $f,g$ is the kernel pair of $h$, this means that the pair $a, b$ factors uniquely through the pair $f,g$.
 :::
+
+This result is similar to the [lemma](/content/regular-epis-kernel-pairs) that a regular monomorphism is the equalizer of its cokernel pair, provided that the cokernel pair exists.
+<!-- TODO: Are these results deducible from one another? -->

content/foundations.md

@@ -97,7 +97,9 @@ If $\C, \D$ are categories, we can therefore construct the functor category $[\C
 
 It is better to state explicitly when the assumption of being locally small is needed.
 
-Equivalences of categories are defined [as usual](https://en.wikipedia.org/wiki/Equivalence_of_categories). A category is _essentially small_ if it is equivalent to a small category. A collection $X$ is essentially small if and only if the associated discrete category $X_{\disc}$ (which has only identity morphisms) is essentially small. In this sense, the two notions are compatible.
+Equivalences of categories are defined [as usual](https://en.wikipedia.org/wiki/Equivalence_of_categories). A category is _essentially small_ if it is equivalent to a small category. A collection $S$ is essentially small if and only if the associated discrete category $S_{\disc}$ (which has only identity morphisms) is essentially small. In this sense, the two notions are compatible.
+
+However, a collection of objects $S \subseteq \Ob(\C)$ of a category $\C$ must not be identified with the full subcategory of $\C$ spanned by $S$: they are different kinds of objects, and their notions of being essentially small differ. For example, the collection of all singletons in $\Set$ is not essentially small, since it is isomorphic to the collection of all sets, whereas the full subcategory of $\Set$ spanned by the singletons is essentially small, since it is equivalent to the trivial category $\1$. For instance, a [generating collection](/category-property/generating_collection) is required to be essentially small as a collection, i.e., isomorphic to a set.
 
 ## Representable functors
 

content/missing_cogenerating_collections.md

@@ -6,7 +6,7 @@ description: A generalization of the proof that the category of commutative ring
 # Missing cogenerating collections
 
 ::: Lemma
-Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions:
+Let $\C$ be a category and $U: \C \to \Set$ be a functor. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions:
 
 1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective.
 2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism.
@@ -15,5 +15,5 @@ Then $\C$ does not have a cogenerating collection.
 :::
 
 ::: Proof
-Assume that there is a cogenerating collection $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction.
+Assume that there is a cogenerating collection $S$. In particular, $S$ is essentially small. By assumption (2) applied to a cardinal $\kappa > \sup \{\card(U(Y)) : Y \in S\}$, there is an object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$ for all $Y \in S$ and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction.
 :::