# implications

id: malcev_additive_criterion
type: category
proof:
See Prop. 2.2.13. 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>.


id: malcev_implies_unital
type: category
proof:
This follows from Corollary 2.2.10 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>. The proof is also written down in <a href="https://math.stackexchange.com/a/5034834/1650" target="_blank">MSE/5033161</a>.


id: biproducts_unital
type: category
proof:
For all objects $X,Y$ the morphism $X \sqcup Y \to X \times Y$ is an isomorphism, hence a strong epimorphism.


id: nno_criterion
type: category
proof:
Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. We define $z \coloneqq i_1 : 1 \to N$ and $s : N \to N$ by $s \circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$, $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$. The condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. This recursively defines the morphisms $\phi_n$. (We are basically using that $\IN$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.


id: nno_pointed_case
type: category
proof:
Let $(N,z,s)$ be a natural numbers object in a category with a zero object, denoted $0$. The morphism $z : 0 \to N$ must be zero. The universal property applied to $A=1$ implies that $s : N \to N$ is an initial object in the category of endomorphisms. This exists, it is given by the identity $0 \to 0$. Therefore, $N = 0$. The general universal property now becomes: For all $f : A \to X$, $g : X \to X$ there is a unique $\Phi : A \to X$ such that $\Phi(a) = f(a)$ and $\Phi(a)=g(\Phi(a))$. Apply this to $g = 0$ to conclude $f = 0$.


id: nno_terminal
type: category
proof:
By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \id_1$ and $s = \id_1$. This precisely means that for all $f : A \to X$ and $g : X \to X$ there is a unique $\Phi : A \to X$ with $\Phi = f$ and $\Phi = g \circ \Phi$. In other words, we have $f = g \circ f$, and therefore $g = \id_X$ (take $f = \id_X$), which proves the claim. (From here one can further deduce that the category is thin.)


id: locally_finitely_presentable_consequence
type: category
proof:
Special case of <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Prop. 1.59 with $\lambda = \aleph_0$.


id: accessible_trivial_consequence
type: category
proof:
For a $\kappa$-accessible category, the set $G$ appearing in the definition gives a small dense full subcategory, which is in particular a generating set.


id: accessible_well-powered
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/accessible+category#wellpoweredness_and_wellcopoweredness" target="_blank">nLab</a>.


id: accessible_locally_small
type: category
proof:
See the proof of Prop. 2.1.5 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.


id: accessible_well-copowered
type: category
proof:
See Thm. 2.49 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> or Prop. 6.1.3 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.


id: finite_accessible
type: category
proof:
See <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.


id: locally_presentable_essentially_small
type: category
proof:
This follows from <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.64.


id: grothendieck_abelian_presentable
type: category
proof:
See <a href="https://arxiv.org/abs/1409.7051" target="_blank">Deriving Auslander's formula</a>, Cor. 5.2, or <a href="https://arxiv.org/abs/math/0102087" target="_blank">Sheafifiable homotopy model categories</a>, Prop. 3.10.


id: locally_strongly_finitely_presentable_raise
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Cor. 3.7.


id: finitely_accessible_raise
type: category
proof:
This is because any regular cardinal is strictly smaller than its successor cardinal. See <a href="https://ncatlab.org/nlab/show/sharply+smaller+cardinal" target="_blank">nLab</a>.


id: accessible_require_Cauchy_complete
type: category
proof:
This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Prop. 2.2.1.


id: countably_accessible_criterion
type: category
proof:
The proof is similar to Thm. 2.2.2 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a> (which only establishes $\aleph_2$-accessibility) and to <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a> (which concerns $\aleph_0$-accessibility in the finite case).

Let $\C$ be a category that is locally finite, essentially countable, and Cauchy complete. By replacing $\C$ with an equivalent category if necessary, we may assume that it is countable and that all Hom-sets are finite <i>sets</i>. Let $\I$ be an $\aleph_1$-filtered category and let $D : \I \to \C$ be a diagram. We will prove that the colimit of $D$ exists and is a retract of some $D(i)$, in fact for arbitrarily large $i$. (Note that one cannot in general prove that it is isomorphic to some $D(i)$; this is false.) It follows that $\aleph_1$-filtered colimits exist and that every object of $\C$ is $\aleph_1$-presentable.

Let $X \in \C$ be a fixed object. Then $$F \coloneqq \Hom(X,D(-)) : \I \to \FinSet$$ is a diagram of finite sets. Regard it as a diagram in $\Set$ and let $L \in \Set$ be its colimit. Thus, for every $i \in \I$ we have maps $u_i : F(i) \to L$ that are jointly surjective, and two elements in $F(i)$ and $F(j)$ become equal in $L$ iff there exists a cospan $i \to k \leftarrow j$ such that these elements map to the same element in $F(k)$.

We claim that $L$ is finite. Otherwise, there would exist infinitely many pairwise distinct elements $l_1,l_2,\dotsc$ in $L$. Choose objects $i_1,i_2,\dotsc \in \I$ such that $l_n$ has a preimage in $F(i_n)$. Since $\I$ is $\aleph_1$-filtered, there exists a cocone $(i_n \to j)_{n \geq 1}$ in $\I$. We then obtain preimages $a_1,a_2,\dotsc$ in $F(j)$, which must be pairwise distinct because $l_1,l_2,\dotsc$ are pairwise distinct. This contradicts the finiteness of $F(j)$. Therefore, $L$ is finite.

For every element of the finite set $L$, choose a preimage in some $F(i)$. Since $\I$ is filtered, there exists $i \in \I$ that works for all elements simultaneously. Equivalently, the canonical map $F(i) \to L$ is surjective.

Now consider the free cocompletion $Y : \C \hookrightarrow \widehat{\C} = [\C^{\op},\Set]$ and the colimit $D_\infty \in \widehat{\C}$ of the diagram $Y \circ D$. Since colimits in $\widehat{\C}$ are computed objectwise, $$D_\infty(X) = \colim_{i \in \I} \Hom(X,D(i)).$$ We have shown above that $D_\infty(X)$ is finite and that there exists some $i_X \in \I$ such that the canonical map $$u_{i_X}(X) : \Hom(X,D(i_X)) \to D_\infty(X)$$ is surjective. Since $\C$ is countable and $\I$ is $\aleph_1$-filtered, there exists a cocone $(i_X \to j)_{X \in \C}$ in $\I$. It follows that $$u_j(X) : \Hom(X,D(j)) \to D_\infty(X)$$ is surjective for all $X \in \C$. Equivalently, $u_j : Y(D(j)) \to D_\infty$ is an epimorphism in $\widehat{\C}$. For every morphism $j \to j'$, the map $u_{j'}$ is likewise an epimorphism. We will now show that some $u_{j'}$ is in fact a split epimorphism in $\widehat{\C}$.

For every $X \in \C$, since $u_j(X)$ is a surjective map of finite sets, there exists a map $$v(X) : D_\infty(X) \to \Hom(X,D(j))$$ such that $u_j(X) \circ v(X) = \id_{D_\infty(X)}$. The issue is that $v$ need not be natural in $X$. To analyze this, let $f : X \to Y$ be a morphism in $\C$. Then we have a diagram of finite sets: $$\begin{CD} D_\infty(Y) @>{v(Y)}>> \Hom(Y,D(j)) @>{u_j(Y)}>> D_\infty(Y) \\ @V{f^*}VV @V{f^*}VV @VV{f^*}V \\ D_\infty(X) @>>{v(X)}> \Hom(X,D(j)) @>>{u_j(X)}> D_\infty(X) \end{CD}$$ The outer rectangle commutes, and the square on the right commutes. Hence, the square on the left commutes after composition with $u_j(X)$. Since $D_\infty(Y)$ is finite, it follows that there exists some morphism $j \to j'$ such that the left square commutes after composition with $$\Hom(X,D(j \to j')) : \Hom(X,D(j)) \to \Hom(X,D(j')).$$ A priori, the index $j'$ depends on the morphism $f : X \to Y$. However, since $\I$ is $\aleph_1$-filtered and $\C$ has only countably many morphisms, we may choose $j'$ independently of $f$. Thus, by construction, $$w(X) \coloneqq \Hom(X,D(j \to j')) \circ v(X) : D_\infty(X) \to \Hom(X,D(j'))$$ is natural in $X$. Moreover, $$\begin{align*} u_{j'}(X) \circ w(X) & = u_{j'}(X) \circ \Hom(X,D(j \to j')) \circ v(X) \\ & = u_j(X) \circ v(X) = \id_{D_\infty(X)}. \end{align*}$$ Therefore, $u_{j'}$ is a split epimorphism in $\widehat{\C}$. Since $\C$ is Cauchy complete, it follows that $D_\infty$ is representable, represented by a retract of $D(j')$. Since $Y$ is fully faithful, this object is a colimit of $D$.


id: locally-finitely-multi-presentable_stable-monos
type: category
proof:
Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.


id: preadditive_products_criterion
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, VIII.2., Theorem 2.


id: additive_biproducts
type: category
proof:
This is standard, see e.g. Prop. 2.1 on the <a href="https://ncatlab.org/nlab/show/additive+category" target="_blank">nLab</a>.


id: abelian_implies_regular
type: category
proof:
In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.


id: grothendieck_abelian_cogenerator
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+and+Sheaves" target="_blank">Kashiwara-Schapira</a>, Thm. 9.6.3.


id: grothendieck_abelian_self-dual
type: category
proof:
This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.


id: finitary_algebraic_consequence
type: category
proof:
This is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras.


id: algebraic_well-copowered
type: category
proof:
See <a href="https://mathoverflow.net/questions/486607" target="_blank">MSE/486607</a>. Alternatively, one may combine the facts that finitary algebraic categories are locally (finitely) presentable and that locally presentable categories are well-copowered, both of which are saved in the database. But we include the direct proof here as well, since it makes it easier to deduce the property for finitary algebraic categories appearing in practice.


id: many_sorted_algebraic_implies_regular
type: category
proof:
The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks.


id: generalized_variety_implies_accessible
type: category
proof:
See <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01, Remark 4.8(2)]</a>.


id: generalized_variety_left_cancellative
type: category
proof:
Let $\C$ be a finitely accessible left cancellative category. The proof of <a href="/category-implication/sifted_colimits_left_cancellative">this result</a> shows that every sifted diagram $\I \to \C$ factors through the preorder reflection of $\I$, and hence reduces to a filtered diagram. Since $\C$ has filtered colimits, it therefore also has sifted colimits. It follows that every functor on $\C$ preserving filtered colimits automatically preserves sifted colimits. In particular, for representable functors this means that every finitely presentable object is automatically strongly finitely presentable. Now let $G$ be a set of finitely presentable objects in $\C$ generating all objects via filtered colimits. The claim follows because every filtered colimit is sifted and the objects in $G$ are strongly finitely presentable.


id: multi-algebraic_implies_locally_finitely_multi-presentable
type: category
proof:
This is because that every (finite product, coproduct)-sketch is clearly a (finite limit, coproduct)-sketch.


id: multi-algebraic_implies_effective_congruences
type: category
proof:
This is Thm. 4.0 in <a href="https://doi.org/10.1007/BF01224953" target="_blank">Yves Diers, Catégories Multialgébriques</a> or <a href="https://translations.thosgood.net/ADM-34-1980-193.pdf" target="_blank">its English translation</a>.


id: zero-no-mono
type: category
proof:
If $f,g : A \rightrightarrows B$ are two morphisms, then $0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g$, so that $f = g$.


id: codiagonal-no-mono
type: category
proof:
For every object $A$ the codiagonal $A + A \to A$ is a split epimorphism, and by assumption a monomorphism, hence an isomorphism. Hence, the two inclusions $i_1,i_2 : A \rightrightarrows A + A$ coincide. Now, if $f, g : A \rightrightarrows B$ are two morphisms, consider the induced morphism $h : A + A \to B$ and compute $f = h \circ i_1 = h \circ i_2 = g$.


