Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .cspell.json

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have the cspell VS code extension which underlines unknown or incorrect words. For unknown / mathematical words I then click quick fix > add to config. Can you perhaps also use it?

The extension is useful since it catches lots of typos. (For example, it caught your typo cocotal in content/missing_cogenerator.md that I fixed in the other commit.)

Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,10 @@
"cogenerating",
"cogenerator",
"cogenerators",
"cogroup",
"Cohomology",
"coidentity",
"coinverse",
"cokernel",
"cokernels",
"colimit",
Expand All @@ -100,6 +103,7 @@
"comonadicity",
"compactification",
"compactifications",
"comultiplication",
"conormal",
"copower",
"copowers",
Expand Down Expand Up @@ -128,6 +132,7 @@
"cospans",
"cosymmetric",
"cosymmetry",
"cototal",
"cotransitive",
"cotransitivity",
"counit",
Expand Down Expand Up @@ -156,6 +161,7 @@
"extensivity",
"extremal",
"Faddeev",
"fibration",
"fieldification",
"filtrations",
"finitary",
Expand All @@ -178,6 +184,7 @@
"hausdorff",
"Hertweck",
"Heyting",
"homeomorphic",
"homotopic",
"homotopy",
"Hušek",
Expand Down Expand Up @@ -238,6 +245,7 @@
"Noetherian",
"Noncommutative",
"objectwise",
"opfibration",
"pointwise",
"Pontryagin",
"poset",
Expand Down
68 changes: 68 additions & 0 deletions content/Grp_total_explicit_proof.md

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have done quite a bit of rewording here. Please check if this is OK for you. I am afraid that the git diff is useless.

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please add a bit of context and motivation here in the introduction? Roughly:

  1. Grp is total by result XYZ
  2. More generally, every category that is monadic over Set is total by result XYZ
  3. Nevertheless, we add a proof for Grp here to highlight XYZ and explain XYZ
  4. The construction of the left adjoint shows in particular that ...

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The context was simply that I was having trouble wrapping my head around the definition just from reading the nLab page without this explicit example as a rough guide.

Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
---
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
---

## Explicit Proof that the Category of Groups is Total

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]$.

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$.

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:

- $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$,

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

$$
\begin{CD}
T(H) @> = >> T(H)\\
@V T(hh') VV @VVV\\
T(\IZ * \IZ') @>>> T(\IZ)
\end{CD}
$$

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 $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)) \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$.

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,
$$\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\\
@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 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

$$
\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)$. <span class="qed">$\square$</span>
6 changes: 4 additions & 2 deletions content/missing_cogenerator.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,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$. <span class="qed">$\square$</span>
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 cototal. 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 G. M. Kelly, <a href="https://www.numdam.org/item/?id=CTGDC_1986__27_2_109_0" target="_blank">A survey of totality for enriched and ordinary categories</a>, 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. <span class="qed">$\square$</span>
Comment thread
ScriptRaccoon marked this conversation as resolved.

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please explain in which way (the dual of) Thm. 5.6 applies. It says cototal => cocompact => hypercocomplete => ..., where does it say that diagrams with "few cocones" have colimits?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't hypercocomplete exactly that?

4 changes: 2 additions & 2 deletions database/data/categories/Alg(R).yaml
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ unsatisfied_properties:
- property: semi-strongly connected
proof: This is because already the full subcategory <a href="/category/CAlg(R)">$\CAlg(R)$</a> of commutative algebras is not semi-strongly connected.

- property: cogenerating set
proof: 'We apply <a href="/content/missing_cogenerating_sets">this lemma</a> 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 <a href="/category/CAlg(R)">$\CAlg(R)$</a> works here.

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Try to find a variant of the lemma that takes care of both categories.


