Add category Mono of injective set functions and commutative squares

databases/catdat/data/categories/FI.yaml

@@ -14,6 +14,7 @@ related_categories:
   - B
   - FS
   - FinSet
+  - Mono
 
 satisfied_properties:
   - property: locally small

databases/catdat/data/categories/Mono.yaml

@@ -0,0 +1,184 @@
+id: Mono
+name: category of injective set functions and commutative diagrams
+notation: $\Mono$
+objects: >-
+  triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \hookrightarrow Y$ is an injective 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}$$
+description: >-
+  This is the full subcategory of $\Set^{\rightarrow}$ consisting of the injective set functions. It is also equivalent to the category of pairs of a set $X$ and a subset $S \subseteq X$, with morphisms $(X, S) \to (Y, T)$ being the functions $f : X \to Y$ such that $f(S) \subseteq T$.
+nlab_link: https://ncatlab.org/nlab/show/Mono
+
+tags:
+  - set theory
+
+related_categories:
+  - Set_arrow
+  - FI
+
+satisfied_properties:
+  - property: locally small
+    proof: This is easy.
+
+  - property: semi-strongly connected
+    proof: This is immediate from the fact that $\Mono$ is a full subcategory of $\Set^{\rightarrow}$, and the latter is semi-strongly connected.
+
+  - property: generator
+    proof: >-
+      The object $0 \hookrightarrow 1$ is a generator. This is because it represents the codomain functor taking an object $f : X \hookrightarrow Y$ to $Y$, and taking a morphism $(\ell, r)$ to $r$. That functor is faithful because once $r$ is fixed, $\ell$ is uniquely determined since $f'$ is a monomorphism in $\Set$.
+
+  - property: cogenerator
+    proof: >-
+      The object $\{ \top, \bot \} \xhookrightarrow{\id} \{ \top, \bot \}$. To see this, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X, Y, f) \rightrightarrows (X', Y', g)$ such that for every morphism $(\ell', r') : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \})$, $(\ell', r') \circ (\ell_1, r_1) = (\ell', r') \circ (\ell_2, r_2)$. Then morphisms $(X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ are equivalent to functions $Y' \to \{ \top, \bot \}$. Since $\{ \top, \bot \}$ is a cogenerator in $\Set$, this implies $r_1 = r_2$; and since $g$ is a monomorphism in $\Set$, we automatically get $\ell_1 = \ell_2$ as well.
+
+  - property: complete
+    proof: The component-wise limit of injective functions is again an injective function, and it forms the limit in $\Mono$.
+    check_redundancy: false
+
+  - property: cocomplete
+    proof: 'We have that $\Mono$ is a reflective subcategory of $\Set^{\rightarrow}$, with the reflector taking a function $f : X \to Y$ to the inclusion map $\im(f) \hookrightarrow Y$. Therefore, the result follows from the fact that $\Set^{\rightarrow}$ is cocomplete.'
+    check_redundancy: false
+
+  - property: disjoint coproducts
+    proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts.
+
+  - property: locally cartesian closed
+    proof: >-
+      For this construction, we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Now, for any object $(D, D')$ of $\Mono$, the reflector functor $\Set^{\rightarrow} \to \Mono$ induces a reflector functor of slices $\Set^{\rightarrow} / (D' \hookrightarrow D)$ to $\Mono / (D, D')$. We claim that this reflector preserves binary products, i.e. it transforms pullbacks over $D' \hookrightarrow D$ in $\Set^{\rightarrow}$ to pullbacks over $(D, D')$ in $\Mono$. Thus, suppose we have two objects $f, g$ of $\Set^{\rightarrow}$ with degree morphisms to $D' \hookrightarrow D$:
+      $$\begin{CD}
+      X @> \deg_X >> D' @< \deg_Y << Y\\
+      @V f VV @VVV @VV g V\\
+      Z @>> \deg_Z > D @<< \deg_W < W.
+      \end{CD}$$
+      Then the reflector turns $f$ into $(Z, \im(f))$ and $g$ into $(W, \im(g))$. The pullback in $\Mono$ is $(Z \times_D W, \im(f) \times_{D'} \im(g))$. On the other hand, taking the pullback in $\Set^{\rightarrow}$ first, and then applying the reflector, gives $(Z \times_D W, \im(X \times_{D'} Y \to Z \times_D W))$. Thus, we must show $\im(f) \times_{D'} \im(g) = \im(X \times_{D'} Y \to Z \times_D W)$.
+
+      We easily see that $\im(X \times_{D'} Y \to Z \times_D W) \subseteq \im(f) \times_{D'} \im(g)$ (this is the inclusion that we automatically get from the canonical comparison morphism). Conversely, suppose we have $z\in \im(f)$ and $w\in \im(g)$ with the same degree (which must be in $D'$). Then there exist $x\in X$ such that $f(x) = z$ and $y\in Y$ such that $g(y) = w$. Since $\deg_X(x) = \deg_Z(z) = \deg_W(w) = \deg_Y(y) \in D'$, we have $(x, y) \in X \times_{D'} Y$, and the image of $(x, y)$ in $Z \times_D W$ is exactly $(z, w)$, finishing the proof of the claim.
+
+      Therefore, from Lemma 5 <a href="/content/subcategories">here</a>, we conclude that each slice of $\Mono$ is cartesian closed, i.e. that $\Mono$ is locally cartesian closed.
+
+  - property: regular subobject classifier
+    proof: 'The object $\{ \top, \bot \} \xhookrightarrow{\id} $\{ \top, \bot \}$ is a regular subobject classifier, with $\top : (1, 1, \id) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ consisting of the maps with image $\top$. This follows from the description of regular monomorphisms below.'
+
+  - property: locally finitely presentable
+    proof: >-
+      It is equivalent to the category of models of the finite limit sketch with a single limit cone
+      $$\begin{CD}
+      X @> \id >> X \\
+      @V \id VV @VV f VV \\
+      X @>> f > Y.
+      \end{CD}$$
+
+  - property: coregular
+    proof: >-
+      For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. It suffices to show regular monomorphisms are stable under pushouts. Thus, suppose we have two morphisms $f : (X, X') \to (Y, Y')$ and $g : (X, X') \to (Z, Z')$ where $f$ is a regular monomorphism, which means $f$ is injective and $X' = f^{-1}(Y')$. Then we can construct a pushout diagram
+      $$\begin{CD}
+      (X, X') @> f >> (Y, Y') \\
+      @V g VV @VV i_1 VV \\
+      (Z, Z') @>> i_2 > ((Y \setminus f(X)) \sqcup Z, i_1(Y') \cup i_2(Z')).
+      \end{CD}$$
+      Here $i_1$ sends $f(x) \mapsto g(x) \in Z$ for $x \in X$, and otherwise it sends $y \mapsto y$ for $y \in Y \setminus f(X)$; and $i_2$ is the inclusion of $Z$. We certainly have $i_2$ is injective; it remains to show $i_2^{-1}(i_1(Y') \cup i_2(Z')) = Z'$. However, we have
+      $$i_2^{-1}(i_1(Y') \cup i_2(Z')) = i_2^{-1}(i_1(Y')) \cup i_2^{-1}(i_2(Z'))$$
+      and obviously $i_2^{-1}(i_2(Z')) = Z'$. Therefore, it suffices to show $i_2^{-1}(i_1(Y')) \subseteq Z'$. Thus, suppose we have $z \in Z$ such that $i_2(z) \in i_1(Y')$. That means there exists $y' \in Y'$ such that $z = i_1(y')$. But in order for $i_1(y')$ to land in the $Z$ portion of $(Y \setminus f(X)) \sqcup Z$, we must have $i_1(y') \in f(X)$. That means there exists $x \in X$ such that $f(x) = y'$; and by the assumption on $f$, in fact $x \in X'$. Therefore, $i_2(g(x)) = i_1(f(x)) = y' = i_2(z)$, so $z = g(x) \in Z'$.
+
+  - property: co-Malcev
+    proof: >-
+      For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Thus, suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is surjective. Since $\Set$ is co-Malcev, it follows that $E \simeq X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $r(i_1(x)) = x \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case.
+
+  - property: effective cocongruences
+    proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \to X \sqcup_Y X$.'
+
+unsatisfied_properties:
+  - property: skeletal
+    proof: Consider the objects $X \xhookrightarrow{\id} X$ and $Y \xhookrightarrow{\id} Y$ for isomorphic but non-equal sets $X$ and $Y$.
+
+  - property: balanced
+    proof: The unique morphism from $0 \hookrightarrow 1$ to $1 \hookrightarrow 1$ is both a monomorphism and an epimorphism, but not an isomorphism (see descriptions below).
+
+  - property: cofiltered-limit-stable epimorphisms
+    proof: >-
+      Consider the sequence of epimorphisms
+      $$\begin{CD}
+      \IN_{\ge n} @> \id >> \IN_{\ge n} \\
+      @V ! VV @VV ! V \\
+      1 @>> \id > 1.
+      \end{CD}$$
+      The limit is
+      $$\begin{CD}
+      0 @> \id >> 0 \\
+      @V ! VV @VV ! V \\
+      1 @>> \id > 1
+      \end{CD}$$
+      which is not an epimorphism.
+
+  - property: Malcev
+    proof: This is clear since $\Set$ is not Malcev, and it has a left exact embedding in $\Mono$ via the functor sending a set $X$ to $X \xhookrightarrow{\id} X$.
+
+special_objects:
+  initial object:
+    description: the unique function $0 \to 0$
+  terminal object:
+    description: the unique function $1 \to 1$
+  coproducts:
+    description: component-wise defined disjoint union, equipped with the disjoint union of the functions
+  products:
+    description: component-wise defined cartesian product, equipped with the product function
+
+special_morphisms:
+  isomorphisms:
+    description: pairs $(\ell, r)$ where $\ell$ and $r$ are both bijections
+    proof: This is easy.
+  monomorphisms:
+    description: pairs $(\ell, r)$ where $r$ is an injective function, from which it automatically follows that $\ell$ is also injective
+    proof: For the non-trivial direction, use the fact that the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \hookrightarrow 1$.
+  epimorphisms:
+    description: pairs $(\ell, r)$ where $r$ is a surjective function
+    proof: >-
+      Suppose we have a morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ such that $r$ is surjective. To see it is an epimorphism, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X', Y', g) \rightrightarrows (T, U, h)$ such that $(\ell_1, r_1) \circ (\ell, r) = (\ell_2, r_2) \circ (\ell, r)$. Then $r_1 \circ r = r_2 \circ r$ implies $r_1 = r_2$. It automatically follows that $\ell_1 = \ell_2$ since $h$ is a monomorphism in $\Set$.
+
+      Conversely, suppose we have an epimorphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$. Then for any set $T$, the morphisms $(X', Y', g) \to (T, T, \id_T)$ are equivalent to the functions $Y' \to T$; therefore,  $r$ is an epimorphism in $\Set$.
+  regular monomorphisms:
+    description: >-
+      pairs $(\ell, r)$ where $r$ is an injective function and moreover the commutative square
+      $$\begin{CD}
+      X @> f >> Y \\
+      @V \ell VV @VV r V \\
+      X' @>> g > Y'
+      \end{CD}$$
+      is in fact a cartesian square
+    proof: >-
+      To show any regular monomorphism satisfies this condition, suppose we have an equalizer diagram
+      $$\begin{CD}
+      X @> f >> Y \\
+      @V \ell VV @VV r V \\
+      X' @> g >> Y' \\
+      @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\
+      X'' @>> h > Y''.
+      \end{CD}$$
+      Without loss of generality, we may assume $f$, $g$, $h$, $\ell$, and $r$ are all inclusion maps. Now suppose we have $y' \in Y'$ which is in the intersection of $X'$ and $Y$. Then $y' \in Y$ implies $r_1(y') = r_2(y')$. Therefore, since $h$ is injective, we can conclude $\ell_1(y') = \ell_2(y')$, so in fact $y' \in X$. This shows $X' \cap Y \subseteq X$; the other inclusion is automatic from the commutativity of the diagram.
+
+      To show any morphism satisfying this condition is a regular monomorphism, we may again assume $f$, $g$, $\ell$, and $r$ are all inclusion maps. We can then construct an equalizer diagram
+      $$\begin{CD}
+      X @> f >> Y \\
+      @V \ell VV @VV r V \\
+      X' @> g >> Y' \\
+      @V \chi_X V \top_{X'} V @V \chi_Y V \top_{Y'} V \\
+      \{ \top, \bot \} @> \id >> \{ \top, \bot \}.
+      \end{CD}$$
+      Here $\top_{X'}$ represents the constant function on $X'$ with value $\top$, and similarly for $\top_{Y'}$. Here, the assumption $X = X' \cap Y$ is used to establish the commutativity of the characteristic morphism $(\chi_X, \chi_Y) : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$.
+  regular epimorphisms:
+    description: pairs $(\ell, r)$ where both $\ell$ and $r$ are surjective functions
+    proof: >-
+      To show any regular epimorphism satisfies this condition, suppose we have a parallel pair
+      $$\begin{CD}
+      X @> f >> Y \\
+      @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\
+      X' @> g >> Y'.
+      \end{CD}$$
+      To form the coequalizer in $\Mono$, first we may form the coequalizer in $\Set^{\rightarrow}$, $\coeq(\ell_1, \ell_2) \xrightarrow{\bar g} \coeq(r_1, r_2)$. Note this is not injective in general; however, we may apply the reflector to get the coequalizer $\im(\bar g) \hookrightarrow \coeq(r_1, r_2)$ in $\Mono$. Here, clearly the map $Y' \to \coeq(r_1, r_2)$ is surjective. Likewise, both the functions $X' \to \coeq(\ell_1, \ell_2)$ and $coeq(\ell_1, \ell_2) \to \im(\bar g)$ are surjective, so their composition $X' \to \coeq(\ell_1, \ell_2)$ is surjective as well.
+
+      To show any morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ satisfying this condition is a regular epimorphism, note that the kernel pair of $(\ell, r)$ can be computed component-wise. Therefore, the coequalizer in $\Set^{\rightarrow}$ of this kernel pair is exactly $(X', Y', g)$, so applying the reflector does nothing and $(X', Y', g)$ is also the coequalizer in $\Mono$.

databases/catdat/data/categories/Set_arrow.yaml

@@ -20,6 +20,7 @@ related_categories:
   - Set
   - SetxSet
   - Sh(X)
+  - Mono
 
 satisfied_properties:
   - property: locally small

databases/catdat/data/macros.yaml

@@ -122,3 +122,4 @@
 \Pair: \mathbf{Pair}
 \Span: \mathbf{Span}
 \Arr: \mathbf{Arr}
+\Mono: \mathbf{Mono}