id: reflexive_pair_trivial
type: category
proof:
Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of the identity morphism on the target, and the cokernel pair of the identity morphism on the source.


id: ccc_no_strict_terminal
type: category
proof:
If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal.


id: power_construction
type: category
proof:
The power $X^I$ can be constructed as $[I \otimes 1, X]$ because $$\begin{align*} \Hom(T,[I \otimes 1, X]) & \cong \Hom(T \times (I \otimes 1),X) \\ & \cong \Hom(I \otimes (T \times 1),X) \\ & \cong \Hom(I \otimes T,X) \\ & \cong \Hom(T,X)^I. \end{align*}$$ In the second isomorphism we have used that $T \times -$ preserves copowers, which is true because it is a left adjoint.


id: lcc_implies_regular
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Lemma A1.5.13. From this it follows also that every elementary topos is regular.


id: cartesian_closed_thin_criterion
type: category
proof:
This is an application of the adjoint functor theorem. Specifically, if $P$ is a complete lattice in which $\sup_i \inf(t,x_i) = \inf(t, \sup_i y_i)$ always holds, then the functor $\inf(t,-)$ is a left adjoint because it preserves all suprema.


id: sequential_implies_lcc
type: category
proof:
Each slice is thin, semi-strongly connected, and has a terminal object. Thus, it corresponds to a linear order with a largest element $1$. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.


id: cartesian_closed_thin_implies_lcc
type: category
proof:
In a thin category, every object is subterminal. Thus, the result follows from Corollary 6 <a href="/content/subcategories">here</a>.


id: complete_characterization
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Thm. 2.


id: finitely_complete_characterization
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Cor. 1.


id: multi-terminal_with_connected
type: category
proof:
Let $(T_i)_{i\in I}$ be a multi-terminal object in a connected category $\C$. By definition of multi-terminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.


id: multi-complete_with_initial_object
type: category
proof:
Let $\C$ be a category with an initial object, and let $D : \I \to \C$ be a small diagram in $\C$. Since $\C$ has an initial object, the category $\Cone(D)$ of cones over $D$ also has an initial object. In particular, $\Cone(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object. In other words, a multi-limit of $D$ is automatically a limit of $D$.


id: regular_well-powered_well-copowered
type: category
proof:
The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$.


id: regular_balanced_epi-regular
type: category
proof:
Given any epimorphism $f : X \twoheadrightarrow Y$ in a regular category, we have the factorization into a regular epimorphism $X \twoheadrightarrow \im(f)$ followed by a monomorphism $\im(f) \hookrightarrow Y$. Because the composition is an epimorphism, the monomorphism $\im(f) \hookrightarrow Y$ must also be an epimorphism, and therefore an isomorphism. It follows that $f$ is in fact a regular epimorphism.


id: congruence_quotients_are_reflexive_coequalizers
type: category
proof:
A congruence $E \rightrightarrows X$ has a common section $X \to E$ given by the reflexivity morphism.


id: cokernels_via_congruence_quotients
type: category
proof:
By the regularity assumption, it suffices to consider cokernels of subobjects. Given a subobject $Y$ of $X$, we have the congruence on $X$ given by the pullback of ${-} : X \times X \to X$ and $Y$. The quotient of this congruence is a cokernel of $Y \hookrightarrow X$.


id: congruence_quotients_via_cokernels
type: category
proof:
For any congruence $E$ on an object $X$ of a preadditive category, let $E_0$ be the kernel of $p_2 : E \to X$.  The restriction of $p_1$ to $E_0$ is a monomorphism.  We can then see that $E$ must be the pullback of $p_1 - p_2 : E \to X$ and $E_0 \hookrightarrow X$.  Then the cokernel of $E_0 \hookrightarrow X$ is a quotient of $E$.


id: core-hin_quotients
type: category
proof:
If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \id$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \id$ and $p_2 \circ r \circ p_1 = p_2 \circ \id$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \id$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\id_X$.


id: preadditive_kernels_normal_imply_effective_congruences
type: category
proof:
Let $f, g : E \rightrightarrows X$ be a congruence. Then let $E_0$ be the kernel of $g$. We see that $f|_{E_0} : E_0 \to X$ is a monomorphism. Let $f|_{E_0}$ be the kernel of a morphism $h : X \to Y$. We claim that $E$ is also the kernel pair of $h$.
To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$. Then we have $$\begin{align*} (x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\ & \iff x_1 - x_2 \in E_0 \\ & \iff h(x_1 - x_2) = 0 \\ & \iff h(x_1) = h(x_2). \end{align*}$$ In particular, applying the forward implications in the case $T \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq g$, we conclude that $h \circ f = h \circ g$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square.


id: additive_effective_congruences_imply_normal
type: category
proof:
Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E \coloneqq X \times Y$ with maps $f, g : E \rightrightarrows X$ defined by $f : (x, y) \mapsto x+i(y)$ and $g : (x, y) \mapsto x$. It is straightforward to check that $f$ and $g$ are jointly monomorphic. Now $E$ is a congruence because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$.


id: regular_effective_congruences_implies_quotients
type: category
proof:
We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient.


id: regular_epi-regular_extensive_consequences
type: category
proof:
Suppose we have a coreflexive corelation $$X+X' \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$ on $X$, where we let $X'$ be an isomorphic copy of $X$ for clarity below. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. That means that for a generalized element $x \in X(T)$, $x \in Y(T)$ if and only if $p(x) = p(x')$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer $K$ of $$p \circ \pi_1,\, p\circ \pi_2 : (X+X') \times (X+X') \rightrightarrows E,$$ where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X') \times (X+X')$, i.e. the four copies of $X \times X$.
On the $X\times X$ quadrant, for generalized elements $x_1, x_2 \in X(T)$, we have $(x_1, x_2) \in K(T)$ if and only if $p(x_1) = p(x_2)$. Since $p\circ i_1$ is a split monomorphism, this is equivalent to $x_1 = x_2$. Thus, the $X\times X$ quadrant of $K$ is the diagonal of $X$. On the $X\times X'$ quadrant, we have $(x_1, x_2')\in K(T)$ if and only if $p(x_1) = p(x_2')$. Since $r(p(x_1)) = x_1$ and $r(p(x_2')) = x_2$, this condition implies $x_1 = x_2$; and then by definition of $Y$, $x_1 = x_2 \in Y(T)$. The converse is straightforward. Thus, the $X\times X'$ quadrant of $K$ is the diagonal of $Y$. Similarly, the $X'\times X$ quadrant of $K$ is the diagonal of $Y$, and the $X'\times X'$ quadrant of $K$ is the diagonal of $X$. Thus, we get that a morphism $h : X+X' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y')$ for every $y \in Y$; $h(y') = h(y)$ for every $y\in Y$; and $h(x') = h(x')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \inc_Y$ and $i_2 \circ \inc_Y$. This means that $E$ is an effective cocongruence.

Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is Example 2.2.18 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>. An alternative proof of this special case is given later in A.5.17.


id: pretopos_balanced
type: category
proof:
Let $\alpha : A \hookrightarrow B$ be a monomorphism. Let $B'$ be a copy of $B$, and likewise let $A'$ be a copy of $A$. Consider the congruence on $B + B'$ generated by $y \sim y'$ for $y \in A$. Formally, we define $$E \coloneqq B + B' + A + A'$$ and define the two morphisms $$f, g : E \rightrightarrows B + B'$$ by extending the identity on $B + B'$ and  $$\begin{align*} f(y) & = \alpha(y), & f(y') & = \alpha(y)', \\ g(y) & = \alpha(y)', & g(y') & = \alpha(y), \end{align*}$$ on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B'$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x')$ if and only if $x = f(e)$, $x' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$.


id: strongly_connected_pointed_criterion
type: category
proof:
By assumption there is a morphism $1 \to 0$. There is also a unique morphism $0 \to 1$. They are necessarily inverse to each other.


id: disjoint_coproducts_thin_trivial
type: category
proof:
For every object $A$ the two inclusions $A \rightrightarrows A + A$ must be equal, so their equalizer is $A$, but also $0$ since the coproduct is disjoint. Hence $A = 0$.


id: disjoint_coproducts_strict
type: category
proof:
Let $1$ be the strict terminal object, and let $A$ be any object. Then $1 \to A + 1$ is an isomorphism, since $1$ is strict. Also, $A \to A + 1$ is a monomorphism by assumption. It follows that the unique morphism $u : A \to 1$ is a monomorphism. For all $f,g : B \to A$ we have $uf = ug$ (since $1$ is terminal), hence $f = g$.


id: strongly_connected_disjoint_products
type: category
proof:
See <a href="https://math.stackexchange.com/a/5132300/1650" target="_blank">MSE/5130190</a> for a proof.


id: disjoint_coproduct_cogenerator
type: category
proof:
Assume that $S$ is a cogenerating set and let $Q \coloneqq \coprod_{X \in S} X$. For $X \in S$ we have a monomorphism $i_X : X \to Q$. If $f,g : A \rightrightarrows B$ are two distinct morphisms, there is some $X \in S$ and a morphism $h : B \to X$ with $hf \neq hg$. Hence, $i_X h f \neq i_X h g$. This proves that $Q$ is a cogenerator.


id: distributive_consequence
type: category
proof:
See the <a href="https://ncatlab.org/nlab/show/distributive+category" target="_blank">nLab</a> or Prop. 3.4 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.


id: distributive_criterion
type: category
proof:
Each functor $A \times -$ is left adjoint and hence preserves finite coproducts (in fact, all colimits).


id: countably_distributive_criterion
type: category
proof:
Each functor $A \times -$ is left adjoint and hence preserves countable coproducts (in fact, all colimits).


id: countably_distributive_filtered_criterion
type: category
proof:
Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all countable coproducts.


id: distributive_duality
type: category
proof:
This is equivalent to the classical result that the <a href="https://en.wikipedia.org/wiki/Distributive_lattice" target="_blank">distributivity law in a lattice</a> can be defined in two ways, see e.g. Birkhoff, <i>Lattice Theory</i>, Ch. IX, Thm. 1.


id: equalizers_criterion
type: category
proof:
The equalizer of $f,g : X \rightrightarrows Y$ is the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$.


id: equalizers_via_coreflexive_equalizers
type: category
proof:
If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\id_X,f), (\id_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\id_X,f)$ and $(\id_X,g)$. Thus, their equalizers agree.


id: equalizers_consequence
type: category
proof:
If $e : X \to X$ is an idempotent, then the equalizer of $e, \id_X : X \rightrightarrows X$ provides a splitting of $e$.


id: reflexive_pair_trivial_2
type: category
proof:
Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.


id: one-way_reflexive
type: category
proof:
Every reflexive pair is equal: If $f s = g s = \id$, then since $s f  = \id$ (one-way), we must have $f = s^{-1}$, and likewise $g = s^{-1}$.


id: exact_filtered_colimits_monos
type: category
proof:
This is because $f : X \longrightarrow Y$ is a monomorphism iff the diagram $$\begin{CD} X @>{\id}>> X \\ @V{\id}VV @VV{f}V \\ X @>>{f}> Y \end{CD}$$ is a pullback, and if a functor preserves finite limits, it preserves pullbacks in particular.


id: biproducts_cartesian_filtered_colimits
type: category
proof:
If $I$ is a finite set, the product functor $\C^I \to \C$ is isomorphic to the coproduct functor $\C^I \to \C$, hence preserves <i>all</i> colimits that exist in $\C$.


