diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index e8f3eb6a..98d82300 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/databases/catdat/data/categories/FI.yaml @@ -14,6 +14,7 @@ related_categories: - B - FS - FinSet + - Mono satisfied_properties: - property: locally small diff --git a/databases/catdat/data/categories/Mono.yaml b/databases/catdat/data/categories/Mono.yaml new file mode 100644 index 00000000..feb44e26 --- /dev/null +++ b/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 here, 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$. diff --git a/databases/catdat/data/categories/Set_arrow.yaml b/databases/catdat/data/categories/Set_arrow.yaml index 3a9c2d79..089f1342 100644 --- a/databases/catdat/data/categories/Set_arrow.yaml +++ b/databases/catdat/data/categories/Set_arrow.yaml @@ -20,6 +20,7 @@ related_categories: - Set - SetxSet - Sh(X) + - Mono satisfied_properties: - property: locally small diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 844eb044..41701714 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -122,3 +122,4 @@ \Pair: \mathbf{Pair} \Span: \mathbf{Span} \Arr: \mathbf{Arr} +\Mono: \mathbf{Mono}