Add various categories with subobject classifiers

content/inclusion-functors.md

@@ -6,13 +6,13 @@ description: We gather results about inclusion functors
 # Inclusion functors
 
 ::: Lemma 1
-Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous.
+Let $\D$ be category that has an extremal cogenerating collection $S$. Let $\C \subseteq \D$ be a full subcategory that contains every object of $S$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous.
 :::
 
 ::: Proof
 Let $D : \I \to \C$ be a diagram such that $D$ has a colimit $(u_i : D(i) \to X)$ in $\C$ and $U \circ D$ has a colimit $(v_i : D(i) \to Y)$ in $\D$. There is a unique morphism $f : Y \to X$ such that $f \circ v_i = u_i$ for every $i \in \I$. Moreover, for every object $T \in \C$ the map of sets
 
 $$f^* : \Hom(X,T) \to \Hom(Y,T)$$
 
-is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \coloneqq Q$ to conclude that $f$ is an isomorphism.
+is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \in S$ to conclude that $f$ is an isomorphism.
 :::

content/natural_numbers_objects.md

@@ -109,3 +109,35 @@ This finishes the proof.
 _Remark._ Actually, the mentioned [result](/category-implication/parametrized_nno_criterion) and Lemma 4 can be combined into an equivalent characterization as follows: In a category with finite products and countable copowers, the NNO (which exists, see [here](/category-implication/nno_criterion)) is a parametrized NNO if and only if for all objects $A$ the canonical morphism
 $$\textstyle \coprod_{n \in \IN} A = \coprod_{n \in \IN} (A \times 1) \to A \times \coprod_{n \in \IN} 1$$
 is an isomorphism. This is the precise connection to countable distributivity.
+
+::: Lemma 5
+Let $F : \C \to \D$ be left adjoint to $G : \D \to \C$. Assume that $1_{\C}$ is a terminal object of $\C$ such that $1_{\D} \coloneqq F(1_{\C})$ is a terminal object of $\D$. Then $F$ preserves natural numbers objects. That is, if $(N,z,s)$ is a natural numbers object in $\C$, then its image $(F(N),F(z),F(s))$ is a natural numbers object in $\D$.
+:::
+
+::: Proof
+For a category $\C$ with a terminal object $1_{\C}$, let $R(\C)$ denote the category of diagrams
+$$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$
+in $\C$. A natural numbers object in $\C$ is precisely an initial object of $R(\C)$. Suppose that $H : \C \to \D$ is a functor between categories with terminal objects that preserves terminal objects. Then $H$ induces a functor $R(H) : R(\C) \to R(\D)$ that maps
+$$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$
+to its image
+$$1_{\D} \cong H(1_{\C}) \xrightarrow{H(x_0)} H(X) \xrightarrow{H(r)} H(X).$$
+
+In the situation of the lemma, we therefore have two functors
+
+$$
+\begin{align*}
+R(F) & : R(\C) \to R(\D),\\
+R(G) & : R(\D) \to R(\C).
+\end{align*}
+$$
+
+Notice that $G$ preserves terminal objects since it is a right adjoint.
+
+We claim that $R(F)$ is left adjoint to $R(G)$. Indeed, for objects $(X,x_0,r) \in R(\C)$ and $(Y,y_0,s) \in R(\D)$, a morphism $R(F)(X,x_0,r) \to (Y,y_0,s)$ is the same as a morphism $f : F(X) \to Y$ such that
+$$f \circ F(x_0) = y_0, \quad s \circ f = f \circ F(r).$$
+Under the adjunction $F \dashv G$, it corresponds to a morphism $\widetilde{f} : X \to G(Y)$ such that
+$$\widetilde{f} \circ x_0 = G(y_0), \quad G(s) \circ \widetilde{f} = \widetilde{f} \circ r.$$
+This is precisely a morphism $(X,x_0,r) \to R(G)(Y,y_0,s)$.
+
+Since $R(F)$ is a left adjoint, it preserves initial objects. This is precisely the statement that $F$ preserves natural numbers objects.
+:::

content/subcategories.md

@@ -100,15 +100,19 @@ where $U(X) \times_{U(Y)} U(X)$ is the kernel pair of $U(f)$, and $U(\im(f))$ is
 :::
 
 ::: Lemma 8
-Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves inhabited finite limits and coequalizers. If $\D$ has effective congruences, then so does $\C$.
+Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has pullbacks and coequalizers, that $U$ preserves pullbacks and coequalizers, and that $U$ preserves jointly monomorphic parallel pairs (which holds, for example, if $\C$ has binary products and $U$ preserves them). If $\D$ has effective congruences, then so does $\C$.
 :::
 
 ::: Proof