id: extensive_cocartesian_cofiltered_limits
type: category
proof:
Let $\C$ be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor $\C \times \C \cong \C/1 \times \C/1 \to \C/(1+1)$ is an equivalence. The forgetful functor $\C/A \to \C$ creates connected limits, and hence preserves cofiltered limits. For every $X \in \C$ the functor $(X,-) : \C \to \C \times \C$ also preserves cofiltered limits. The composition of these functors is $X \sqcup - : \C \to \C$ and therefore also preserves cofiltered limits.


id: CIP_criterion
type: category
proof:
Let $(X_i)_{i \in I}$ be a family of objects. For every finite subset $E \subseteq I$ the canonical morphism $\coprod_{i \in E} X_i = \prod_{i \in E} X_i \to \prod_{i \in I} X_i$ is a (split) monomorphism. Hence, their colimit is also a monomorphism, which is the canonical morphism $\coprod_{i \in I} X_i \to \prod_{i \in I} X_i$.


id: extensive_consequences
type: category
proof:
These are Prop. 2.6 and 2.8 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.


id: extensive_distributivity
type: category
proof:
This is Prop. 4.5 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.


id: infinitary_extensive_distributivity
type: category
proof:
One can adjust the proof of Prop. 4.5 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a> (which deals with the finite case).


id: lcc_implies_extensive
type: category
proof:
The pullback functor preserves finite coproducts because it has a right adjoint. Remark: In combination with other implication, this result implies that every elementary topos is extensive.


id: lcc_extensive_yields_infinitary
type: category
proof:
The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the <a href="https://ncatlab.org/nlab/show/extensive+category" target="_blank">nLab</a>.


id: filtered_is_sifted
type: category
proof:
Every filtered category $\C$ is inhabited and has final diagonal functors $\Delta : \C \to \C^J$ for all finite index categories $J$; in particular, it is inhabited and its diagonal $\Delta: \C \to \C \times \C$ is final.


id: coproducts_implies_sifted
type: category
proof:
The category is inhabited by assumption, and the coproduct of two objects is initial in the corresponding category of cospans.


id: sifted_left_cancellative_implies_thin
type: category
proof:
For any object $X$ in a left-cancellative category, the connected component containing $$X \xrightarrow{\id} X \xleftarrow{\id} X$$ in the category of cospans from $X$ to $X$ consists only of cospans $$X \xrightarrow{f} Y \xleftarrow{g} X$$ where $f=g$; hence when the category is also sifted, all cospans must be of this form, and so any two parallel morphisms are equal.


id: filtered-finite-thin
type: category
proof:
Let $\C$ be a thin, filtered, and w.l.o.g. finite category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal.


id: aleph1-filtered-countable-thin
type: category
proof:
Let $\C$ be a thin, $\aleph_1$-filtered, and w.l.o.g. countable category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal.


id: directed_colimits_suffice
type: category
proof:
This is Theorem 1.5. in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>.


id: sequential_colimits_consequence
type: category
proof:
Assume that $e : X \to X$ is an idempotent morphism. Consider the sequence $$X \xrightarrow{e} X \xrightarrow{e} X \to \cdots.$$ A cocone under this sequence is a family of morphisms $f_n : X \to Y$ satisfying $$f_n = f_{n+1} e.$$ Then $$f_n = f_{n+1} e = f_{n+2} e^2 = f_{n+2} e = f_{n+1}$$ shows that all the morphisms are equal. Thus, a cocone is the same as a morphism $f_0 : X \to Y$ with $f_0 = f_0 e$, meaning it coequalizes $\id_X,e : X \rightrightarrows X$. Hence, if a colimit exists, $e$ splits.


id: sequential_limits_criterion
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Prop. 3. The proof can easily be adapted to this case. Namely, the limit of $\cdots \to X_2 \to X_1 \to X_0$ is the equalizer of two suitable endomorphisms of $\prod_{n \geq 0} X_n$.


id: direct_implies_sequential_limits
type: category
proof:
Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 \coloneqq n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction.


id: finite_filtered_colimits
type: category
proof:
We may assume that the category $\C$ is finite and Cauchy complete. The answer at <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a> shows that every filtered colimit in $\C$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\C$. It follows that for every filtered diagram of morphisms $X_i \to Y_i$ their colimit $X_\infty \to Y_\infty$ exists, which is a retract of one of the $X_i \to Y_i$. Therefore, if every $X_i \to Y_i$ is a monomorphism, also $X_\infty \to Y_\infty$ is a monomorphism.


id: aleph1-filtered-colimits-include-filtered-colimits
type: category
proof:
Every $\aleph_1$-filtered category is also $\aleph_0$-filtered, i.e. filtered. Therefore, every $\aleph_1$-filtered diagram is also a filtered diagram, hence has a colimit by assumption.


id: kappa-filtered-colimits_require_Cauchy_complete
type: category
proof:
More generally, if $\kappa$ is any infinite regular cardinal, a category with $\kappa$-filtered colimits must be Cauchy cocomplete. This is because the <a href="/category/walking_idempotent">walking idempotent</a> is $\kappa$-filtered. See also <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Prop. 2.2.1.


id: sifted_colimits_consequence
type: category
proof:
This is because filtered categories are sifted and because the index category for a reflexive coequalizer is sifted.


id: sifted_colimits_criterion
type: category
proof:
See Cor. 5.2 in <a href="http://www.tac.mta.ca/tac/volumes/37/35/37-35abs.html" target="_blank">Chen's paper</a>.


id: sifted_colimits_left_cancellative
type: category
proof:
Let $D : \I \to \C$ be a sifted diagram in a left cancellative category with filtered colimits. We claim that $D(f) = D(g)$ whenever $f,g : i \rightrightarrows j$ are parallel morphisms, i.e. for the cospan $i \xrightarrow{f} j \xleftarrow{g} i$.

This is trivially true for the identity cospan. Since $\I$ is sifted, it suffices to prove that $D(f) = D(g) \iff D(f') = D(g')$ whenever there is a morphism of cospans $(f,g) \to (f',g')$. Such a morphism is given by a morphism $h : \cod(f) \to \cod(f')$ satisfying $hf = f'$ and $hg = g'$. The implication $D(f) = D(g) \implies D(f') = D(g')$ is formal, while the converse follows because $D(h)$ is a monomorphism.

It follows that the diagram $D$ factors as $\I \to \I_p \to \C$, where $\I_p$ is the preorder reflection of $\I$ (same objects, with $i \leq j$ whenever there exists a morphism $i \to j$). Since $\I$ is sifted, the preorder $\I_p$ is filtered. Hence, the diagram $\I_p \to \C$ has a colimit, and this colimit is also a colimit of the original diagram $\I \to \C$.


id: generator_via_coproduct
type: category
proof:
If $S$ is a generating set, we claim that $U \coloneqq \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.


id: free-algebra-generates
type: category
proof:
Pick an algebraic theory that represents the category. The free algebra $F(1)$ on one generator is a generator since morphisms $F(1) \to X$ correspond to the elements of (the underlying set of) the algebra $X$.


id: groupoid_with_multi-terminal
type: category
proof:
Let $f,g : A \rightrightarrows B$ be a parallel pair of morphisms. Since the category has a multi-terminal object, the connected component containing $A$ and $B$ has a terminal object. But since the category is a groupoid, both $A$ and $B$ are terminal objects in the connected component, hence $f=g$.


id: strict_initial_trivial
type: category
proof:
If $0$ is the zero object, then for every object $A$ the unique morphism $A \to 0$ is an isomorphism by assumption.


id: strict_initial_left_criterion
type: category
proof:
It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \id_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.


id: finite_products_characterization
type: category
proof:
The non-trivial direction follows since finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$.


id: products_criterion
type: category
proof:
The product $\prod_{i \in I} X_i$ is the cofiltered limit of the finite partial products $\prod_{i \in E} X_i$ where $E$ ranges over the finite subsets of $I$.


id: products_criterion_countable
type: category
proof:
The product $\prod_{i \in I} X_i$ is the $\aleph_1$-cofiltered limit of the countable partial products $\prod_{i \in C} X_i$ where $C$ ranges over the countable subsets of $I$.


id: countable_products_criterion
type: category
proof:
If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$.


id: countable_powers_criterion
type: category
proof:
We can write $X^{\IN}$ as the limit of the sequence $\cdots \to X^3 \to X^2 \to X \to 1$ with transition morphisms $f_n : X^{n+1} \to X^n$, $(x_1,\dotsc,x_{n+1}) \mapsto (x_1,\dotsc,x_n)$, i.e., $p_i f_n = p_i$ for $1 \leq i \leq n$.


id: copowers_criterion
type: category
proof:
Let $\C$ be a category with filtered colimits and finite copowers. Let $X \in \C$ be an object and $I$ be a set. The poset $P_{<\aleph_0}(I)$ of finite subsets of $I$ is filtered, and we have a diagram $P_{<\aleph_0}(I) \to \C$, $A \mapsto A \otimes X$. Its colimit is the copower $I \otimes X$.


id: copowers_criterion_countable
type: category
proof:
Let $\C$ be a category with $\aleph_1$-filtered colimits and countable copowers. Let $X \in \C$ be an object and $I$ be a set. The poset $P_{<\aleph_1}(I)$ of countable subsets of $I$ is $\aleph_1$-filtered, and we have a diagram $P_{<\aleph_1}(I) \to \C$, $A \mapsto A \otimes X$. Its colimit is the copower $I \otimes X$.


id: pullbacks_criterion
type: category
proof:
The pullback of $f : X \to S$ and $g : Y \to S$ is the equalizer of $p_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S$.


id: connected_limits_characterization
type: category
proof:
The direction $\Rightarrow$ is trivial. The direction $\Leftarrow$ can be found at the <a href="https://ncatlab.org/nlab/show/connected+limit" target="_blank">nLab</a>.


id: wide_pullbacks_criterion
type: category
proof:
To prove $\Leftarrow$, a wide pullback can be constructed as a cofiltered limit of finite pullbacks, and finite pullbacks can be reduced to binary pullbacks (the empty-indexed pullback always exists). Conversely, assume that wide pullbacks exist in $\C$. For every object $A$ then the slice category $\C / A$ has wide pullbacks and a terminal object, hence is complete. Since a cofiltered limit can be finally reduced to such a slice, we are done.


id: wide_pullbacks_finite
type: category
proof:
Each slice category has finite products and is essentially finite, hence has all products by <a href="/category-implication/freyd_finite">this result</a> followed by <a href="/category-implication/thin_finite_product_reduction">this result</a>.


id: subobject_classifier_consequence
type: category
proof:
The first part holds by convention, and the second part: any monomorphism $U \to X$ is the equalizer of $\chi_U,\chi_X : X \rightrightarrows \Omega$.


id: subobject_classifier_well-powered
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Prop. I.3.1.


id: subobject_classifier_pointed_case
type: category
proof:
The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.


id: regular_subobjects_trivial
type: category
proof:
In a right cancellative category, every regular monomorphism is an isomorphism, so that a terminal object is a regular subobject classifier.


id: regular_subobject_classifier_strict
type: category
proof:
Let $\Omega$ be a regular subobject classifier. Since $1$ is a strict terminal object, $\top : 1 \to \Omega$ is an isomorphism. This implies that every regular monomorphism is an isomorphism. Hence, by taking the equalizer of two parallel morphisms, we see that the category is thin.


id: thin_regular-subobject-trivial
type: category
proof:
For the forward direction, if $f,g : X \rightrightarrows Y$ are morphisms, their equalizer is a regular monomorphism $E \hookrightarrow X$, hence an isomorphism. But this means $f = g$. The reverse implication is trivial.


id: regular_subobject_classifier_disallows_malcev
type: category
proof:
The regular subobject classifier $\Omega$ is an internal poset (cf. <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). Concretely, since the category is Malcev, it has binary products, so the intersection of regular subobjects is again a regular subobject. Namely, the intersection of the equalizer of $f_1, g_1 : X \rightrightarrows Y_1$ with the equalizer of $f_2, g_2 : X \rightrightarrows Y_2$ is the equalizer of $(f_1, f_2), (g_1, g_2) : X \rightrightarrows Y_1 \times Y_2$. This intersection operation on regular subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is defined as the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every regular monomorphism must be an isomorphism. (From here, we can infer that the category is thin – or, if the category has a subobject classifier, that the category is trivial.)


id: disjoint_finite_coproducts_disallows_regular-subobject-trivial
type: category
proof:
For any object $X$, the unique morphism $! : 0 \to X$ is a regular monomorphism, as the equalizer of the two coprojections $X \rightrightarrows X \sqcup X$. Therefore, it is an isomorphism.


id: disjoint_finite_coproducts_disallows_regular-quotient-trivial
type: category
proof:
For any object $X$, the coequalizer of the two coprojections $X \rightrightarrows X \sqcup X$ is the codiagonal $\nabla : X \sqcup X \to X$. Therefore, these two coprojections are equal. But their equalizer is also the unique morphism $! : 0 \to X$. It follows that $! : 0 \to X$ is an isomorphism.


id: core-thin_products_thin
type: category
proof:
Let $X$ be any object. The swap $\tau : X \times X \to X \times X$ is an automorphism, hence equal to the identity. It follows that the projections $p_1,p_2 : X \times X \rightrightarrows X$ are the same. And this means that every two morphisms $Y \rightrightarrows X$ are the same.


id: thin_via_locally-finite
type: category
proof:
If $A,B$ are objects, we have a bijection $\Hom(A,B)^{\IN} \cong \Hom(A,B^{\IN})$. By assumption, this set is finite. Hence, $\Hom(A,B)$ has at most one element.


id: direct_implies_one-way
type: category
proof:
The category is one-way since any non-identity endomorphism yields an infinite sequence of equal non-identity morphisms. The category is skeletal since any non-identity isomorphism $f : A \to B$ yields the infinite sequence $\dotsc,f^{-1},f,f^{-1},f$.


id: one-way_zero
type: category
proof:
If $f,g : A \rightrightarrows B$ are two morphisms, then since $0_{B,B} = \id_B$ we have  $$f = 0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g = g.$$


id: direct_criterion
type: category
proof:
See the <a href="https://ncatlab.org/nlab/show/direct+category#direct_versus_oneway_categories" target="_blank">nLab</a> for a proof.


id: freyd_small
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Prop. 3. The proof works for any category with powers.


id: freyd_countable
type: category
proof:
Adjust the proof of <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Prop. 3.


id: thin_finite_product_reduction
type: category
proof:
The category is equivalent to a finite preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a finite one.


id: thin_countable_product_reduction
type: category
proof:
The category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one.


id: topos_consequence
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8; and <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Proposition 2.4.1.


id: topos_well-copowered_criterion
type: category
proof:
This follows from <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Theorem IV.7.8 (and Prop. I.3.1).


id: topos_implies_coregular
type: category
proof:
This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, A2.6.3.


id: grothendieck_topos_definition
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Appendix, Prop. 4.4.


id: grothendieck_topos_consequence
type: category
proof:
A Grothendieck topos is locally presentable by Prop. 3.4.16 in <a href="https://www.cambridge.org/core/books/handbook-of-categorical-algebra/5033A02442342401E7BCC26A042DAB94" target="_blank">Handbook of Categorical Algebra Vol. 3</a>, has a cogenerator (see <a href="https://ncatlab.org/nlab/show/cogenerator" target="_blank">nLab</a>) and is infinitary extensive by <a href="https://ncatlab.org/nlab/show/Giraud%27s+theorem" target="_blank">Giraud's Theorem</a>. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). Every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits (<a href="https://ncatlab.org/nlab/show/sheaf+toposes+are+equivalently+the+left+exact+reflective+subcategories+of+presheaf+toposes" target="_blank">nLab</a>), so we conclude with Lemma 3 <a href="/content/subcategories">here</a>.


id: topos_is_locally_cartesian_closed
type: category
proof:
See <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Cor. A2.3.4.


id: topos_no_stable_epis
type: category
proof:
Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.


id: right_adjoint_consequences
type: functor
proof:
This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 5.1.


id: saft
type: functor
proof:
This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the <a href="https://ncatlab.org/nlab/show/adjoint+functor+theorem" target="_blank">nLab</a>, or in <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 8.2.


id: reflector_consequences
type: functor
proof:
If $F : \C \to \D$ is a reflector, it is left adjoint to a fully faithful functor $G : \D \to \C$. Thus, the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>). This shows that $G$ is a right inverse of $F$.


