The category of posets without isolated points

.cspell.json

@@ -20,7 +20,8 @@
 		"networkidle",
 		"devlog",
 		"cech",
-		"Unif"
+		"Unif",
+		"noiso"
 	],
 	"words": [
 		"abelian",

database/data/categories/FinSet_even.yaml

@@ -90,7 +90,6 @@ unsatisfied_properties:
 
   - property: Cauchy complete
     proof: 'The constant map $e : \{0,1\} \to \{0,1\}$, $x \mapsto 0$ is idempotent and does not split in $\FinSet_{\even}$, since a splitting $\{0,1\} \to X \to \{0,1\}$ would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e) = \{0\}$.'
-    label: FinSet_even_not_cauchy_complete
 
   - property: extensive
     proof: >-
@@ -111,11 +110,6 @@ unsatisfied_properties:
       - FinSet_even_inclusion_continuous
       - FinSet_even_inclusion_cocontinuous
 
-  - property: multi-cocomplete
-    proof: 'Assume that $D : \I \to \FinSet_{\even}$ is a small diagram. If $(D(i) \to X)_{i \in \I}$ is any cocone, then the constant map $0 : X \to \{0,1\}$ is a morphism of cocones from $(D(i) \to X)_{i \in \I}$ to the cocone $(0 : D(i) \to \{0,1\})_{i \in \I}$. Therefore, the category of cocones under $D$ is connected; it has a weakly terminal object. Thus, if a multi-colimit of $D$ exists, it is necessarily a colimit of $D$. But since we already know that $\FinSet_{\even}$ is not cocomplete (for example, since it is not Cauchy complete), we are done.'
-    references:
-      - FinSet_even_not_cauchy_complete
-
 special_objects:
   initial object:
     description: empty set

database/data/categories/FinSet_odd.yaml

@@ -103,11 +103,6 @@ unsatisfied_properties:
   - property: natural numbers object
     proof: By Lemma 2 <a href="/content/natural_numbers_objects">here</a>, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. But there is no finite set with this property.
 
-  - property: multi-complete
-    proof: The same proof as for <a href="/category/FinSet_power_3">$\FinSet_{3^\bullet}$</a> works here.
-    references:
-      - FinSet_power_3_not_multi-complete
-
 special_objects:
   terminal object:
     description: singleton set

database/data/categories/FinSet_power_3.yaml

@@ -103,15 +103,6 @@ unsatisfied_properties:
   - property: natural numbers object
     proof: By Lemma 2 <a href="/content/natural_numbers_objects">here</a>, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. But there is no finite set with this property.
 
-  - property: multi-complete
-    proof: >-
-      Let $I$ be an infinite set and, for every $i \in I$, let $A_i$ be a set of cardinality $3$. Assume that the multi-product of the family $(A_i)_{i \in I}$ exists in $\FinSet_{3^\bullet}$, i.e. that the category of cones has a multi-terminal object. Here, a cone can be identified with a map
-      $$\textstyle f : X \to \prod_{i \in I} A_i,$$
-      where $X \in \FinSet_{3^\bullet}$ and the product is taken in $\Set$. Therefore, there is a family of cones $(p_j : P_j \to \prod_{i \in I} A_i)_{j \in J}$ such that for every cone $f : X \to \prod_{i \in I} A_i$ there is a unique index $j \in J$ and a unique map $g : X \to P_j$ such that $p_j \circ g = f$. Applying this to $X = \{0\}$, we see that the maps $p_j$ induce a <i>bijective</i> map
-      $$\textstyle\coprod_{j \in J} P_j \to \prod_{i \in I} A_i.$$
-      In particular, the images of the maps $p_j$ are pairwise disjoint. Since $\prod_{i \in I} A_i$ is an infinite set, $J$ is infinite. In particular, there are distinct indices $j_1,j_2 \in J$. Choose elements $y_1 \in P_{j_1}$ and $y_2 \in P_{j_2}$. There is a map $f : \{0,1,2\} \to \prod_{i \in I} A_i$ with image $\{p_{j_1}(y_1), p_{j_2}(y_2)\}$. By assumption, there is some (unique) index $k \in J$ such that $f$ factors through $p_k$. But then both $p_{j_1}(y_1)$ and $p_{j_2}(y_2)$ are contained in the image of $p_k$, so that $j_1 = k = j_2$, which is a contradiction.
-    label: FinSet_power_3_not_multi-complete
-
 special_objects:
   terminal object:
     description: singleton set

database/data/categories/Pos.yaml

@@ -13,6 +13,7 @@ related:
   - FinOrd
   - PreOrd
   - Mono
+  - Pos_noiso
 
 satisfied_properties:
   - property: locally small
@@ -36,6 +37,7 @@ satisfied_properties:
 
   - property: extremal generator
     proof: We have that $\{0<1\}$ is an extremal generator even in <a href="/category/PreOrd">$\PreOrd$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
+    label: pos_extremal_generator
     references:
       - preord_extremal_generator
 
@@ -71,15 +73,16 @@ unsatisfied_properties:
   - property: effective cocongruences
     proof: |-
       Let $X$ be $\IR$ with the standard (total) order, and let $E$ be the poset with underlying set $\IR \times \{ 0, 1 \}$ and partial order such that $(x, m) \le (y, n)$ if and only if $x < y$ or $(x, m) = (y, n)$. The two maps $\IR \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\IP, \le)$, the induced equivalence relation on the set of order-preserving functions $\IR \to \IP$ is that $f \sim g$ if and only if $f(x) \le g(y)$ and $g(x) \le f(y)$ whenever $x < y$. This relation is clearly reflexive and symmetric; for transitivity, if $f \sim g$ and $g \sim h$, then whenever $x < y$, we have $f(x) \le g(\frac{x+y}{2}) \le h(y)$ and similarly $h(x) \le g(\frac{x+y}{2}) \le f(y)$, showing that $f \sim h$.
