The PR #160 motivates to add the property of having an injective cogenerator. For example, $[0,1]$ is an injective cogenerator in CompHaus, and $Q/Z$ is an injective cogenerator in Ab. Every Grothendieck abelian category has an injective cogenerator.
We also have the following result. To add it to CatDat, we should also add the new property "monomorphisms are stable under pushouts", which is very much related to the property being regular (which however talks about regular monomorphisms).
Lemma. If a category has an injective cogenerator, then monomorphisms are stable under pushouts.
Proof:
Pick an injective cogenerator $Q$. Assume we have a pushout square
i
A -----> B
| |
a| |b
v v
X -----> Y
j
in which $i : A \to B$ is a monomorphism. To show that $j : X \to Y$ is a monomorphism, take two morphisms $x,y : T \rightrightarrows X$ with $jx=jy$. Since $Q$ is a cogenerator, to show that $x=y$, it suffices to prove that $qx = qy$ for every morphism $q : X \to Q$. For any such morphism, since $Q$ is also injective, we find $f : B \to Q$ with $fi=qa$. By the universal property of the pushout, there is a (unique) morphism $g : Y \to Q$ with $gb=f$ and $gj=q$. Therefore, $qx=gjx=gjy=qy$, and we are done.
Corollary. If a category is mono-regular, has an injective cogenerator, is finitely cocomplete, and has coreflexive equalizers, then it is coregular.
This is the generalization of the proof that CompHaus is coregular from #160.
As usual, the dual properties should also be added: existence of a projective generator, and pullback-stable epimorphisms.
Maybe we should first have a PR that adds the properties pushout-stable monos and pullback-stable epis. Then, in a second PR, add the rest.
The PR #160 motivates to add the property of having an injective cogenerator. For example,$[0,1]$ is an injective cogenerator in CompHaus, and $Q/Z$ is an injective cogenerator in Ab. Every Grothendieck abelian category has an injective cogenerator.
We also have the following result. To add it to CatDat, we should also add the new property "monomorphisms are stable under pushouts", which is very much related to the property being regular (which however talks about regular monomorphisms).
Lemma. If a category has an injective cogenerator, then monomorphisms are stable under pushouts.
Proof:
Pick an injective cogenerator$Q$ . Assume we have a pushout square
in which$i : A \to B$ is a monomorphism. To show that $j : X \to Y$ is a monomorphism, take two morphisms $x,y : T \rightrightarrows X$ with $jx=jy$ . Since $Q$ is a cogenerator, to show that $x=y$ , it suffices to prove that $qx = qy$ for every morphism $q : X \to Q$ . For any such morphism, since $Q$ is also injective, we find $f : B \to Q$ with $fi=qa$ . By the universal property of the pushout, there is a (unique) morphism $g : Y \to Q$ with $gb=f$ and $gj=q$ . Therefore, $qx=gjx=gjy=qy$ , and we are done.
Corollary. If a category is mono-regular, has an injective cogenerator, is finitely cocomplete, and has coreflexive equalizers, then it is coregular.
This is the generalization of the proof that CompHaus is coregular from #160.
As usual, the dual properties should also be added: existence of a projective generator, and pullback-stable epimorphisms.
Maybe we should first have a PR that adds the properties pushout-stable monos and pullback-stable epis. Then, in a second PR, add the rest.