id: equivalence_criterion
type: functor
proof:
This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IV, Theorem 4.1.


id: equivalence_invertible
type: functor
proof:
If a functor $F$ has a right inverse $R$ and a left inverse $L$, then $$L \cong L \circ F \circ R \cong R.$$ Hence, $R$ (and $L$) are (pseudo-)inverse to $F$.


id: preserve_finite_products_criterion
type: functor
proof:
This is because finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$. We need the assumption on the source category since otherwise $X_1 \times \cdots \times X_n$ might not exist.


id: continuous_criterion
type: functor
proof:
This follows from the construction of limits via equalizers and products, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 2.2.


id: continuous_criterion_filtered
type: functor
proof:
This is because every limit can be written as a filtered limit of finite limits, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IX, Theorem 1.1.


id: product_criterion_filtered
type: functor
proof:
This is because every product can be written as a filtered limit of finite products, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IX, Theorem 1.1.


id: left_exact_consequences
type: functor
proof:
Finite products and equalizers are special cases of finite limits. Moreover, a morphism $f : X \to Y$ is a monomorphism if and only the square $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y \end{CD}$$ is a pullback square, and pullbacks are special cases of finite limits.


id: left_exact_criterion
type: functor
proof:
This follows from the construction of finite limits via equalizers and finite products, see  <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 2.2.


id: representable_is_continuous
type: functor
proof:
This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 4.1.


id: criterion_coreflexive_equalizers
type: functor
proof:
This follows easily from <a href="/category-implication/equalizers_via_coreflexive_equalizers">this result</a> about categories and its proof.


id: another_regular-mono-preserving_criterion
type: functor
proof:
Let $F : \C \to \D$ be a functor preserving coreflexive equalizers, where $\C$ has pushouts; we only need that $\C$ has cokernel pairs. Let $i : X \to Y$ be a regular monomorphism in $\C$. By Prop. 3.2 at the <a href="https://ncatlab.org/nlab/show/regular+epimorphism#MorphismsWithKernelPairsAreRegularIffEffective" target="_blank">nLab</a>, $i$ is the equalizer of the two canonical morphisms $u_1,u_2 : Y \rightrightarrows Y \sqcup_X Y$ into the cokernel pair of $i$. By the universal property of the pushout, there is a morphism $\nabla : Y \sqcup_X Y \to Y$ with $\nabla u_1 = \nabla u_2 = \id_Y$. Thus, $u_1,u_2$ is a coreflexive pair. Since $F$ preserves coreflexive equalizers by assumption, $F(i)$ is the equalizer of $F(u_1), F(u_2)$. In particular, $F(i)$ is a regular monomorphism.


id: faithful-via-equalizers
type: functor
proof:
Let $f,g : X \rightrightarrows Y$ be two morphisms in the source category, and choose an equalizer $E \hookrightarrow X$. By assumption, $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. Thus, if $F(f) = F(g)$, then $F(E) \to F(X)$ is an isomorphism. Since $F$ is conservative, $E \to X$ is an isomorphism, which means $f = g$.


id: conservative_criterion
type: functor
proof:
If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$.


id: left-invertible_consequences
type: functor
proof:
Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is a morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.


id: monadic_consequences
type: functor
proof:
This is clear since for a monad $T$ the forgetful functor from the category of $T$-algebras has these properties.


id: crude_monadicity_theorem
type: functor
proof:
This is the crude monadicity theorem. A proof can be found in <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Thm. IV.4.2.


id: split_mono_is_regular_mono
type: morphism
proof:
Let $f : A \to B$ be a split monomorphism, and choose a morphism $g : B \to A$ with $g \circ f = \id_A$. Then it is easy to check that $f$ is an equalizer of $\id_B, f \circ g : B \rightrightarrows B$.


id: regular_epi_and_mono_is_iso
type: morphism
proof:
If $p : A \to B$ is the coequalizer of $f,g : C \rightrightarrows A$, then $p \circ f = p \circ g$. If $p$ is also a monomorphism, this implies $f = g$. But then $\id_B$ is a coequalizer of $f,g$, so that $p$ is an isomorphism.


# categories

id: FiltVect
objects:
A filtered vector space over a field $K$ consists of a vector space $V$ over $K$ together with an $\IZ$-indexed sequence of subspaces $F^n(V) \subseteq V$ satisfying $F^{n+1}(V) \subseteq F^n(V)$ for all $n \in \IZ$. $$\cdots \subseteq F^1(V) \subseteq F^0(V) \subseteq F^{-1}(V) \subseteq \cdots \subseteq V$$

morphisms:
A morphism $(V,F) \to (W,G)$ is a linear map $f : V \to W$ satisfying $f_*(F^n(V)) \subseteq G^n(W)$ for all $n \in \IZ$. We call such morphisms filtered linear maps.


id: J2
objects: pairs $(X,\alpha)$, where $X$ is a set and $\alpha : X \to X \times X$ is an isomorphism
morphisms:
A morphism $(X,\alpha) \to (Y,\beta)$ is a map $f : X \to Y$ satisfying $$(f \times f) \circ \alpha = \beta \circ f.$$


id: LRS_R
objects:
locally ringed spaces over $R \neq 0$, i.e. pairs $(X,\O_X)$ consisting of a topological space and a sheaf of commutative $R$-algebras on it whose stalks are local rings

morphisms:
A morphism $(f,f^\sharp) : (X,\O_X) \to (Y,\O_Y)$ consists of a continuous map $f : X \to Y$ and a homomorphism $f^\sharp : \O_Y \to f_* \O_X$ of sheaves of $R$-algebras such that for every $x \in X$ the induced map on stalks $f_x : \O_{Y,f(x)} \to \O_{X,x}$ is local.


id: M-Set
objects: sets with a left action of a monoid $M$
morphisms:
maps that are compatible with the $M$-action, meaning $f(m \cdot x)=m \cdot f(x)$, also called $M$-maps


id: Pos
morphisms: order-preserving functions
objects:
partially ordered sets (aka posets), i.e. sets equipped with a reflexive, transitive, antisymmetric relation


id: Sch_R
morphisms: morphisms of locally ringed spaces over $R$
objects:
schemes over $R \neq 0$, i.e. locally ringed spaces over $R$ that have an open covering by affine schemes over $R$