-      On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of <a href="/content/effective-congruence-quotients">this result</a>, $E$ would be the cokernel pair of the equalizer of the two maps $\IR \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.
+      On the other hand, if this cocongruence on $\IR$ were effective, i.e. the cokernel pair of some order-preserving map $P \to \IR$, then $P$ must be empty since the two maps $\IR \rightrightarrows E$ agree nowhere. So $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.
+    label: Pos_no_effective_cocongruences
 
 special_objects:
   initial object:
     description: empty poset
   terminal object:
     description: singleton poset
   coproducts:
-    description: disjoint union with the obvious partial order that leaves the distinct summands incomparable
+    description: disjoint union with the obvious partial order in which distinct summands are incomparable
   products:
     description: direct products with the evident partial order
 

database/data/categories/Pos_noiso.yaml

@@ -0,0 +1,111 @@
+id: Pos_noiso
+name: category of partially ordered sets without isolated points
+notation: $\Pos_{\noiso}$
+objects: partially ordered sets that have no isolated points
+morphisms: order-preserving functions
+description: Here, a point is called isolated if it is not comparable to any other point. Thus, we consider partially ordered sets whose connected components have cardinality $\geq 2$. This category provides an example of an infinitary extensive category that is not Cauchy complete.
+nlab_link: null
+
+tags:
+  - order theory
+
+related:
+  - Pos
+
+satisfied_properties:
+  - property: locally small
+    proof: It is a full subcategory of <a href="/category/Pos">$\Pos$</a>, which is locally small.
+
+  - property: binary products
+    proof: Let $P,Q$ be two posets without isolated points. Then $P \times Q$ has no isolated points, because if a point $(p,q) \in P \times Q$ is isolated, it is easy to check that $p$ is isolated as well.
+
+  - property: infinitary extensive
+    proof: 'It is easy to check that $\Pos_{\noiso} \hookrightarrow \Pos$ is closed under coproducts. If $f : X \to P + Q$ is an order-preserving map, where $X,P,Q$ have no isolated points, then the preimage $f^*(P)$ also has no isolated points. In fact, if $x \in f^*(P)$, then there is some $y \neq x$ in $X$ that is comparable to $x$, since $X$ has no isolated points. Then $f(x) \in P$ and $f(y)$ is comparable to $f(x)$. It follows that $f(y) \in P$, and hence $y \in f^*(P)$. We conclude the proof with Lemma 11 <a href="/content/subcategories">here</a>.'
+
+  - property: semi-strongly connected
+    proof: This property is inherited from <a href="/category/Pos">$\Pos$</a>.
+
+  - property: extremal generator
+    proof: The ordered set $\{0 < 1\}$ is an extremal generator, even for <a href="/category/PreOrd">$\PreOrd$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
+    references:
+      - preord_extremal_generator
+
+  - property: extremal cogenerator
+    proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for <a href="/category/Pos">$\Pos$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
+    references:
+      - pos_extremal_cogenerator
+
+  - property: well-powered
+    proof: This follows from the description of monomorphisms below.
+
+  - property: well-copowered
+    proof: This follows from the description of epimorphisms below.
+
+  - property: ℵ₁-filtered
+    proof: In fact, every small diagram has a cocone. Simply take the colimit in <a href="/category/Pos">$\Pos$</a> and then map it to $\{0 < 1\}$ via a constant map.
+
+  - property: cokernel pairs
+    proof: Let $P \to Q$ be an order-preserving map between posets without isolated points. We show that the poset $Q \sqcup_P Q$, constructed as the poset reflection of the pushout in $\PreOrd$, also has no isolated points. Notice that the inclusion maps $Q \twoheadrightarrow Q \sqcup_P Q$ are injective because the codiagonal $Q \sqcup_P Q \to Q$ provides a retraction. Every point in $Q \sqcup_P Q$ lies in the image of one of the two inclusion maps. Let us say that it comes from a point $q \in Q$ in the first copy. Since $q$ is not isolated, it is comparable to a point $q' \in Q$ distinct from $q$. Since the inclusion map into $Q \sqcup_P Q$ is injective, the images of $q$ and $q'$ are also distinct, and of course they are still comparable.
+
+unsatisfied_properties:
+  - property: skeletal
+    proof: This is trivial.
+
+  - property: terminal object
+    proof: Assume that there is a terminal object $P$. In particular, there is exactly one order-preserving map $\{0 < 1\} \to P$. Since every constant map is order-preserving, it follows that $P$ has exactly one element. But then $P$ has an isolated point.
+
+  - property: strongly connected
+    proof: There is no map $\{0 < 1\} \to \varnothing$.
+
+  - property: Cauchy complete
+    proof: The constant map $\{0 < 1\} \to \{0 < 1\}$, $x \mapsto 0$ does not split, because a splitting would also be a splitting in $\Pos$, therefore isomorphic to $\{0 < 1\} \twoheadrightarrow \{0\} \hookrightarrow \{0 < 1\}$. But $\{0\}$ has an isolated point.
+
+  - property: balanced
+    proof: The inclusion of $\{0 < 1\} \sqcup \{2 < 3\}$ (which has two components) into $\{0 < 1 < 2 < 3\}$ provides a counterexample.
+
+  - property: kernel pairs
+    proof: >-
+      First, we observe that the inclusion functor $\Pos_{\noiso} \hookrightarrow \Pos$ is continuous. This follows from the dual of Lemma 1 <a href="/content/inclusion-functors">here</a>, since $\Pos_{\noiso}$ contains the extremal generator $\{0 < 1\}$ of $\Pos$. Therefore, it suffices to find a morphism in $\Pos_{\noiso}$ whose kernel pair in $\Pos$ has an isolated point.
+      Consider the epimorphism $f : \{0 < 1\} \sqcup \{1' < 2\} \to \{0 < 1 < 2\}$ that identifies $1$ and $1'$. The kernel pair has the elements
+      $$(0,0),(1,1),(1',1'),(2,2),(1,1'),(1',1).$$
+      It is easy to check that the element $(1,1')$ is isolated.
+    references:
+      - pos_extremal_generator
+    label: Pos_noiso_inclusion_continuous
+
+  - property: equalizers of cokernel pairs
+    proof: Consider the constant order-preserving map $\{0 < 1\} \to \{0 < 1\}$, $x \mapsto 0$. Its cokernel pair is $\{0 < 1, 0 < 1'\}$ with the two obvious maps from $\{0 < 1\}$. Since we have seen above that the inclusion functor $\Pos_{\noiso} \hookrightarrow \Pos$ is continuous, the equalizer of $\{0 < 1\} \rightrightarrows \{0 < 1, 0 < 1'\}$ must be the poset $\{0\}$, which, however, has an isolated point.
+    references:
+      - Pos_noiso_inclusion_continuous
+
+  - property: quotients of congruences
+    proof: The inclusion functor $\Pos_{\noiso} \hookrightarrow \Pos$ is cocontinuous by Lemma 1 <a href="/content/inclusion-functors">here</a>, since $\Pos_{\noiso}$ contains the extremal cogenerator $\{0 < 1\}$ of $\Pos$. Therefore, it suffices to find a congruence whose quotient in $\Pos$ has an isolated point. Take any non-empty poset $X$ without isolated points, such as $\{0 < 1\}$, and consider the maximal congruence $X \times X \rightrightarrows X$. Its quotient in $\Pos$ is just $\{\ast\}$, which therefore has an isolated point.
+    references:
+      - pos_extremal_cogenerator
+
+  - property: effective cocongruences
+    proof: We can reuse the proof from <a href="/category/Pos">$\Pos$</a>, since the posets considered there have no isolated points.
+    references:
+      - Pos_no_effective_cocongruences
+
+special_objects:
+  initial object:
+    description: empty poset
+  coproducts:
+    description: disjoint union with the obvious partial order in which distinct summands are incomparable
+  products:
+    description: '[non-empty case] direct products with the evident partial order'
+
+special_morphisms:
+  isomorphisms:
+    description: bijective functions that are order-preserving and order-reflecting
+    proof: This is easy.
+  monomorphisms:
+    description: injective order-preserving functions
+    proof: 'For the non-trivial direction, assume that $f : P \to Q$ is a monomorphism and $a,b \in P$ satisfy $f(a)=f(b)$. Consider the two constant maps $c_a, c_b : \{0 < 1\} \to P$ with values $a$ and $b$. These are valid morphisms in $\Pos_{\noiso}$. Then $f \circ c_a = f \circ c_b$, so $c_a = c_b$, which means that $a = b$.'
+  epimorphisms:
+    description: surjective order-preserving functions
+    proof: We can use the same proof as for <a href="/category/Pos">$\Pos$</a>.
+  regular monomorphisms:
+    description: embeddings
+    proof: 'We use the fact that the regular monomorphisms in <a href="/category/Pos">$\Pos$</a> are precisely the embeddings, but we have to be a little careful since $\Pos_{\noiso}$ does not have all finite (co-)limits. If $P \to Q$ is an embedding of posets without isolated points, we have seen in the proof for $\Pos$ that it is the equalizer of its cokernel pair $Q \rightrightarrows Q \sqcup_P Q$ in $\Pos$. Moreover, we have seen above that this cokernel pair has no isolated points. It follows that $P \to Q$ is a regular monomorphism in $\Pos_{\noiso}$. Conversely, suppose that $P \to Q$ is a regular monomorphism in $\Pos_{\noiso}$. Since we already know that the inclusion functor $\Pos_{\noiso} \hookrightarrow \Pos$ is continuous, it follows that $P \to Q$ is also a regular monomorphism in $\Pos$. Therefore, it is an embedding.'

database/data/category-implications/equalizers.yaml

@@ -30,6 +30,13 @@
     - Cauchy complete
   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: multi_equalizers_consequence
+  assumptions:
+    - multi-complete
+  conclusions:
+    - Cauchy complete
+  proof: 'More precisely, if a category has multi-equalizers, then it is Cauchy complete. Namely, if $e : X \to X$ is an idempotent morphism, a cone over $e,\id_X$ is a morphism $f : Y \to X$ with $f = e \circ f$. In particular, $e : X \to X$ is such a cone, and $f$ can be regarded as a morphism of cones $f \to e$. This shows that the category of cones is connected. A multi-terminal object in the category of cones is therefore a terminal object, i.e. an equalizer of $e,\id_X$, and hence a splitting of $e$ (cf. <a href="/category-implication/equalizers_consequence">this result</a>).'
+
 - id: reflexive_pair_trivial_2
   assumptions:
     - subobject-trivial

database/data/category-properties/multi-cocomplete.yaml

@@ -1,6 +1,6 @@
 id: multi-cocomplete
 relation: is
-description: 'A <i>multi-colimit</i> of a diagram $D : \S \to \C$ is a set $I$ of cocones under $D$ such that every cocone under $D$ uniquely factors through a unique cocone belonging to $I$. This property refers to the existence of multi-colimits of small diagrams. Note that any diagram with no cocone admits a multi-colimit, which is the empty set of cocones.'
+description: 'A <i>multi-colimit</i> of a diagram $D : \S \to \C$ is a set $I$ of cocones under $D$ such that every cocone under $D$ uniquely factors through a unique cocone belonging to $I$. In other words, it is a multi-initial object in the category of cocones. This property refers to the existence of multi-colimits of small diagrams. Note that any diagram with no cocone admits a multi-colimit, which is the empty set of cocones.'
 nlab_link: https://ncatlab.org/nlab/show/multilimit
 dual: multi-complete
 invariant_under_equivalences: true

database/data/category-properties/multi-complete.yaml

@@ -1,6 +1,6 @@
 id: multi-complete
 relation: is
-description: 'A <i>multi-limit</i> of a diagram $D : \S \to \C$ is a set $I$ of cones over $D$ such that every cone over $D$ uniquely factors through a unique cone belonging to $I$. This property refers to the existence of multi-limits of small diagrams. Note that any diagram with no cone admits a multi-limit, which is the empty set of cones.'
+description: 'A <i>multi-limit</i> of a diagram $D : \S \to \C$ is a set $I$ of cones over $D$ such that every cone over $D$ uniquely factors through a unique cone belonging to $I$. In other words, it is a multi-terminal object in the category of cones. This property refers to the existence of multi-limits of small diagrams. Note that any diagram with no cone admits a multi-limit, which is the empty set of cones.'
 nlab_link: https://ncatlab.org/nlab/show/multilimit
 dual: multi-cocomplete
 invariant_under_equivalences: true

database/data/category-properties/multi-initial object.yaml

@@ -1,6 +1,6 @@
 id: multi-initial object
 relation: has a
-description: This property refers to the existence of a multi-colimit of the empty diagram. A category has a multi-initial object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a initial object.
+description: A category has a <i>multi-initial object</i> if the empty diagram has a multi-colimit. That is, there is a small family of objects $(X_i)_{i \in I}$ such that for every object $Y$ there is a unique index $i \in I$ with a unique morphism $X_i \to Y$. A category has a multi-initial object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a initial object.
 nlab_link: https://ncatlab.org/nlab/show/multilimit
 dual: multi-terminal object
 invariant_under_equivalences: true

database/data/category-properties/multi-terminal object.yaml

@@ -1,6 +1,6 @@
 id: multi-terminal object
 relation: has a
-description: This property refers to the existence of a multi-limit of the empty diagram. A category has a multi-terminal object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a terminal object.
+description: A category has a <i>multi-terminal object</i> if the empty diagram has a multi-limit. That is, there is a small family of objects $(X_i)_{i \in I}$ such that for every object $Y$ there is a unique index $i \in I$ with a unique morphism $Y \to X_i$. A category has a multi-terminal object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a terminal object.
 nlab_link: https://ncatlab.org/nlab/show/multilimit
 dual: multi-initial object
 invariant_under_equivalences: true

database/data/macros.yaml

@@ -40,6 +40,7 @@
 \ab: \mathrm{ab}
 \reg: \mathrm{reg}
 \fin: \mathrm{fin}
+\noiso: \mathrm{noiso}
 
 # operators
 \Mor: \operatorname{Mor}