- property: codistributive
proof: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see <a href="https://math.stackexchange.com/questions/625874" target="_blank">MSE/625874</a> 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$.'
Expand Down
6 changes: 3 additions & 3 deletions database/data/categories/CAlg(R).yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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$.'
Expand All @@ -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 <a href="/content/missing_cogenerating_sets">this lemma</a> 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 <a href="/content/missing_cogenerator">here</a> gives a contradiction, using the distinguished morphisms in place of zero morphisms.'

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The lemma has been added to unify various proofs. If we only write now "an argument similar to ...", the lemma has lost its purpose. I suggest to either write down a self-contained proof or find a variant of the lemma that handles this. Maybe (a spontaneous guess!) also a reduction to the category of non-unital commutative algebras is possible (which is pointed): you are working with augmented algebras here, which are equivalent to non-unital algebras.


- 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}$.'
Expand Down
4 changes: 2 additions & 2 deletions database/data/categories/CRing.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ unsatisfied_properties:
- property: balanced
proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample.

- property: cogenerating set
proof: 'We apply <a href="/content/missing_cogenerating_sets">this lemma</a> 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 <a href="/category/CAlg(R)">$\CAlg(R)$</a> 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.'
Expand Down
9 changes: 6 additions & 3 deletions database/data/categories/Cat.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,6 @@ unsatisfied_properties:
- property: balanced
proof: Since we know that <a href="/category/Mon">$\Mon$</a> 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 <a href="/category/Mon">$\Mon$</a>, which we know does not exist.'

- property: regular
proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.

Expand Down Expand Up @@ -89,6 +86,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: >-

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we can make the proof more conceptual by doing something like: if Cat is cototal, then also 1 / Cat is cototal by result XYZ, and then (adjunction?) also Grp is cototal, which is not true. In fact, you are basically repeating the proof that Grp is not cototal here.

Alternatively, can we use the lemma?

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.

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now consider the ultra-wide pushout diagram $1 \rightrightarrows B S_\kappa$

Please explain this a bit more. I assume you mean the diagram that consists of the unique morphisms $1 \to B S_\kappa$ for all $\kappa$?

The notation $1 \rightrightarrows B S_\kappa$ is a bit weird since $\rightrightarrows$ indicates two arrows. Likewise, the notation $1 \rightrightarrows B S_\kappa \to \C is a bit weird.

Also, this is not a pushout diagram (it lacks the pushout object).

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe one can use a notation like $X \mathrel{\substack{\rightarrow\\[-0.6ex]\cdots\\[-0.6ex]\rightarrow}} Y$, a variant of the \rightrightrightarrows macro that I have added recently.

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe it's better to denote this group by $A_\kappa$ so that one doesn't think all the time of the symmetric group (which is literally denoted $S_\kappa$ in the literature).

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we maybe want to write Aut(X) instead of End(X)?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be pretty much equivalent given the group of units functor is a coreflector from monoids to groups, right?

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes it is equivalent, I just wanted to ask if Aut(X) is better because it is used by default in the context of group actions.

@ScriptRaccoon ScriptRaccoon Aug 4, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for example the group of permutations of $\kappa$ of finite support which are even

Maybe formulate it just like in the proof for SemiGrp:

such as the alternating group on $\kappa$

I have also used the term "alternating group" (on infinite sets) in other proofs. Since the sign only makes sense for permutations with finite support, this condition should be clear.


On the other hand, we claim that $1 \rightrightarrows B S_\kappa$ does not have a pushout in $\Cat$; by G. M. Kelly, <a href="https://www.numdam.org/item/?id=CTGDC_1986__27_2_109_0" target="_blank">A survey of totality for enriched and ordinary categories</a>, 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.

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As in my other comment, please explain in which way Thm. 5.6. gives us that the pushout would exist.

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

$\lambda > \card(\Mor(\C))$

Maybe one can briefly mention that this is possible since $C$ is small.


special_objects:
initial object:
description: empty category
Expand Down
6 changes: 5 additions & 1 deletion database/data/categories/Grp.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,10 @@ satisfied_properties:
- property: effective cocongruences
proof: A proof can be found <a href="/content/cocongruences_of_groups">here</a>.

- property: total
proof: This follows formally from the fact that $\Grp$ is finitary algebraic and therefore locally presentable. For a more explicit proof, see <a href="/content/Grp_total_explicit_proof">here</a>.
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
Expand All @@ -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 <a href="/content/missing_cogenerator">this lemma</a> 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
Expand Down
Loading