id: Set_arrow
objects: triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \to Y$ is a function
morphisms:
a morphism $(X, Y, f) \to (X', Y', f')$ is a pair of functions $\ell : X \to X'$ and $r : Y \to Y'$ making a commutative square $$\begin{CD} X @>{f}>> Y \\ @V{\ell}VV @VV{r}V \\ X' @>>{f'}> Y' \end{CD}$$


id: Set_f
objects: sets
morphisms:
maps $f : X \to Y$ with the property that for every $y \in Y$ the fiber $f^*(\{y\})$ is a finite set


id: Sp
morphisms: natural transformations
objects:
combinatorial species, defined as functors $\IB \to \FinSet$, where $\IB$ is the category of finite sets and bijections


id: sSet
morphisms: natural transformations
objects:
simplicial sets, i.e. functors $\Delta^{\op} \to \Set$ where <a href="/category/Delta">$\Delta$</a> denotes the simplex category.


id: walking_coreflexive_pair
objects: two objects $[0]$ and $[1]$
morphisms:
the identities, two morphisms $i,j : [0] \rightrightarrows [1]$, a morphism $p : [1] \to [0]$ with $p i = p j = \id_{[0]}$, and the two idempotent morphisms $ip, jp : [1] \to [1]$.


id: walking_fork
objects: three objects $0,1,2$
morphisms:
one morphism $i : 0 \to 1$, two morphisms $f,g : 1 \rightrightarrows 2$, one morphism $0 \to 2$ (namely, $f \circ i = g \circ i$), and the identities


id: walking_splitting
objects: two objects $0$ and $1$
morphisms:
the identities, morphisms $i : 0 \to 1$, $p : 1 \to 0$ satisfying $pi = \id_0$, and the idempotent $ip : 1 \to 1$.


# special_objects

category_id: Ban
type: coproducts
description:
The coproduct of a family of Banach spaces $(X_i,|{-}|)_{i \in I}$ is the subspace $\bigl\{x \in \prod_{i \in I} X_i : \sum_{i \in I} |x_i| < \infty\bigr\}$ of their vector space product equipped with the $1$-norm $|x|_1 \coloneqq \sum_{i \in I} |x_i|$.


category_id: Ban
type: products
description:
The product of a family of Banach spaces $(X_i,|{-}|)_{i \in I}$ is the subspace $\bigl\{x \in \prod_{i \in I} X_i : \sup_{i \in I} |x_i| < \infty\bigr\}$ of their vector space product equipped with the $\sup$-norm $|x|_\infty \coloneqq \sup_{i \in I} |x_i|$.


category_id: CompHaus
type: coproducts
description:
Stone-Čech compactification of the disjoint union with the disjoint union topology (in the finite case, the disjoint union is already compact Hausdorff so Stone-Čech compactification is not necessary)


category_id: CompHaus
type: products
description:
direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a> (which is compact by the Tychonoff product theorem)


category_id: FiltVect
type: coproducts
description:
direct sums of the underlying vector spaces equipped with the filtration $F^n(\bigoplus_i V_i) \coloneqq \bigoplus_i F^n(V_i)$


category_id: FiltVect
type: products
description:
direct products of the underlying vector spaces equipped with the filtration $F^n(\prod_i V_i) \coloneqq \prod_i F^n(V_i)$


category_id: Haus
type: products
description:
direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a>


category_id: J2
type: coproducts
description:
See <a href="https://matheplanet.de/matheplanet/nuke/html/article.php?sid=1713" target="_blank">here</a> for a description


category_id: Man
type: products
description:
[finite case] direct products $X \times Y$ with the product topology and the charts $\IR^{n + m} = \IR^n \times \IR^m \cong U \times V \hookrightarrow X \times Y$ for charts $\IR^n \cong U \hookrightarrow X$ and $\IR^m \cong V \hookrightarrow Y$


category_id: Meas
type: products
description:
direct products with the <a href="https://de.wikipedia.org/wiki/Produkt-%CF%83-Algebra" target="_blank">product $\sigma$-algebra</a>


category_id: Met_c
type: coproducts
description:
Given metric spaces $(X_i,d_i)$ with $d_i \leq 1$ w.l.o.g, we endow the disjoint union $\coprod_i X_i$ with the metric $d$ that extends the metrics $d_i$ and satisfies $d(x,y) = 1$ when $x,y$ are in different $X_i$.


category_id: Met_c
type: products
description:
[countable case] In the finite case, take direct products with the metric $d(x,y) = \sup_i d_i(x_i,y_i)$, but other metrics such as $d(x,y) = \sum_i d_i(x_i,y_i)$ also work. In the countable case, one can assume $d_i \leq 1$ and then define $d(x,y) = \sum_i d_i(x,y) / 2^i$.


category_id: Met_oo
type: coproducts
description:
disjoint union with the metric that extends the given ones and gives points in different spaces the distance $\infty$


category_id: Sch_R
type: products
description:
[finite case] The idea is to use $\Spec(A) \times \Spec(B) = \Spec(A \otimes_R B)$ and then to glue affine pieces together. See EGA I, Chap. I, Thm. 3.2.1.


category_id: SemiGrp
type: coproducts
description:
similar to free products of monoids, but where the empty word is not allowed, and of course we do (and can) not demand that the factors are $\neq 1$


category_id: Sh(X)
type: initial object
description:
constant sheaf with value $\varnothing$, sending all non-empty open sets to $\varnothing$ and the empty set to a singleton


category_id: Top_*
type: products
description:
direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a> and the obvious base point


# special_morphisms

category_id: Ab
type: monomorphisms
description: injective homomorphisms
proof:
This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.


category_id: Ab
type: epimorphisms
description: surjective homomorphisms
proof:
For the non-trivial direction, if $f : A \to B$ is an epimorphism, then $p \circ f = 0$ for the projection  $p : B \to B/f(A)$ implies that $p = 0$, so that $B = f(A)$.


category_id: Ab_fg
type: monomorphisms
description: injective homomorphisms
proof:
Let $f : A \to B$ be a monomorphism of finitely generated abelian groups. Let $a \in A$ be in the kernel of $a$. Then we may view $a$ as a morphism $a : \IZ \to A$ with $f \circ a = 0$, and $\IZ$ is finitely generated. Hence, $a = 0$.


category_id: BN
type: isomorphisms
description: only the number $0$
proof:
The $0$ is the only natural number which has an additive inverse, since for $n > 0$ we have $n + m > 0$ for all $m$.


category_id: BOn
type: isomorphisms
description: only the ordinal $0$
proof:
The $0$ is the only ordinal which has an additive inverse, since for $\alpha > 0$ we have $\alpha + \beta > 0$ for all $\beta$.


category_id: BOn
type: regular monomorphisms
description: ordinals of the form $\alpha \cdot \omega$, where $\alpha$ is any ordinal
proof:
This results from the proof that equalizers exist, see <a href="https://math.stackexchange.com/questions/5029668" target="_blank">MSE/5029668</a>.


category_id: Ban
type: monomorphisms
description: injective linear contractions
proof:
The unit ball functor $U : \Ban \to \Set$ is faithful and representable (by $\IC$), hence reflects and preserves monomorphisms.


category_id: Ban
type: epimorphisms
description: linear contractions with dense image
proof:
Let $f : X \to Y$ be an epimorphism of Banach spaces. The subspace $U \coloneqq \overline{f(X)} \subseteq Y$ is closed. It is well-known that the quotient $Y/U$ is also a Banach space with a projection $p : Y \to Y/U$. Since $p \circ f = 0 = 0 \circ f$, we infer $p = 0$, so that $U = Y$.


category_id: Ban
type: regular monomorphisms
description:
For a linear contraction $f : X \to Y$ the following are equivalent: (1) $f$ is a regular monomorphism. (2) $f$ is isometric. (3) $f$ is isomorphic to the inclusion of a closed subspace of $Y$.

proof:
(1) implies (2): This follows immediately from the concrete construction of equalizers.
(2) implies (3): The image of $f$ is complete, hence closed. The rest is clear.
(3) implies (1): If $U \subseteq Y$ is a closed subspace, then the inclusion is the kernel of the projection $Y \to Y/U$, where $Y/U$ is the <a href="https://math.stackexchange.com/questions/319867" target="_blank">well-known</a> quotient Banach space.


category_id: Ban
type: regular epimorphisms
description:
For a linear contraction $f : X \to Y$ the following are equivalent: (1) $f$ is a regular epimorphism. (2) The norm on $Y$ is given by $|y| = \inf \{|x| : f(x) = y\}$. (3) $f$ maps the open unit ball of $X$ onto the open unit ball of $Y$.

proof:
First of all, notice that all three conditions imply that $f$ is surjective.
(1) implies (2): This follows immediately from the concrete construction of coequalizers, and the quotient Banach space in particular.
(2) implies (1): Let $U \coloneqq \ker(f)$. Then $U$ is a closed subspace of $X$, and $f$ induces a bijective linear contraction $\tilde{f} : X/U \to Y$. It is isometric by assumption on $f$ and the definition of the norm on $X/U$. Thus, $\tilde{f}$ is an isomorphism. Since $X/U$ is the cokernel of $U \hookrightarrow X$, it follows that $f$ is a regular epimorphism.
(2) implies (3): Let $y \in Y$ be an element with $|y| < 1$. Since $|y|$ is the infimum of all $|x|$ with $f(x)=y$, there is some $x$ with $f(x)=y$ and $|x| < 1$.
(3) implies (2): Let $y \in Y$. Since $f$ is a linear contraction, the inequality $|y| \leq \inf \{|x| : f(x) = y\}$ holds. Let $\varepsilon > 0$. Consider $y' \coloneqq y / (|y| + \varepsilon)$. Then $|y'| < 1$. Thus, by assumption, there is some $x' \in X$ with $|x'| < 1$ and $f(x') =y'$. Let $x \coloneqq (|y| + \varepsilon) x'$. Then $f(x) = y$ and $|x| < |y| + \varepsilon$. Thus, the infimum in question is $\leq |y| + \varepsilon$, for every $\varepsilon > 0$, and hence $\leq |y|$.


category_id: CAlg(R)
type: epimorphisms
description: a homomorphism of algebras which is an epimorphism of commutative rings
proof:
The forgetful functor $\CAlg(R) \to \CRing$ is faithful and hence reflects epimorphisms, but it also preserves epimorphisms since it preserves pushouts (since $\CAlg(R) \cong R / \CRing$). For epimorphisms of commutative rings see the page for <a href="/category/CRing">$\CRing$</a>.


category_id: CMon
type: epimorphisms
description:
A morphism in $\CMon$ is an epimorphism iff it is an epimorphism in $\Mon$, which in turn can be characterized by <a href="https://en.wikipedia.org/wiki/Isbell's_zigzag_theorem" target="_blank">Isbell's zigzag theorem</a>.

proof:
If $f : M \to N$ is a homomorphism of commutative monoids which is an epimorphism in $\Mon$, then it is trivially also an epimorphism in $\CMon$. The converse requires a proof, which can be found at <a href="https://math.stackexchange.com/a/5133596/1650">MSE/5133488</a>.
	


category_id: CRing
type: epimorphisms
description:
A ring map $f : R \to S$ is an epimorphism iff $S$ equals the <i>dominion</i> of $f(R) \subseteq S$, meaning that for every $s \in S$ there is some matrix factorization $(s) = Y X Z$ with $X \in M_{n \times n}(R)$, $Y \in M_{1 \times n}(S)$, and $Z \in M_{n \times 1}(S)$.

proof:
See <a href="https://stacks.math.columbia.edu/tag/04VM" target="_blank">Stacks Project</a> ,or, for many more results, the seminar <a href="https://www.numdam.org/issues/SAC_1967-1968__2_/">Les épimorphismes d'anneaux</a>. See also <a href="https://mathoverflow.net/questions/109/" target="_blank">MO/109</a> for some results.


category_id: Cat
type: monomorphisms
description: faithful functors that are injective on objects
proof:
Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : 1 \to \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \to B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \to \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.


category_id: Cat
type: epimorphisms
description:
A functor $F : \C \to \D$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\D$ there is a zigzag over $U \coloneqq F(\C)$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \D$ and $y_1,\dotsc,y_m \in \D$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.

proof:
This is an extension of the <a href="https://en.wikipedia.org/wiki/Isbell's_zigzag_theorem" target="_blank">corresponding theorem for monoids</a> and proven in <a href="https://www.jstor.org/stable/2373286" target="_blank">Epimorphisms and Dominions, III</a> by John R. Isbell.


category_id: CompHaus
type: monomorphisms
description: injective continuous maps (which are automatically closed embeddings)
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. To prove the parenthetical remark, given an injective continuous function $f : X \to Y$ between compact Hausdorff spaces, the image of $f$ is a closed subset. Also, the induced map from $X$ to $\im(f)$ with the subspace topology is a bijective continuous map between compact Hausdorff spaces, so it is a homeomorphism.


category_id: CompHaus
type: epimorphisms
description: surjective continuous maps (which are automatically quotient maps)
proof:
For the non-trivial direction, and for a proof of the parenthetical remark, see the proof above that $\CompHaus$ is epi-regular.


category_id: Delta
type: isomorphisms
description: bijective order-preserving maps
proof:
This is easy. Notice that bijective order-preserving maps automatically also reflect the order (because we work with totally ordered sets).


category_id: Delta
type: monomorphisms
description: injective order-preserving maps
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.


category_id: Delta
type: epimorphisms
description: surjective order-preserving maps
proof:
We can use the same proof as for <a href="/category/FinOrd">$\FinOrd$</a> since this has merely used the non-empty ordered set $\{0 < 1\}$.


category_id: FI
type: epimorphisms
description: bijective maps
proof:
Take an epimorphism $X \to Y$ in this category, w.l.o.g. the inclusion of a subset $X \subseteq Y$. This means that for two injective maps $f,g : Y \rightrightarrows T$ with $f|_X = g|_X$ we must have $f = g$. Let $T \coloneqq Y + (Y \setminus X)$ (disjoint union), $f$ be the inclusion into the first summand, $g|_X$ be the inclusion into the first summand, and $g|_{Y \setminus X}$ be the inclusion into the second summand. Then $f$ and $g$ are injective with $f|_X = g|_X$, so that $f = g$. But this means $X = Y$.


category_id: FS
type: monomorphisms
description: bijective maps
proof:
Assume that $f : X \to Y$ is a monomorphism in this category. If $a,b \in X$ are such that $a \neq b$ but $f(a) = f(b)$, let $h : X \to X$ be the transposition that swaps $a$, $b$. Then $f \circ \id_X = f = f \circ h$, so by assumption $\id_X = h$, a contradiction. This shows that $f$ is bijective.


category_id: FiltVect
type: isomorphisms
proof: This is straightforward to verify.
description:
A filtered linear map $f : (V,F) \to (W,G)$ is an isomorphism if $f : V \to W$ is bijective and $f_*(F^n(V)) = G^n(W)$ for all $n \in \IZ$.


category_id: FiltVect
type: monomorphisms
description: injective filtered linear maps
proof:
For the non-trivial direction, the forgetful functor $\FiltVect \to \Set$ is representable (by $K$ equipped with the trivial filtration), and therefore preserves monomorphisms.


category_id: FiltVect
type: epimorphisms
description: surjective filtered linear maps
proof:
We saw above that the category has cokernels, and that these are preserved by the forgetful functor to $\Vect$. Moreover, a morphism is an epimorphism if and only if its cokernel is zero, and a filtered vector space is zero if and only if its underlying vector space is zero. Therefore, the claim follows from the classification of epimorphisms in $\Vect$.


category_id: FiltVect
type: regular monomorphisms
description:
A filtered linear map $f : (V,F) \to (W,G)$ is a regular monomorphism if and only if $f : V \to W$ is injective and $F^n(V) = f^*(G^n(W))$ for all $n \in \IZ$.

proof:
Every kernel (and hence every equalizer) satisfies this property by the construction of kernels. Conversely, suppose that $f : (V,F) \to (W,G)$ is a filtered linear map satisfying this condition. Then $f$ induces an isomorphism between $(V,F)$ and $(U,G)$, where $U \coloneqq \im(f) \subseteq W$ is equipped with the induced filtration $G^n(U) \coloneqq U \cap G^n(W)$. Endow $W/U$ with the induced filtration $G^n(W/U) \coloneqq \pi_*(G^n(W))$, where $\pi : W \to W/U$ is the quotient map. Then $\pi : (W,G) \to (W/U,G)$ is a filtered linear map, and by the general construction of kernels, its kernel is the vector space $U$ equipped with the induced filtration. Hence, $f : (V,F) \to (W,G)$ is a kernel of $\pi : (W,G) \to (W/U,G)$.


category_id: FiltVect
type: regular epimorphisms
description:
A filtered linear map $f : (V,F) \to (W,G)$ is a regular epimorphism if and only if $f : V \to W$ is surjective and $G^n(W) = f_*(F^n(V))$ for all $n \in \IZ$.

proof:
Every cokernel (and hence every coequalizer) satisfies this property by the construction of cokernels. Conversely, suppose that $f : (V,F) \to (W,G)$ is a filtered linear map satisfying this condition. Let $U \subseteq V$ be the kernel of the underlying linear map $f : V \to W$, equipped with the induced filtration $F^n(U) \coloneqq U \cap F^n(V)$. The inclusion $(U,F) \to (V,F)$ is a filtered linear map. By the general construction of cokernels, its cokernel is $(V/U,F)$, where $F^n(V/U) \coloneqq \pi_*(F^n(V))$ and $\pi : V \to V/U$ is the quotient map. It remains to observe that the induced isomorphism of vector spaces $h : V/U \to W$, characterized by $h \circ \pi = f$, is in fact an isomorphism of filtered vector spaces. Indeed, $$h_*(F^n(V/U)) = h_*(\pi_*(F^n(V))) = f_*(F^n(V)) = G^n(W).$$


category_id: FinAb
type: monomorphisms
description: injective homomorphisms
proof:
Let $f : A \to B$ be a monomorphism of finite abelian groups. Let $a \in A$ be in the kernel of $a$, say of order $n$. Then we may view $a$ as a morphism $a : \IZ/n \to A$ with $f \circ a = 0$, and $\IZ/n$ is finite. Hence, $a = 0$.


category_id: FinGrp
type: monomorphisms
description: injective homomorphisms
proof:
Let $f : A \to B$ be a monomorphism of finite groups. Let $a \in A$ be in the kernel of $a$, say of order $n$. Then we may view $a$ as a morphism $a : C_n \to A$ with $f \circ a = 1$ (the trivial homomorphism), and $C_n$ is finite. Hence, $a = 1$.


category_id: FinGrp
type: epimorphisms
description: surjective homomorphisms
proof:
For the non-trivial direction, if $f : G \to H$ is an epimorphism, we may factor it as $G \to f(G) \to H$, and $f(G) \to H$ is still an epimorphism, but also an inclusion and hence a monomorphism. Since we already know that the category is mono-regular, $f(G) \to H$ must be an isomorphism.


category_id: FinOrd
type: epimorphisms
description: surjective order-preserving maps
proof:
The proof is similar to the one for <a href="/category/Set">$\Set$</a>: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphisms $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^*(A) = f^*(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^*(A) \setminus f^*(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.


category_id: FinVect_c
type: monomorphisms
description: injective linear maps
proof:
For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms.


category_id: FinVect_c
type: epimorphisms
description: surjective linear maps
proof:
For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.


category_id: Fld
type: regular monomorphisms
proof: See <a href="https://math.stackexchange.com/questions/5129895" target="_blank">MSE/5129895</a>.
description:
A Galois extension is a regular monomorphism iff it is procyclic, and the general case can be reduced to this situation; see the reference for details.


category_id: FreeAb
type: monomorphisms
description: injective homomorphisms
proof:
Let $f : A \to B$ be a monomorphism of free abelian groups. Let $a \in A$ be in the kernel of $a$. Then we may view $a$ as a morphism $a : \IZ \to A$ with $f \circ a = 0$, and $\IZ$ is free. Hence, $a = 0$.


category_id: FreeAb
type: epimorphisms
description:
homomorphisms $f : A \to B$ with the property that $f(A)$ is not contained in a proper direct summand of $B$.

proof:
Let $f : A \to B$ be a morphism of free abelian groups such that $f(A)$ is not contained in a proper direct summand of $B$. Then $f$ is an epimorphism: If $t : B \to C$ is a morphism with $t \circ f = 0$, we want to show $t = 0$. Since the image of $t$ is free abelian (as a subgroup of $B$), we may assume that $t$ is surjective. Since $C$ is free, $t$ splits, so its kernel $K$ is a direct summand of $B$ (Splitting Lemma). It contains $f(A)$ because of $t \circ f = 0$. By assumption, $K = B$, so that $t = 0$. Conversely, assume that $f : A \to B$ is an epimorphism, and that $f(A)$ is contained in a direct summand $K$ of $B$. Let $L$ be a complement of $B$ (which is free abelian) and let $p : B \to L$ be the projection. Then $t \circ f = 0$, so $t = 0$. But then $L = 0$, which means $K = B$.


category_id: Grp
type: epimorphisms
description: surjective homomorphisms
proof:
For the non-trivial direction, if $f : G \to H$ is an epimorphism, we may factor it as $G \to f(G) \to H$, and $f(G) \to H$ is still an epimorphism, but also an inclusion and hence a monomorphism. Since we already know that the category is balanced, $f(G) \to H$ must be an isomorphism.


category_id: Grp_c
type: monomorphisms
description: injective homomorphisms
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the countable group $\IZ$), hence preserves monomorphisms.


category_id: Haus
type: epimorphisms
description: continuous maps with dense image
proof:
It is clear that continuous maps with dense image are epimorphism, but the other direction is non-trivial. See <a href="https://math.stackexchange.com/questions/214045" target="_blank">MSE/214045</a> for a proof.


category_id: Haus
type: regular monomorphisms
description: embeddings with closed image
proof:
The explicit construction of equalizers shows that they are embeddings, and they have a closed image because of the well-known lemma that for a Hausdorff space the diagonal $X \to X \times X$ has closed image. For the other non-trivial direction, see <a href="https://math.stackexchange.com/questions/214045/" target="_blank">MSE/214045</a>.


category_id: Haus
type: regular epimorphisms
description: surjective quotient maps
proof:
The coequalizer of two continuous maps $f,g : X \rightrightarrows Y$ of Hausdorff spaces is given by $Y \to Q \to Q_H$, where $Y \to Q$ is their coequalizer in $\Top$ and $Q \to Q_H$ is the Hausdorff reflection of $Q$. By the construction of coequalizers in <a href="/category/Top">$\Top$</a>, the map $Y \to Q$ is a surjective quotient map. Moreover, the construction of the Hausdorff reflection (see <a href="https://ncatlab.org/nlab/show/Hausdorff+space#HausdorffReflectionViaHomsIntoAllHausdorffSpaces" target="_blank">nLab</a>) shows that $Q \to Q_H$ is also a surjective quotient map. Hence, $Y \to Q_H$ is a surjective quotient map as well. Conversely, if $p : X \to Y$ is a surjective quotient map between Hausdorff spaces, we know from the classification in $\Top$ that $p$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$ in $\Top$. Since $X \times_Y X$ is Hausdorff, the same universal property remains valid in $\Haus$.


category_id: J2
type: epimorphisms
description: surjective morphisms
proof:
For the non-trivial direction: The category is epi-regular (since it is an elementary topos), and every regular epimorphism is surjective (this holds in any algebraic category).


category_id: LRS_R
type: isomorphisms
proof: This is easy.
description:
A morphism $(f,f^\sharp) : (X, \O_X) \to (Y,\O_Y)$ is an isomorphism iff $f : X \to Y$ is a homeomorphism and $f^\sharp : \O_Y \to f_* \O_X$ is an isomorphism of sheaves.


category_id: LRS_R
type: epimorphisms
description:
A morphism $(f,f^\sharp) : (X, \O_X) \to (Y,\O_Y)$ is an epimorphism iff $f : X \to Y$ is surjective and $f^\sharp : \O_Y \to f_* \O_X$ is a monomorphism sheaves.

proof:
It is obvious that morphisms with this property are epimorphisms. For the opposite, assume that $(f,f^\sharp) : (X, \O_X) \to (Y,\O_Y)$ is an epimorphism. Then the codiagonal $$(Y,\O_Y) \sqcup_{(X,\O_X)} (Y,\O_Y) \to (Y,\O_Y)$$ is an isomorphism. By construction of the pushout, the underlying space of the pushout is $Y \sqcup_X Y$. Hence, $f$ is an epimorphism in $\Top$, i.e. it is surjective. For open subsets $V \subseteq Y$ the preimage in the pushout is $V \sqcup_{f^{-1}(V)} V$, and its ring of sections is the pullback $\O_Y(V) \times_{\O_X(f^{-1}(V))} \O_Y(V)$. Since the diagonal $$\O_Y(V) \to \O_Y(V) \times_{\O_X(f^{-1}(V))} \O_Y(V)$$ is an isomorphism, the map $f^\sharp(V) : \O_Y(V) \to \O_X(f^{-1}(V))$ is a monomorphism. Hence, $f^\sharp$ is a monomorphism of sheaves.


category_id: M-Set
type: epimorphisms
description: surjective $M$-maps
proof:
This holds in every functor category $[\C,\Set]$, here applied to the case that $\C$ has just one object.


category_id: Man
type: epimorphisms
description: smooth maps with dense image
proof:
Let $f : X \to Y$ be a smooth map which is not dense. Choose some non-empty open subset $U \subseteq Y$ that is disjoint from $f(X)$. Take any $p \in U$. There is a smooth <i>bump function</i> $g : Y \to \IR$ with $g(p) = 1$ and $\supp(g) \subseteq U$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25). Hence, $g \neq 0$ and $g \circ f = 0 = 0 \circ f$. Thus, $f$ is not an epimorphism.


category_id: Meas
type: regular monomorphisms
description: embeddings
proof:
(This is the same proof as for <a href="/category/Top">$\Top$</a>.) Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the trivial $\sigma$-algebra.


category_id: Meas
type: regular epimorphisms
description:
A measurable map $f : X \to Y$ is a regular epimorphism iff $f$ is surjective and $f$ is a quotient map, meaning that a subset of $Y$ is measurable when its $f$-preimage is measurable.

proof:
The proof works the same as for $\Top$ (and can in fact be generalized to topological functors). Regular epimorphisms are surjective quotient maps by the explicit construction of coequalizers. Conversely, if $q : X \to Y$ is a surjective quotient map, then one checks that $q$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$: This is true for the underlying sets, and measurability of the induced morphism follows since $q$ is a quotient map.


category_id: Met_c
type: regular monomorphisms
description: embeddings of closed subspaces
proof:
A reference is Example 7.58 (3) in <a href="https://ncatlab.org/nlab/show/Abstract+and+Concrete+Categories" target="_blank">Joy of Cats</a>, but a proof is missing there.


category_id: Mon
type: epimorphisms
description:
A monoid map $f : T \to S$ is an epimorphism iff $S$ equals the <i>dominion</i> of $U \coloneqq f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.

proof:
This is <a href="https://en.wikipedia.org/wiki/Isbell's_zigzag_theorem" target="_blank">Isbell's zigzag Theorem</a>, see references there.


category_id: Mono
type: isomorphisms
proof: This is easy.
description:
morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a bijection between $X$ and $Y$, and $f(X') = Y'$


category_id: Mono
type: monomorphisms
description: morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$
proof:
For the non-trivial direction, use the fact that the functor taking an object $(X, X')$ to $X$ and a morphism $f : (X, X') \to (Y, Y')$ to the function $f : X \to Y$ is representable by $(1, 0)$.


category_id: Mono
type: epimorphisms
description: morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$
proof:
For the non-trivial direction, use the fact that the forgetful functor $\Mono \to \Set$, $(X, X') \mapsto X$, has a right adjoint given by $X \mapsto (X, X)$. Therefore, the forgetful functor preserves epimorphisms; so if $f : (X, X') \to (Y, Y')$ is an epimorphism in $\Mono$, then $f : X \to Y$ is an epimorphism in <a href="/category/Set">$\Set$</a> and therefore surjective.


category_id: Mono
type: regular monomorphisms
description:
morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$, and $f^{-1}(Y') = X'$ (in particular, if $f : X \to Y$ is an inclusion map, then this is equivalent to $X' = X \cap Y'$)

proof:
To show any regular monomorphism satisfies this condition, suppose we have a parallel pair $g, h : (Y, Y') \rightrightarrows (Z, Z')$. To form the equalizer in $\Mono$, first we form the equalizer $f : X \hookrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of limits in the proof of completeness above, the equalizer in $\Mono$ is $(X, f^{-1}(Y'))$. Thus, we see that $f^{-1}(Y') = X'$.
For the other direction, suppose we are given a morphism $f : (X, X') \to (Y, Y')$ satisfying this condition. We can then construct an equalizer diagram $$\begin{CD} (X, X') @> f >> (Y, Y') @> \chi_{f(X)} > \top_Y > (\{ \top, \bot \}, \{ \top, \bot \}). \end{CD}$$ Here $\chi_{f(X)} : Y \to \{ \top, \bot \}$ is the characteristic function of the subset $f(X) \subseteq Y$, and $\top_Y$ is the constant function on $Y$ with value $\top$.


category_id: Mono
type: regular epimorphisms
description:
morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$, and $f(X') = Y'$

proof:
To show any regular epimorphism satisfies this condition, suppose we have a parallel pair $g, h : (Z, Z') \rightrightarrows (X, X')$. To form the coequalizer in $\Mono$, first we form the coequalizer $f : X \twoheadrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of colimits in the proof of cocompleteness above, the coequalizer in $\Mono$ is $(Y, f(X'))$. Thus, we see that $f(X') = Y'$.
To show any morphism $f : (X, X') \to (Y, Y')$ satisfying this condition is a regular epimorphism, note that the kernel pair of $f$ can be computed component-wise. Therefore, in general the coequalizer of the kernel pair of $f$ is $(f(X), f(X'))$; and with the given assumptions on $f$, this is isomorphic to $(Y, Y')$.


category_id: PMet
type: epimorphisms
description: surjective non-expansive maps
proof:
Let $f : X \to Y$ be a non-expansive map that is not surjective. Choose $y_0 \in Y \setminus f(X)$. We extend the pseudo-metric from $Y$ to $Z \coloneqq Y \sqcup \{y'_0\}$ via $d(y,y'_0) \coloneqq d(y,y_0)$, i.e., we make $y_0,y'_0$ indistinguishable. Let $g : Y \to Z$ be the inclusion and $h : Y \to Z$ be the map that composes $g$ with the swap between $y_0$ and $y'_0$. Both are isometric and satisfy $g \circ f = h \circ f$. Therefore, $f$ is not an epimorphism.


category_id: PMet
type: regular epimorphisms
description:
surjective non-expansive maps $f : X \to Y$ with the property that for all $x,x' \in X$, $d(p(x),p(x'))$ is the infimum of the sums $\sum_{i=0}^{n-1} d(y_i,x_{i+1})$, where $x=x_0$, $x_i \sim y_i$ for $0 \leq i \leq n$, and $y_n = x'$.

proof:
This follows from the construction of the quotient pseudo-metric on $X/{\sim}$ in <a href="https://mathoverflow.net/questions/123739" target="_blank">MO/123739</a>.


category_id: Pos
type: epimorphisms
description: surjective order-preserving functions
proof:
Clearly, surjective maps are epimorphisms. Conversely, assume that $f : P \to Q$ is an order-preserving map which is not surjective. Choose $q \in Q \setminus f(P)$. The order-preserving maps $Q \to \{0 < 1\}$ correspond to the upper sets in $Q$, and composing them with $f$ corresponds to taking their $f$-preimages. Consider the two upper sets $Q_{> q}$ and $Q_{\geq q}$. Their $f$-preimages are the same since $q \notin f(P)$. Therefore, $f$ is not an epimorphism.


category_id: Pos
type: regular monomorphisms
description: embeddings
proof:
Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C \coloneqq Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p'$ in $C$ iff $p \leq p'$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a partial order, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.


category_id: Prost
type: epimorphisms
description: surjective order-preserving functions
proof:
Clearly, surjective maps are epimorphisms. The converse follows since, as mentioned, the forgetful functor $\Prost \to \Set$ has a right adjoint hence preserves epimorphisms.


category_id: Prost
type: regular monomorphisms
description: embeddings
proof:
Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C \coloneqq Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p'$ in $C$ iff $p \leq p'$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a preorder, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.


category_id: R-Mod
type: epimorphisms
description: surjective $R$-linear maps
proof:
The forgetful functor to abelian groups is faithful and preserves colimits, hence reflects and preserves epimorphisms. Alternatively, use the same proof as for abelian groups.


category_id: Rel
type: isomorphisms
description: bijective functions
proof:
For the non-trivial direction, assume that $R : A \to B$ is a relation which has an inverse relation $S : B \to A$. For every $a \in A$ we have $(a,a) \in \id_A = S \circ R$, so there is some $b \in B$ with $(a,b) \in R$ (and $(b,a) \in S$). This shows that $R$ is left-total, and for right-total the argument is similar. By symmetry, this also holds for $S$. To show that $R$ is a function, assume $(a,b_1), (a,b_2) \in R$. Choose some $b_3 \in B$ with $(b_3,a) \in S$. It follows $(b_3,b_1) \in S \circ R = \id_A$, so $b_3 = b_1$. Similarly, $(b_3,b_2) \in S \circ R = \id_A$, so $b_3 = b_2$. This shows that $R$ is a function, i.e. left-unique. That $R$ is injective, i.e. right-unique, follows by symmetry. Finally, $R$ is surjective since it is right-total.


category_id: Rel
type: monomorphisms
proof: See <a href="https://math.stackexchange.com/questions/350716/" target="_blank">MSE/350716</a>.
description:
A relation $R : A \to B$ is a monomorphism iff the map $R_* : P(A) \to P(B)$ defined by $T \mapsto \{b \in B : \exists \, a \in T: (a,b) \in R \}$ is injective.


category_id: Rel
type: epimorphisms
proof: See <a href="https://math.stackexchange.com/questions/350716/" target="_blank">MSE/350716</a>.
description:
A relation $R : A \to B$ is an epimorphism iff the map $R^* : P(B) \to P(A)$ defined by $S \mapsto \{a \in A : \exists \, b \in S: (a,b) \in R \}$ is injective.


category_id: Sch_R
type: isomorphisms
proof: This is easy.
description:
pairs $(f,f^{\sharp})$ consisting of a homeomorphism $f$ and an isomorphism of sheaves $f^{\sharp}$ of $R$-algebras


category_id: SemiGrp
type: epimorphisms
description:
A semigroup homomorphism $f : T \to S$ is an epimorphism iff $S$ equals the <i>dominion</i> of $U \coloneqq f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.

proof:
This is <a href="https://en.wikipedia.org/wiki/Isbell's_zigzag_theorem" target="_blank">Isbell's zigzag Theorem</a>, see references there.


category_id: Set
type: monomorphisms
description: injective maps
proof:
For the non-trivial direction, if $f : X \to Y$ is a monomorphism of sets and $a,b \in X$ satisfy $f(a) = f(b)$, then $f \circ a = f \circ b$ when we regard $a,b$ as morphisms $a,b : 1 \to X$. Hence, $a = b$. More generally, if $\C$ is a category that admits a faithful and representable functor $U : \C \to \Set$, then the monomorphisms in $\C$ are precisely the morphisms whose $U$-image is injective.


category_id: Set
type: epimorphisms
description: surjective maps
proof:
For the non-trivial direction, if $f : X \to Y$ is an epimorphism of sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.


category_id: Set_arrow
type: monomorphisms
description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective
proof:
For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$.


category_id: Set_arrow
type: epimorphisms
description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective
proof:
For the non-trivial direction, use the fact that the category is epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise.


category_id: Set_c
type: epimorphisms
description: surjective maps
proof:
For the non-trivial direction, if $f : X \to Y$ is an epimorphism of countable sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.


category_id: Set_f
type: monomorphisms
description: injective maps
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the singleton), hence preserves monomorphisms.


category_id: Set_f
type: epimorphisms
description: surjective maps with finite fibers
proof:
For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.


category_id: Set_*
type: epimorphisms
description: surjective pointed maps
proof:
If $f : X \to Y$ is an epimorphism of pointed sets, then the inclusion $i : f(X) \hookrightarrow Y$ is an epimorphism as well. But it is also a split monomorphism (we may map everything in $Y \setminus f(X)$ to the base point of $f(X)$, and do not touch the rest), hence an isomorphism.


category_id: Setne
type: epimorphisms
description: surjective maps
proof:
For the non-trivial direction, let $f : X \to Y$ be an epimorphism of non-empty sets. Then the inclusion $f(X) \hookrightarrow Y$ is an epimorphism as well, but also a split monomorphism (we can just map everything in $Y \setminus f(X)$ to a fixed element of $f(X)$). As such, it must be an isomorphism.


category_id: Sh(X)
type: monomorphisms
description: morphisms of sheaves that are injective on every open subset
proof:
For the non-trivial direction, assume that $f : F \to G$ is a monomorphism of sheaves on $X$. Then the diagonal $F \to F \times_G F$ is an isomorphism. Since pullbacks of sheaves are constructed section-wise, it follows that the diagonal $F(U) \to F(U) \times_{G(U)} F(U)$ is an isomorphism for every open set $U \subseteq X$. But this means that $f(U) : F(U) \to G(U)$ is injective.


category_id: Sh(X)
type: epimorphisms
description:
morphisms of sheaves $f : F \to G$ that are "locally surjective": for every local section $g \in G(U)$ there is an open covering $U = \bigcup_{i \in I} U_i$ such that each $g|_{U_i} \in G(U_i)$ is contained in the image of $f(U_i) : F(U_i) \to G(U_i)$.

proof:
The one direction is easy. For the other one, assume that $f : F \to G$ is an epimorphism of sheaves. For every $x \in X$ the map on stalks $f_x : F_x \to G_x$ is an epimorphism because the stalk functor $\Sh(X) \to \Set$ admits a right adjoint: take skyscraper sheaves. For $x \in U$ then $g_x \in G_x$ has a preimage in $F_x$, say represented by some $f \in F(V_x)$ for some $x \in V_x \subseteq U$. By construction of the stalk $G_x$, there is some $x \in U_x \subseteq V_x$ with $f(U_x)(f|_{U_x}) = g|_{U_x}$. Hence, the sets $(U_x)$ provide the open covering.


category_id: Sh(X,Ab)
type: monomorphisms
description: morphisms of abelian sheaves that are injective on every open subset
proof:
For the non-trivial direction, assume that $f : F \to G$ is a monomorphism of abelian sheaves on $X$. Then the diagonal $F \to F \times_G F$ is an isomorphism. Since pullbacks of abelian sheaves are constructed section-wise, it follows that the diagonal $F(U) \to F(U) \times_{G(U)} F(U)$ is an isomorphism for every open set $U \subseteq X$. But this means that $f(U) : F(U) \to G(U)$ is injective.


category_id: Sh(X,Ab)
type: epimorphisms
description:
morphisms of abelian sheaves $f : F \to G$ that are "locally surjective": for every local section $g \in G(U)$ there is an open covering $U = \bigcup_{i \in I} U_i$ such that each $g|_{U_i} \in G(U_i)$ is contained in the image of $f(U_i) : F(U_i) \to G(U_i)$.

proof:
The one direction is easy. For the other one, assume that $f : F \to G$ is an epimorphism of abelian sheaves. For every $x \in X$ the homomorphism on stalks $f_x : F_x \to G_x$ is an epimorphism because the stalk functor  $\Sh(X,\Ab) \to \Ab$ admits a right adjoint: take skyscraper sheaves. For $x \in U$ then $g_x \in G_x$ has a preimage in $F_x$, say represented by some $f \in F(V_x)$ for some $x \in V_x \subseteq U$. By construction of the stalk $G_x$, there is some $x \in U_x \subseteq V_x$ with $f(U_x)(f|_{U_x}) = g|_{U_x}$. Hence, the sets $(U_x)$ provide the open covering.


category_id: Sp
type: monomorphisms
description: pointwise injective natural transformations
proof:
If $a : F \to G$ is a monomorphism of species, then the diagonal morphism $F \to F \times_G F$ is an isomorphism, so that for every $x$ the diagonal morphism $F(x) \to F(x) \times_{G(x)} F(x)$ is an isomorphism, i.e., $a(x) : F(x) \to G(x)$ is a monomorphism. This argument works for every functor category where the target has fiber products.


category_id: Top
type: epimorphisms
description: surjective continuous maps
proof:
The proof works exactly as for the category of sets, where we endow $2$ with the indiscrete topology.


category_id: Top
type: regular monomorphisms
description: embeddings
proof:
Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \to \{0,1\}$, where $\{0,1\}$ carries the indiscrete topology.


category_id: Top
type: regular epimorphisms
description: surjective quotient maps
proof:
Regular epimorphisms are surjective quotient maps by the explicit construction of coequalizers. Conversely, if $q : X \to Y$ is a surjective quotient map, then one checks that $q$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$: This is true for the underlying sets, and continuity of the induced morphism follows since $q$ is a quotient map.


category_id: Top_*
type: monomorphisms
description: injective pointed continuous maps
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the discrete two-point space), hence preserves monomorphisms.


category_id: Top_*
type: epimorphisms
description: surjective pointed continuous maps
proof:
For the non-trivial direction: The forgetful functor $\Top_* \to \Top$ preserves pushouts and hence also epimorphisms, and we already know the epimorphisms in $\Top$.


category_id: Top_*
type: regular monomorphisms
description: embeddings
proof:
Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \to \{0,1\}$, where $\{0,1\}$ carries the indiscrete topology and $1$ is the base point.


category_id: Top_*
type: regular epimorphisms
description: surjective pointed quotient maps
proof:
Regular epimorphisms are surjective pointed quotient maps by the explicit construction of coequalizers. Conversely, if $q : X \to Y$ is a surjective pointed quotient map, then one checks that $q$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$: This is true for the underlying pointed sets, and continuity of the induced morphism follows since $q$ is a quotient map.


category_id: TorsAb
type: monomorphisms
description: injective group homomorphisms
proof:
For the non-trivial direction, assume $f : A \to B$ is a monomorphism and $a \in A$ satisfies $f(a)=0$. Choose $n \geq 1$ with $n a = 0$. Then $a$ corresponds to a homomorphism of torsion abelian groups $\tilde{a} : \IZ/n \to A$ satisfying $f \circ \tilde{a} = 0$. Hence, $\tilde{a} = 0$, which means $a = 0$.


category_id: TorsAb
type: epimorphisms
description: surjective homomorphisms
proof:
Clearly, surjective homomorphisms are epimorphisms. The converse follows since the forgetful functor $\TorsAb \to \Ab$ has a right adjoint, hence preserves epimorphisms.


category_id: TorsFreeAb
type: monomorphisms
description: injective group homomorphisms
proof:
For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the group $\IZ$), hence preserves monomorphisms.


category_id: TorsFreeAb
type: epimorphisms
description: homomorphisms $f : A \to B$ such that $B/f(A)$ is a torsion group
proof:
The homomorphism $f$ is an epimorphism iff its cokernel in $\TorsFreeAb$ is trivial. As with all types of colimits, the cokernel is the torsion-free reflection of the cokernel in $\Ab$, which is $B/f(A)$. This is trivial iff $B/f(A)$ is torsion.


category_id: TorsFreeAb
type: regular monomorphisms
description:
injective group homomorphisms $i : A \to B$ such that $B/i(A)$ is torsion-free, i.e., $i$ is the inclusion of a <i>saturated subgroup</i>

proof:
If $i : A \to B$ is the kernel of $f : B \to C$ in $\TorsFreeAb$, it is also the kernel of $f$ in $\Ab$, so we know that $i$ is injective with $i(A) = \{b \in B : f(b) = 0\}$. If $n \in \IZ \setminus \{0\}$ and $b \in B$ satisfy $f(n b) = 0$, then also $f(b)=0$ since $C$ is torsion-free. This shows that $B/i(A)$ is torsion-free. Conversely, if $i$ is injective and $B/i(A)$ is torsion-free, then $i$ is the kernel of the natural homomorphism $B \to B/i(A)$.


category_id: TorsFreeAb
type: regular epimorphisms
description: surjective group homomorphisms
proof:
By the construction of the coequalizer in $\TorsFreeAb$ as the torsion-free reflection of the coequalizer in $\Ab$, every regular epimorphism is surjective. Conversely, if $f : A \to B$ is a surjective homomorphism of torsion-free abelian groups, in $\Ab$ it is the coequalizer of the two projections $A \times_B A \rightrightarrows A$, and $A \times_B A$ is also torsion-free. Hence, it is also the coequalizer of these projections in $\TorsFreeAb$.


category_id: Vect
type: epimorphisms
description: surjective linear maps
proof:
The forgetful functor to abelian groups is faithful and preserves colimits, hence reflects and preserves epimorphisms. Alternatively, just use the same proof as for abelian groups.


category_id: Z
type: monomorphisms
description: pointwise injective natural transformations
proof:
If $a : F \to G$ is a monomorphism of Z-functors, then the diagonal morphism $F \to F \times_G F$ is an isomorphism, so that for every $R$ the diagonal morphism $F(R) \to F(R) \times_{G(R)} F(R)$ is an isomorphism, i.e., $a(R) : F(R) \to G(R)$ is a monomorphism. This argument works for every functor category where the target has fiber products.


category_id: sSet
type: monomorphisms
description: pointwise injective transformations
proof:
If $a : F \to G$ is a monomorphism of simplicial sets, then the diagonal morphism $F \to F \times_G F$ is an isomorphism, so that for every $n$ the diagonal morphism $F(n) \to F(n) \times_{G(n)} F(n)$ is an isomorphism, i.e., $a(n) : F(n) \to G(n)$ is a monomorphism. This argument works for every functor category where the target has fiber products.


category_id: walking_coreflexive_pair
type: monomorphisms
description: the identities and $i$, $j$
proof:
Since $pi = \id$, but $ip \neq \id$, we conclude that $i$ is a monomorphism, but $p$ is not. Likewise, $j$ is a monomorphism. Since $p$ is not a monomorphism, $ip$ and $jp$ are also no monomorphisms.


category_id: walking_coreflexive_pair
type: epimorphisms
description: the identities and $p$
proof:
Since $pi = \id$, but $ip \neq \id$, we conclude that $p$ is an epimorphism, but $i$ is not. Hence, also $ip$ is not an epimorphism. Likewise, $j$ and $jp$ are no epimorphisms.


category_id: walking_fork
type: regular monomorphisms
description: the identities and $i$
proof:
First, $i$ is the equalizer of $f,g$. The morphism $f$ is an epimorphism (and a monomorphism), but no isomorphism, hence cannot be a regular monomorphism. The same holds for $g$.


category_id: walking_splitting
type: monomorphisms
description: the identities and $i$
proof:
The morphism $i$ is even a split monomorphism. The morphism $p$ is not a monomorphism since $p \circ \id_1 = p \circ ip$. The morphism $ip$ is not a monomorphism since it would imply that $p$ is a monomorphism.


category_id: walking_splitting
type: epimorphisms
description: the identities and $p$
proof:
The morphism $p$ is even a split monomorphism. The morphism $i$ is not an epimorphism since $\id_1 \circ i = ip \circ i$. The morphism $ip$ is not a epimorphism since it would imply that $i$ is an epimorphism.


