diff --git a/.cspell.json b/.cspell.json index 03cf06420..f0a1a8087 100644 --- a/.cspell.json +++ b/.cspell.json @@ -20,7 +20,8 @@ "networkidle", "devlog", "cech", - "Unif" + "Unif", + "noiso" ], "words": [ "abelian", diff --git a/database/data/categories/FinSet_even.yaml b/database/data/categories/FinSet_even.yaml index 43e010929..2c171deb8 100644 --- a/database/data/categories/FinSet_even.yaml +++ b/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 diff --git a/database/data/categories/FinSet_odd.yaml b/database/data/categories/FinSet_odd.yaml index 287f69795..4d5042b49 100644 --- a/database/data/categories/FinSet_odd.yaml +++ b/database/data/categories/FinSet_odd.yaml @@ -103,11 +103,6 @@ unsatisfied_properties: - property: natural numbers object proof: By Lemma 2 here, 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 $\FinSet_{3^\bullet}$ works here. - references: - - FinSet_power_3_not_multi-complete - special_objects: terminal object: description: singleton set diff --git a/database/data/categories/FinSet_power_3.yaml b/database/data/categories/FinSet_power_3.yaml index 1b91f9ce3..c8d2859b1 100644 --- a/database/data/categories/FinSet_power_3.yaml +++ b/database/data/categories/FinSet_power_3.yaml @@ -103,15 +103,6 @@ unsatisfied_properties: - property: natural numbers object proof: By Lemma 2 here, 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 bijective 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 diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index 8353be374..8774f2c40 100644 --- a/database/data/categories/Pos.yaml +++ b/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 $\PreOrd$. Now apply Lemma 10 here. + label: pos_extremal_generator references: - preord_extremal_generator @@ -71,7 +73,8 @@ 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 this result, $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: @@ -79,7 +82,7 @@ special_objects: 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 diff --git a/database/data/categories/Pos_noiso.yaml b/database/data/categories/Pos_noiso.yaml new file mode 100644 index 000000000..9c7030cae --- /dev/null +++ b/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 $\Pos$, 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 here.' + + - property: semi-strongly connected + proof: This property is inherited from $\Pos$. + + - property: extremal generator + proof: The ordered set $\{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. + references: + - preord_extremal_generator + + - property: extremal cogenerator + proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. + 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 $\Pos$ 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 here, 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 here, 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 $\Pos$, 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 $\Pos$. + regular monomorphisms: + description: embeddings + proof: 'We use the fact that the regular monomorphisms in $\Pos$ 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.' diff --git a/database/data/category-implications/equalizers.yaml b/database/data/category-implications/equalizers.yaml index de1cf8697..00b4cae00 100644 --- a/database/data/category-implications/equalizers.yaml +++ b/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. this result).' + - id: reflexive_pair_trivial_2 assumptions: - subobject-trivial diff --git a/database/data/category-properties/multi-cocomplete.yaml b/database/data/category-properties/multi-cocomplete.yaml index a7100425a..3f4ac56d6 100644 --- a/database/data/category-properties/multi-cocomplete.yaml +++ b/database/data/category-properties/multi-cocomplete.yaml @@ -1,6 +1,6 @@ id: multi-cocomplete relation: is -description: 'A multi-colimit 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 multi-colimit 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 diff --git a/database/data/category-properties/multi-complete.yaml b/database/data/category-properties/multi-complete.yaml index 0e77a032a..9091ba58d 100644 --- a/database/data/category-properties/multi-complete.yaml +++ b/database/data/category-properties/multi-complete.yaml @@ -1,6 +1,6 @@ id: multi-complete relation: is -description: 'A multi-limit 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 multi-limit 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 diff --git a/database/data/category-properties/multi-initial object.yaml b/database/data/category-properties/multi-initial object.yaml index ca7735368..e7ff72968 100644 --- a/database/data/category-properties/multi-initial object.yaml +++ b/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 multi-initial object 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 diff --git a/database/data/category-properties/multi-terminal object.yaml b/database/data/category-properties/multi-terminal object.yaml index 38a841d90..9b633fbbb 100644 --- a/database/data/category-properties/multi-terminal object.yaml +++ b/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 multi-terminal object 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 diff --git a/database/data/macros.yaml b/database/data/macros.yaml index f90e0a2c6..3a68c46ec 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -40,6 +40,7 @@ \ab: \mathrm{ab} \reg: \mathrm{reg} \fin: \mathrm{fin} +\noiso: \mathrm{noiso} # operators \Mor: \operatorname{Mor}