-Suppose we have a congruence $E \hookrightarrow X\times X$ in $\C$. We can then form the quotient $X \to X/E$ as a coequalizer, along with the kernel pair $X \times_{X/E} X$ and the comparison map $i$ in the diagram below:
-$$E \xrightarrow{i} X \times_{X/E} X \rightrightarrows X \to X/E.$$
-By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
-$$UE \xrightarrow{Ui} UX \times_{U(X/E)} UX \rightrightarrows UX \to U(X/E).$$
-Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ is a monomorphism since $U$ preserves pullbacks and therefore preserves monomorphisms; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ to reflexivity and symmetry morphisms for $UE$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ to a transitivity morphism for $UE$. This congruence $UE$ of $\D$ is effective, so we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $E$ is effective.
+Suppose we have a congruence $E \rightrightarrows X$ in $\C$. We first observe that its image $U(E) \rightrightarrows U(X)$ is a congruence in $\D$, and therefore effective. It is jointly monomorphic by assumption on $U$; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ into reflexivity and symmetry morphisms for $U(E)$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ into a transitivity morphism for $U(E)$.
+
+Now let $X/E$ be the quotient of $E \rightrightarrows X$, i.e. its coequalizer. We will show that the canonical morphism
+$$E \to X \times_{X/E} X$$
+is an isomorphism. Since $U$ is fully faithful and preserves pullbacks, it suffices to prove that the canonical morphism
+$$U(E) \to U(X) \times_{U(X/E)} U(X)$$
+is an isomorphism, where $U(X/E)$ is the coequalizer of $U(E) \rightrightarrows U(X)$ since $U$ preserves coequalizers. Since the congruence $U(E) \rightrightarrows U(X)$ is effective by the first part of the proof, this follows from [this lemma](/content/effective-congruence-quotients).
+
+Finally, to prove the parenthetical remark, assume that $\C$ has binary products and that $U$ preserves them. Then $U$ preserves jointly monomorphic parallel pairs, because it preserves monomorphisms (as it preserves pullbacks), and a pair $A \rightrightarrows B$ is jointly monomorphic if and only if the induced morphism $A \to B \times B$ is a monomorphism.
 :::
 
 ::: Lemma 9

database/data/categories/DiGraph.yaml

@@ -17,6 +17,7 @@ related:
   - walking_pair
   - Cat
   - Bin
+  - DiGraph_fc
 
 satisfied_properties:
   - property: locally small
@@ -36,19 +37,20 @@ unsatisfied_properties:
     proof: >-
       Assume that $G$ is a generator. Consider the edgeless graph $H$ with two vertices. Since it has two distinct endomorphisms $H \rightrightarrows H$, there is a morphism $G \to H$. Since $H$ has no edges, this implies that $G$ has no edges. The directed graph $L$ with a single vertex and two loops has two distinct endomorphisms $L \rightrightarrows L$, but since their maps on vertices agree, every morphism $G \to L$ equalizes them. Thus, $G$ is not a generator.
 
-      Alternatively, the claim follows from <a href="/content/topos-with-generator">this result</a>, since the terminal graph (having one vertex and one loop) has a subgraph (having one vertex and no loops) which is neither initial nor terminal.
+      Alternatively, the claim follows from <a href="/content/topos-with-generator">this result</a>, since the terminal directed graph (having one vertex and one loop) has a subgraph (having one vertex and no loops) which is neither initial nor terminal.
+    label: DiGraph_no_generator
 
   - property: semi-strongly connected
     proof: Let $G$ be the directed cycle $0 \to 1 \to 0$ and $H$ be the directed cycle $0 \to 1 \to 2 \to 0$. There is no morphism of directed graphs $G \to H$ since $H$ does not contain two edges of the form $x \to y \to x$ (a vertex can only reoccur after $3$ steps). There is also no morphism $H \to G$, because this would amount to a sequence of edges $x \to y \to z \to x$ in $G$. Every edge in $G$ alternates between the two vertices, so if, say, $x=0$, then $y=1$, $z=0$, and then $x=1$, contradicting $x=0$. More generally, if $C_n$ is the directed $n$-cycle, a morphism of directed graphs $C_n \to C_m$ exists if and only if $m \mid n$.
     label: DiGraph_not_semi-strongly_connected
 
 special_objects:
   initial object:
-    description: the graph with no vertices and hence no edges
+    description: the directed graph with no vertices and hence no edges
   terminal object:
-    description: the graph with one vertex and one loop
+    description: the directed graph with one vertex and one loop
   coproducts:
-    description: The coproduct of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\coprod_i V_i, \coprod_i E_i, \coprod_i s_i, \coprod_i t_i)$. Intuitively, we take the disjoint union of the vertices, keep the edges in the individual graphs, and do not add any edges between distinct graphs.
+    description: The coproduct of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\coprod_i V_i, \coprod_i E_i, \coprod_i s_i, \coprod_i t_i)$. Intuitively, we take the disjoint union of the vertices, keep the edges in the individual directed graphs, and do not add any edges between distinct directed graphs.
   products:
     description: The product of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\prod_i V_i, \prod_i E_i, \prod_i s_i, \prod_i t_i)$.