From 7848ac7d9e9ad8cd97e84aa529e2f9ee1beafb54 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 12:27:20 +0100 Subject: [PATCH] consistent notation of empty sets, singletons, and two-element sets --- CLAUDE.md | 1 + CONTRIBUTING.md | 7 ++-- content/congruences_in_rel.md | 2 +- content/functors_on_discrete_categories.md | 6 ++-- content/thin_algebraic_categories.md | 4 +-- database/data/categories/Cat.yaml | 6 ++-- database/data/categories/CompHaus.yaml | 2 +- database/data/categories/Euclid_coprod.yaml | 2 +- database/data/categories/FI.yaml | 6 ++-- database/data/categories/FS.yaml | 4 +-- database/data/categories/FinSet.yaml | 2 +- database/data/categories/FinSet_odd.yaml | 4 +-- database/data/categories/FinSet_power_3.yaml | 4 +-- database/data/categories/Haus.yaml | 8 ++--- database/data/categories/Man.yaml | 2 +- database/data/categories/Meas.yaml | 12 +++---- database/data/categories/Met.yaml | 10 +++--- database/data/categories/Met_c.yaml | 4 +-- database/data/categories/PMet.yaml | 6 ++-- database/data/categories/Pos.yaml | 2 +- database/data/categories/PreOrd.yaml | 4 +-- database/data/categories/Quiv_fc.yaml | 4 +-- database/data/categories/SeqSet.yaml | 6 ++-- database/data/categories/SeqSet_conn.yaml | 10 +++--- database/data/categories/Set.yaml | 4 +-- database/data/categories/Set_arrow.yaml | 8 ++--- database/data/categories/Set_c.yaml | 6 ++-- database/data/categories/Set_family.yaml | 2 +- .../data/categories/Set_family_mostly_0.yaml | 6 ++-- .../data/categories/Set_family_mostly_1.yaml | 32 ++++++++--------- database/data/categories/Set_ff.yaml | 8 ++--- database/data/categories/Setne.yaml | 2 +- database/data/categories/Sh(X).yaml | 2 +- database/data/categories/Sp.yaml | 8 ++--- database/data/categories/Top.yaml | 4 +-- database/data/categories/Top_pointed.yaml | 4 +-- database/data/categories/Unif.yaml | 6 ++-- database/data/categories/Z.yaml | 2 +- .../cocompletion-discrete-pair-join.yaml | 10 +++--- .../categories/forked_commutative_square.yaml | 8 ++--- database/data/categories/omega-Set.yaml | 36 +++++++++---------- database/data/categories/sSet.yaml | 2 +- .../category-implications/generators.yaml | 2 +- .../data/functor-implications/adjoints.yaml | 2 +- .../limits preservation.yaml | 2 +- database/data/functor-implications/misc.yaml | 4 +-- .../data/functors/binary_coproduct_sets.yaml | 4 +-- .../data/functors/binary_product_sets.yaml | 4 +-- .../data/functors/continuous_functions.yaml | 4 +-- .../data/functors/countable_copower_sets.yaml | 2 +- database/data/functors/nerve.yaml | 2 +- .../functors/power_set_contravariant.yaml | 4 +-- .../data/functors/power_set_covariant.yaml | 6 ++-- database/data/functors/rational_product.yaml | 2 +- database/data/functors/sequences_sets.yaml | 2 +- .../data/functors/simple_group_probing.yaml | 2 +- database/data/functors/squaring_sets.yaml | 6 ++-- database/data/functors/trivial_BG.yaml | 2 +- database/data/functors/trivial_Idem.yaml | 6 ++-- database/data/functors/trivial_groups.yaml | 2 +- database/data/functors/trivial_sets.yaml | 2 +- .../walking_morphism_representation.yaml | 4 +-- database/data/morphisms/terminal-map.yaml | 8 ++--- .../1_tensor.yaml | 4 +-- .../Cat_cartesian.yaml | 2 +- .../Set_cartesian.yaml | 2 +- .../Set_cocartesian.yaml | 2 +- .../Top_cartesian.yaml | 2 +- .../strict.yaml | 2 +- 69 files changed, 178 insertions(+), 176 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 555f15bd6..b2f5227f6 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -102,6 +102,7 @@ Writing and notation conventions: - Write `non-empty`, `non-unital`, `non-expansive` (with a hyphen). - Use `\varnothing` (not `\emptyset`), `f : X \to Y` (not `\colon`), and `\coloneqq` (not `:=`). +- Write concrete sets as `\varnothing`, `\{\ast\}`, `\{0,1\}` (or `\{a,b\}`), never as `0`, `1`, `2`. This also applies to the initial and terminal objects of a specific category (e.g. `x : \{\ast\} \to X` in `\Set`, the trivial category `\1`, or "the terminal object $T$" of a presheaf category). Only abstract initial and terminal objects in statements about arbitrary categories, monoidal units, and the zero and trivial objects of algebra (the zero module $0$, the trivial group $1$) may be called `0` and `1`. - Write parallel morphisms as `f,g : A \rightrightarrows B`. - Never use one-off font commands such as `\mathcal`, `\mathrm`, `\mathbf`, or `\operatorname` directly. Reuse a macro from [database/data/macros.yaml](database/data/macros.yaml) (e.g. `\IN`, `\Grp`, `\Ab`, `\C`, `\Q`, `\T`) or define a new one there. - In displayed formulas containing `\prod` or `\coprod`, add `\textstyle` for the more compact layout, e.g. `$$\textstyle h : A \to \prod_{i \in I} Q_i$$`. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ee2098002..ba701d399 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -179,9 +179,10 @@ As a practical guideline, avoid introducing more than four properties (or four c 1. Write `non-empty`, not `nonempty`. Same for `non-unital`, `non-expansive`, etc. 2. Use `\varnothing` to display the empty set, not `\emptyset`. -3. For declarations of functions or morphisms, use `f : X \to Y`, not `f \colon X \to Y`. -4. For definitions, use `\coloneqq` instead of `:=`. -5. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](database/data/macros.yaml). +3. Write concrete sets explicitly, not as `0`, `1`, `2`: the empty set as `\varnothing`, a singleton as `\{\ast\}`, a two-element set as `\{0,1\}` or `\{a,b\}`, also when they are initial or terminal objects (e.g. `x : \{\ast\} \to X` in `\Set`). +4. For declarations of functions or morphisms, use `f : X \to Y`, not `f \colon X \to Y`. +5. For definitions, use `\coloneqq` instead of `:=`. +6. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](database/data/macros.yaml). ### Citations diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md index 5bd5807b9..b79b259e7 100644 --- a/content/congruences_in_rel.md +++ b/content/congruences_in_rel.md @@ -12,7 +12,7 @@ $$R_* : P(X) \to P(Y),\, S \mapsto \bigl\{ y\in Y \mid \exists x\in S, (x, y) \i is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\Set$. In particular, we get $$i_* : P(E) \to P(X + X) \cong P(X) \times P(X)$$ -which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $q_1, q_2$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions. +which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $q_1, q_2$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object $\{\ast\}$, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions. Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \id$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\Set$. diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md index 55da32655..74c230b31 100644 --- a/content/functors_on_discrete_categories.md +++ b/content/functors_on_discrete_categories.md @@ -7,14 +7,14 @@ description: We describe which functors on discrete categories are continuous or Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited. -First, we consider the trivial case $\S = 1$. +First, we consider the trivial case $\S = \1$. ::: Lemma 1 -Consider the trivial category $1 = \{0\}$ with a unique object $0$. Let $F : 1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$. +Consider the trivial category $\1$ with a unique object $0$. Let $F : \1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$. ::: ::: Proof -If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal. +If $F$ is continuous, it preserves terminal objects. Since $0 \in \1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to \1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal. ::: ::: Lemma 2 diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md index c83b4569f..19f357101 100644 --- a/content/thin_algebraic_categories.md +++ b/content/thin_algebraic_categories.md @@ -12,11 +12,11 @@ Evaluate later if we want to remove it. --> ::: Lemma -Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism. +Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq \1$ or $\C \simeq I$, where $I$ is the walking morphism. ::: ::: Proof -Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$; there is a morphism $0 \to F(1)$ but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. +Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(\{\ast\})$, which means it is either the initial object $0$ or $F(\{\ast\})$ itself (since $\C$ is thin). If $F(\{\ast\}) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(\{\ast\})$; there is a morphism $0 \to F(\{\ast\})$ but no morphism $F(\{\ast\}) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. ::: Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator). diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 861621557..40fd17bc3 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -91,9 +91,9 @@ unsatisfied_properties: - property: cototal # TODO: refactor this once we add "hypercocomplete" proof: >- - In fact, it is not hypercocomplete. For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $1 \dottedrightrightarrows B G_\kappa \to \C$ is essentially small: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. + In fact, it is not hypercocomplete. For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $\1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $\1 \dottedrightrightarrows B G_\kappa \to \C$ is essentially small: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $\1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. - On the other hand, we claim that $1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$, showing that it is not hypercocomplete. To see this, suppose we have a pushout $\C$ of $1 \dottedrightrightarrows B G_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$ (which is possible since $\C$ is a small category). Then the coprojection $i_\lambda : B G_\lambda \to \C$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows B G_\kappa \to B G_\lambda$ in which $B G_\kappa \to B G_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B G_\lambda \to B G_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B G_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $G_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $G_\lambda$ has cardinality $\lambda$. + On the other hand, we claim that $\1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$, showing that it is not hypercocomplete. To see this, suppose we have a pushout $\C$ of $\1 \dottedrightrightarrows B G_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$ (which is possible since $\C$ is a small category). Then the coprojection $i_\lambda : B G_\lambda \to \C$ must be split monic, since we can construct a cocone $\1 \dottedrightrightarrows B G_\kappa \to B G_\lambda$ in which $B G_\kappa \to B G_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B G_\lambda \to B G_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B G_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $G_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $G_\lambda$ has cardinality $\lambda$. label: Cat_not_cototal special_objects: @@ -112,7 +112,7 @@ special_morphisms: proof: This is easy. monomorphisms: description: faithful functors that are injective on objects - proof: 'Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : 1 \rightrightarrows \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \rightrightarrows B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \rightrightarrows \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.' + proof: 'Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : \1 \rightrightarrows \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \rightrightarrows B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \rightrightarrows \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.' epimorphisms: description: 'A functor $F : \C \to \D$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\D$ there is a zigzag over $U \coloneqq F(\C)$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \D$ and $y_1,\dotsc,y_m \in \D$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.' proof: This is an extension of the corresponding theorem for monoids and proven by Isbell. diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index f75a6ddf4..709bc7481 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -76,7 +76,7 @@ unsatisfied_properties: - property: parametrized natural numbers object proof: >- - Let $I \coloneqq [0, 1]$. If a parametrized natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition + Let $I \coloneqq [0, 1]$. If a parametrized natural numbers object $(N, z : \{\ast\} \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition $$\begin{align*} I & \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I, \\ x & \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1}, diff --git a/database/data/categories/Euclid_coprod.yaml b/database/data/categories/Euclid_coprod.yaml index b3bcd1526..77f4eb6cb 100644 --- a/database/data/categories/Euclid_coprod.yaml +++ b/database/data/categories/Euclid_coprod.yaml @@ -21,7 +21,7 @@ satisfied_properties: proof: It is a full subcategory of $\Top$, which is locally small. - property: finite products - proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0=1$ and $\IR^n \times \IR^m \cong \IR^{n+m}$. + proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0 = \{0\}$ and $\IR^n \times \IR^m \cong \IR^{n+m}$. - property: infinitary extensive proof: The free coproduct completion of any category is infinitary extensive; for the finite case see Carboni–Lack–Walters, Proposition 2.4. diff --git a/database/data/categories/FI.yaml b/database/data/categories/FI.yaml index 08a45e382..6d5f5ad0c 100644 --- a/database/data/categories/FI.yaml +++ b/database/data/categories/FI.yaml @@ -65,12 +65,12 @@ unsatisfied_properties: proof: This is trivial. - property: cogenerator - proof: Let $Q$ be a finite set. When $Q$ is empty, it is clearly no cogenerator. Otherwise, $Q + 1$ has at least two elements, so that there are two different morphisms $1 \rightrightarrows Q + 1$. But there is no morphism $Q + 1 \to Q$ at all. Hence, $Q$ is no cogenerator. + proof: Let $Q$ be a finite set. When $Q$ is empty, it is clearly no cogenerator. Otherwise, $Q \sqcup \{\ast\}$ has at least two elements, so that there are two different morphisms $\{\ast\} \rightrightarrows Q \sqcup \{\ast\}$. But there is no morphism $Q \sqcup \{\ast\} \to Q$ at all. Hence, $Q$ is no cogenerator. - property: binary powers proof: >- - Assume that two finite sets $X,Y$ have a product $P$ in this category. Elements of $P$ are the same as maps $1 \to P$, and they are automatically injective. Therefore, - $$P \cong \Hom(1,P) \cong \Hom(1,X) \times \Hom(1,Y) \cong X \times Y,$$ + Assume that two finite sets $X,Y$ have a product $P$ in this category. Elements of $P$ are the same as maps $\{\ast\} \to P$, and they are automatically injective. Therefore, + $$P \cong \Hom(\{\ast\},P) \cong \Hom(\{\ast\},X) \times \Hom(\{\ast\},Y) \cong X \times Y,$$ and the projections must agree as well. But they are usually not injective. In particular, the product $X \times X$ never exists when $X$ has $>1$ elements. - property: sequential colimits diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index 479c8627a..7c7709532 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -73,7 +73,7 @@ unsatisfied_properties: proof: Its core is $\IB$, which we know is not thin. - property: generator - proof: Let $G$ be a finite set. There are at least two morphisms $G + 2 \rightrightarrows 2$, but there is no morphism $G \to G + 2$ at all. Hence, $G$ is not a generator. + proof: Let $G$ be a finite set. There are at least two morphisms $G \sqcup \{0,1\} \rightrightarrows \{0,1\}$, but there is no morphism $G \to G \sqcup \{0,1\}$ at all. Hence, $G$ is not a generator. - property: connected proof: 'If $f : \varnothing \to X$ is surjective, then $X = \varnothing$, and if $f : X \to \varnothing$ is any map, then also $X = \varnothing$. This shows that $\{ \varnothing \}$ is a connected component in this category. (The other connected component consists of all non-empty finite sets.)' @@ -82,7 +82,7 @@ unsatisfied_properties: proof: 'Let $X_n \coloneqq \{1,\dotsc,n\}$. We define the truncation $p_n : X_{n+1} \to X_n$ by extending the identity of $X_n$ with $p_n(n+1) \coloneqq n$. Assume the sequence of truncations $\cdots \to X_2 \to X_1$ has a limit $(f_n : X \to X_n)$ in this category. But $f_n$ is surjective, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.' - property: binary copowers - proof: Assume that the copower $X \coloneqq 2+2$ exists. Since we have a surjective map $2 \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to 2$ shows that $X$ has at least $2$ elements. Thus, $X \cong 2$. For all finite sets $Y$ we get a bijection $\Hom(2,Y) \cong \Hom(2,Y)^2$, in particular the cardinalities are the same. For $Y=2$ this gives the contradiction $2 = 4$. + proof: Let $T \coloneqq \{0,1\}$ and assume that the copower $X \coloneqq T + T$ exists. Since we have a surjective map $T \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to T$ shows that $X$ has at least $2$ elements. Thus, $X \cong T$. For all finite sets $Y$ we get a bijection $\Hom(T,Y) \cong \Hom(T,Y)^2$, in particular the cardinalities are the same. For $Y = T$ this gives the contradiction $2 = 4$. - property: locally cocartesian coclosed proof: >- diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 34320ae42..3035325aa 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -60,7 +60,7 @@ unsatisfied_properties: proof: This is trivial. - 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. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property. label: FinSet_no_NNO special_objects: diff --git a/database/data/categories/FinSet_odd.yaml b/database/data/categories/FinSet_odd.yaml index a78849b86..2d3b57f51 100644 --- a/database/data/categories/FinSet_odd.yaml +++ b/database/data/categories/FinSet_odd.yaml @@ -80,13 +80,13 @@ unsatisfied_properties: proof: 'The map $e : \{0,1,2\} \to \{0,1,2\}$, $0 \mapsto 0$, $1 \mapsto 1$, $2 \mapsto 1$ is idempotent and does not split in $\FinSet_{\odd}$, since a splitting $\{0,1,2\} \to X \to \{0,1,2\}$ would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e) = \{0,1\}$.' - property: cofiltered - proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{\odd}$ such that $! : X \to \{*\}$ factors through $\varnothing$, i.e. $X = \varnothing$, which is not a valid object of $\FinSet_{\odd}$.' + proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{\odd}$ such that $! : X \to \{\ast\}$ factors through $\varnothing$, i.e. $X = \varnothing$, which is not a valid object of $\FinSet_{\odd}$.' - property: binary copowers proof: A direct proof is possible, but it is best to first establish that the inclusion functor $\FinSet_{\odd} \hookrightarrow \Set$ is cocontinuous. This follows from Lemma 1 here since $\FinSet_{\odd}$ contains the extremal cogenerator $\{0,1,2\}$ of $\Set$. Therefore, binary copowers exist only if $\FinSet_{\odd}$ is closed under binary copowers in $\Set$. But $\{0\} \sqcup \{0\}$ does not have odd cardinality. - 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. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property. special_objects: terminal object: diff --git a/database/data/categories/FinSet_power_3.yaml b/database/data/categories/FinSet_power_3.yaml index 343519875..d439cf76c 100644 --- a/database/data/categories/FinSet_power_3.yaml +++ b/database/data/categories/FinSet_power_3.yaml @@ -71,7 +71,7 @@ unsatisfied_properties: proof: 'Consider the idempotent map $e : \{0,1,2\} \to \{0,1,2\}$ defined by $e(0)=0$, $e(1)=1$, $e(2)=1$. If it splits in $\FinSet_{3^\bullet}$ as $\{0,1,2\} \to X \to \{0,1,2\}$, this would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e)=\{0,1\}$. But then $X$ is not a valid object of $\FinSet_{3^\bullet}$.' - property: cofiltered - proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{3^\bullet}$ such that $! : X \to \{*\}$ factors through $\varnothing$, i.e. $X = \varnothing$, but $0$ is not a power of $3$.' + proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{3^\bullet}$ such that $! : X \to \{\ast\}$ factors through $\varnothing$, i.e. $X = \varnothing$, but $0$ is not a power of $3$.' - property: binary copowers proof: >- @@ -96,7 +96,7 @@ unsatisfied_properties: - FinSet_power_3_inclusion_cocontinuous - 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. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property. special_objects: terminal object: diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 05e6ab251..2a3ce2f4b 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -63,14 +63,14 @@ unsatisfied_properties: proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff). - property: regular subobject classifier - proof: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$). + proof: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = \{\ast\}$, we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, it must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$). label: Haus_no_regular_subobject_classifier - property: cartesian filtered colimits proof: 'It is shown in MSE/1255678 that $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits (so that it cannot be a left adjoint). The same example also works in $\Haus$: Surely $\IQ$ is Hausdorff, $X_n$ is Hausdorff, as is their colimit $X$, and the colimit (taken in $\Top$) of the $X_n \times \IQ$ admits a bijective continuous map to a Hausdorff space, therefore is also Hausdorff, meaning it is also the colimit taken in $\Haus$.' - property: cofiltered-limit-stable epimorphisms - proof: 'The following is a basic counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' + proof: 'The following is a basic counterexample for sets: The unique maps $\IN_{\geq n} \to \{\ast\}$ are surjective, but their limit $\varnothing = \bigcap_{n \geq 0} \IN_{\geq n} \to \{\ast\}$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' - property: filtered-colimit-stable monomorphisms proof: >- @@ -96,9 +96,9 @@ unsatisfied_properties: proof: >- In fact, it is not hypercocomplete. For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich, there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) - Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. + Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $\{\ast\} \dottedrightrightarrows X_\kappa$ where each morphism $\{\ast\} \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $\{\ast\} \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $\{\ast\} \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. - On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. + On the other hand, we claim that $\{\ast\} \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $\{\ast\} \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. - property: extremal generating collection proof: The proof is the same as the one for $\Top$; there the test spaces we use are of the form $\kappa \sqcup \{ \kappa \}$ and $\kappa + 1$, which are both Hausdorff spaces. diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index 6572969fa..a722dff8f 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -53,7 +53,7 @@ satisfied_properties: - property: extremal generator proof: >- - The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Man \to \Set$. Since we have an epimorphism $\IR \to 1$, we see that $\IR$ is also a generator. + The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Man \to \Set$. Since we have an epimorphism $\IR \to \{\ast\}$, we see that $\IR$ is also a generator. We claim that in fact, $\IR$ is an extremal generator. To see this, suppose we have a smooth map $f : M \to N$ which induces a bijection of smooth curves on $M$ to smooth curves on $N$. By considering constant curves, we must have that $f$ is a bijection on the underlying sets. Now for any point $p \in M$ and any tangent vector $v \in T_{f(p)}(N)$, there exists a smooth curve $\gamma : \IR \to N$ such that $\gamma(0) = f(p)$ and $\gamma'(0) = v$. By the assumption on $f$, there exists a smooth curve $\beta : \IR \to M$ such that $\gamma = f \circ \beta$. By the injectivity of $f$, we must have $\beta(0) = p$, so $\beta'(0) \in T_p(M)$ and $f_*(\beta'(0)) = \gamma'(0) = v$. This shows that $f_* : T_p(M) \to T_{f(p)}(N)$ is surjective, hence $f$ is a submersion whose fibers are singletons. Therefore, by the submersion theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism. diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index 040e6a84c..da5942305 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -66,11 +66,11 @@ satisfied_properties: - property: extremal cogenerator proof: >- - First, take the two-element set $2$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $2$ are measurable), and use that $2$ is a cogenerator for $\Set$ to show that $2$ with the trivial $\sigma$-algebra is a cogenerator for $\Meas$. + First, take the set $\{0,1\}$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $\{0,1\}$ are measurable), and use that $\{0,1\}$ is a cogenerator for $\Set$ to show that $\{0,1\}$ with the trivial $\sigma$-algebra is a cogenerator for $\Meas$. - Now, we claim that adding the two-element set $2$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating collection. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $2$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $2$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces. + Now, we claim that adding the set $\{0,1\}$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating collection. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $\{0,1\}$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $\{0,1\}$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces. - Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$. + Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $\{0,1\}$ is an extremal cogenerator of $\Meas$. references: - Set_extremal_cogenerator @@ -140,8 +140,8 @@ unsatisfied_properties: - property: infinitary distributive proof: >- - Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. If $1$ denotes the singleton space, we therefore have $X \cong \coprod_{x \in X} 1$ in $\Meas$. However, we claim that the canonical bijective measurable map - $$\textstyle\coprod_{x,y \in X} 1 \to X \times X$$ + Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. Therefore, $X \cong \coprod_{x \in X} \{\ast\}$ in $\Meas$. However, we claim that the canonical bijective measurable map + $$\textstyle\coprod_{x,y \in X} \{\ast\} \to X \times X$$ is not an isomorphism, i.e. that $X \times X$ does not carry the discrete $\sigma$-algebra. More precisely, we will show that the diagonal $\Delta \subseteq X \times X$ is not measurable. (This is well-known and is remarked for example in Wengenroth, end of Ch. 1, but we include the proof nevertheless.) Assume that $\Delta \subseteq X \times X$ is measurable. Then (cf. MSE/61617) there is a countable family of rectangles $(A_n \times B_n)_{n \in \IN}$ such that $\Delta \in \sigma(\{A_n \times B_n : n \in \IN\})$. Consider the product of the characteristic functions @@ -174,7 +174,7 @@ special_morphisms: proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. epimorphisms: description: surjective measurable maps - proof: Use the same proof as for sets, where $2 = \{0,1\}$ is endowed with the trivial $\sigma$-algebra. + proof: Use the same proof as for sets, where $\{0,1\}$ is endowed with the trivial $\sigma$-algebra. regular monomorphisms: description: embeddings proof: '(This is the same proof as for $\Top$.) Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the trivial $\sigma$-algebra.' diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index b9b5ae06a..b9a94d682 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -68,7 +68,7 @@ satisfied_properties: proof: >- Let $G$ be the metric space with underlying set $\IR_{\ge 0}$ equipped with the metric where $d(x,y) = 0$ if $x=y$, and otherwise $d(x,y) = x+y$. We claim that $G$ is an extremal generator. - First, to see that $G$ is a generator, note that the one-point metric space $1$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, $G$ is also a generator. + First, to see that $G$ is a generator, note that the one-point metric space $\{\ast\}$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow \{\ast\}$, $G$ is also a generator. Now, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, $$\begin{align*} @@ -144,7 +144,7 @@ unsatisfied_properties: label: Met_no_filtered_colimit_stable_monos - property: natural numbers object - proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist; see MSE/1778408. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. Since there is a map $\{\ast\} \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist; see MSE/1778408. - property: effective congruences proof: 'Any kernel pair of $h : X \to Z$ in $\Met$ corresponds to a closed subset of $X\times X$. However, there are plenty of non-closed congruences, such as $\Delta \cup (\IQ \times \IQ) \subseteq \IR \times \IR$ with the subspace metric.' @@ -166,14 +166,14 @@ unsatisfied_properties: - property: regular subobject classifier proof: >- - Assume that $\top : 1 \to \Omega$ is a regular subobject classifier. We can identify $\top$ with a point $\top \in \Omega$, and for every regular monomorphism $Y \hookrightarrow X$ there is a unique non-expansive map $f : X \to \Omega$ such that $f^*(\{\top\}) = Y$ as metric spaces, and hence as topological spaces. + Assume that $\top : \{\ast\} \to \Omega$ is a regular subobject classifier. We can identify $\top$ with a point $\top \in \Omega$, and for every regular monomorphism $Y \hookrightarrow X$ there is a unique non-expansive map $f : X \to \Omega$ such that $f^*(\{\top\}) = Y$ as metric spaces, and hence as topological spaces. - The underlying set of $\Omega$ is identified with $\Hom(1,\Omega) \cong \Sub_{\reg}(1)$. There are two regular subobjects of $1 = \{\ast\}$, namely $\{\ast\} \subseteq \{\ast\}$ and $\varnothing \subseteq \{\ast\}$ (the latter being the equalizer of, say, two maps $\{\ast\} \rightrightarrows \{0,1\}$). Thus, $\Omega$ has exactly two points and is therefore discrete. In particular, $\top : 1 \to \Omega$ is a clopen inclusion. The universal property then implies that every regular monomorphism is a clopen inclusion. But this is not the case: for example, the inclusion $[0,\infty) \hookrightarrow \IR$ is the equalizer of $\id : \IR \to \IR$ and the absolute value function $|{-}| : \IR \to \IR$, where $\IR$ is equipped with the standard metric. + The underlying set of $\Omega$ is identified with $\Hom(\{\ast\},\Omega) \cong \Sub_{\reg}(\{\ast\})$. There are two regular subobjects of $\{\ast\}$, namely $\{\ast\} \subseteq \{\ast\}$ and $\varnothing \subseteq \{\ast\}$ (the latter being the equalizer of, say, two maps $\{\ast\} \rightrightarrows \{0,1\}$). Thus, $\Omega$ has exactly two points and is therefore discrete. In particular, $\top : \{\ast\} \to \Omega$ is a clopen inclusion. The universal property then implies that every regular monomorphism is a clopen inclusion. But this is not the case: for example, the inclusion $[0,\infty) \hookrightarrow \IR$ is the equalizer of $\id : \IR \to \IR$ and the absolute value function $|{-}| : \IR \to \IR$, where $\IR$ is equipped with the standard metric. label: Met_no_regular_subobject_classifier - property: coaccessible proof: >- - Assume that $\Met$ is $\kappa$-coaccessible for a regular cardinal $\kappa$. In particular, every metric space is a limit of $\kappa$-copresentable metric spaces. We claim that every $\kappa$-copresentable metric space has at most one point. Since the forgetful functor $\Met \to \Set$ is representable (by $1$), it preserves limits, so that every limit of such metric spaces also has at most one point. This is a contradiction, since there are metric spaces with two points. + Assume that $\Met$ is $\kappa$-coaccessible for a regular cardinal $\kappa$. In particular, every metric space is a limit of $\kappa$-copresentable metric spaces. We claim that every $\kappa$-copresentable metric space has at most one point. Since the forgetful functor $\Met \to \Set$ is representable (by $\{\ast\}$), it preserves limits, so that every limit of such metric spaces also has at most one point. This is a contradiction, since there are metric spaces with two points. To prove the claim, let $X$ be a $\kappa$-copresentable metric space and $a,b \in X$. We will show that $a = b$. Choose a real number $\delta > 0$ with $d(a,b) \leq \delta$. Fix a set $I$ with $\card(I) \geq \kappa$, and let $P$ be the set of all subsets $S \subseteq I$ with $\card(S) < \kappa$, ordered by inclusion. Since $\kappa$ is regular, a union of fewer than $\kappa$ elements of $P$ belongs to $P$ again, so that $P$ is $\kappa$-directed. For $S \in P$ let $D(S)$ be the set $\{0,1\}^S$ equipped with the metric $d(x,y) \coloneqq \delta$ for $x \neq y$. For $S \subseteq T$ in $P$, the restriction map $D(T) \to D(S)$ is non-expansive. This defines a $\kappa$-cofiltered diagram $D : P^{\op} \to \Met$. diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 9bf98d2a1..8a1360484 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -58,7 +58,7 @@ satisfied_properties: proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' - property: extremal generator - proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to 1$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.' + proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to \{\ast\}$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.' - property: extremal cogenerator proof: >- @@ -95,7 +95,7 @@ unsatisfied_properties: proof: 'Consider the metric subspace $\{(a,b) \in \IR^2 : a \leq b\}$ of $\IR^2$.' - property: regular subobject classifier - proof: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' + proof: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = \{\ast\}$, we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, it must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' references: - Haus_no_regular_subobject_classifier diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 78b4e8419..445958612 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -68,7 +68,7 @@ satisfied_properties: proof: >- The proof will be similar to the one for $\Met$. Namely, let $G$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$ for $x, y \in \IR_{\ge 0}$, and $d(x, 0') = d(0', x) = x$ for $x \in \IR_{\ge 0}$. We will show $G$ is an extremal generator for $\PMet$. - First, to see $G$ is a generator, note that the one-point metric space is a generator since it represents the forgetful functor $\PMet\to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, $G$ is also a generator. + First, to see $G$ is a generator, note that the one-point metric space is a generator since it represents the forgetful functor $\PMet\to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow \{\ast\}$, $G$ is also a generator. Now, suppose that $f : X \to Y$ is a non-expansive map of pseudo-metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon \ge 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $G$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0') = x_1$. Hence, $$\begin{align*} @@ -114,10 +114,10 @@ unsatisfied_properties: proof: The coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408 (the proof also works for pseudo-metric spaces). For example, the copower $\IR \sqcup \IR$ does not exist. We only get coproducts when allowing $\infty$ as a distance. - property: natural numbers object - proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. Since there is a map $\{\ast\} \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408. - property: effective cocongruences - proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$, which does not exist.' + proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to \{\ast\}$ does not have any cokernel pair, since that would have to be a coproduct $\{\ast\} \sqcup \{\ast\}$, which does not exist.' references: - Top_no_effective_cocongruences diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index bfa9cf633..b5392c348 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -69,7 +69,7 @@ unsatisfied_properties: proof: Assume that there is a regular subobject classifier $\Omega$, so that (by the classification of regular monomorphisms) $\Hom(P,\Omega)$ is isomorphic to the set of subsets of $P$. By taking $P = \{0\}$ we see that $\Omega$ has $2$ elements, so that either $\Omega \cong \{0,1\}$ (discrete) or $\Omega \cong \{0 < 1\}$. By taking $P = \{0 < 1\}$ we see that $\Omega$ has four pairs $(x,y)$ with $x \leq y$. But $\{0,1\}$ has only two and $\{0 < 1\}$ has only three such pairs. - property: cofiltered-limit-stable epimorphisms - proof: Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique maps $X_n \to 1$ are surjective, but their limit $\varnothing \to 1$ is not surjective. + proof: Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique maps $X_n \to \{\ast\}$ are surjective, but their limit $\varnothing \to \{\ast\}$ is not surjective. - property: effective cocongruences proof: >- diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index af746df49..aeaced1e7 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -45,7 +45,7 @@ satisfied_properties: proof: The set $\{0,1\}$ with the chaotic preorder $(0 \leq 1$, $1 \leq 0)$ is a regular subobject classifier since order-preserving maps $P \to \{0,1\}$ correspond to subsets of $P$. - property: extremal generator - proof: 'We claim that $\{ 0 < 1 \}$ is an extremal generator. First, the singleton preordered set $1$ is a generator, since it represents the forgetful functor $\PreOrd \to \Set$ which is faithful. Since we have an epimorphism $\{ 0 < 1 \} \to 1$, it follows that $\{ 0 < 1 \}$ is also a generator. Now, suppose we have a morphism $f : P \to Q$ such that $f \circ {-} : \Hom(\{0<1\}, P) \to \Hom(\{0<1\}, Q)$ is a bijection. Then considering constant functions, we can see that $f$ must be a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then that induces a morphism $\{0<1\} \to Q$ with $0 \mapsto f(p_1), 1 \mapsto f(p_2)$. The corresponding morphism $\{0<1\}\to P$ must send $0\mapsto p_1, 1 \mapsto p_2$, showing that $p_1 \le p_2$. It follows that $f$ is an isomorphism.' + proof: 'We claim that $\{ 0 < 1 \}$ is an extremal generator. First, the singleton preordered set $\{\ast\}$ is a generator, since it represents the forgetful functor $\PreOrd \to \Set$ which is faithful. Since we have an epimorphism $\{ 0 < 1 \} \to \{\ast\}$, it follows that $\{ 0 < 1 \}$ is also a generator. Now, suppose we have a morphism $f : P \to Q$ such that $f \circ {-} : \Hom(\{0<1\}, P) \to \Hom(\{0<1\}, Q)$ is a bijection. Then considering constant functions, we can see that $f$ must be a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then that induces a morphism $\{0<1\} \to Q$ with $0 \mapsto f(p_1), 1 \mapsto f(p_2)$. The corresponding morphism $\{0<1\}\to P$ must send $0\mapsto p_1, 1 \mapsto p_2$, showing that $p_1 \le p_2$. It follows that $f$ is an isomorphism.' label: PreOrd_extremal_generator - property: extremal cogenerator @@ -67,7 +67,7 @@ unsatisfied_properties: proof: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the functor $\Set \to \PreOrd$ that equips a set with the chaotic preorder. - property: effective cocongruences - proof: 'Consider the preordered set $C \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows C$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element preordered set with the trivial preorder.' + proof: 'Consider the preordered set $C \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $\{\ast\} \rightrightarrows C$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to \{\ast\}$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element preordered set with the trivial preorder.' special_objects: initial object: diff --git a/database/data/categories/Quiv_fc.yaml b/database/data/categories/Quiv_fc.yaml index 97ee12a17..2d5463893 100644 --- a/database/data/categories/Quiv_fc.yaml +++ b/database/data/categories/Quiv_fc.yaml @@ -30,8 +30,8 @@ satisfied_properties: - property: subobject classifier proof: >- - The previous proofs show that $\Quiv_{\fc} \subseteq \Quiv$ is closed under finite limits. The subobject classifier $\Omega$ of $\Quiv$ is finite; see nLab for a detailed description. Hence, $\top : 1 \to \Omega$ is a morphism in $\Quiv_{\fc}$. If $X \hookrightarrow Y$ is a monomorphism in $\Quiv_{\fc}$, it is also a monomorphism in $\Quiv$ since the inclusion functor preserves pullbacks. Hence, there is a unique morphism of quivers $Y \to \Omega$ such that - $$\begin{CD} X @>>> Y \\ @V{!}VV @VVV \\ 1 @>>> \Omega \end{CD}$$ + The previous proofs show that $\Quiv_{\fc} \subseteq \Quiv$ is closed under finite limits. The subobject classifier $\Omega$ of $\Quiv$ is finite; see nLab for a detailed description. Hence, $\top : T \to \Omega$ is a morphism in $\Quiv_{\fc}$, where $T$ denotes the terminal quiver (having one vertex and one loop). If $X \hookrightarrow Y$ is a monomorphism in $\Quiv_{\fc}$, it is also a monomorphism in $\Quiv$ since the inclusion functor preserves pullbacks. Hence, there is a unique morphism of quivers $Y \to \Omega$ such that + $$\begin{CD} X @>>> Y \\ @V{!}VV @VVV \\ T @>>> \Omega \end{CD}$$ is a pullback square in $\Quiv$, i.e. a pullback square in $\Quiv_{\fc}$. - property: infinitary extensive diff --git a/database/data/categories/SeqSet.yaml b/database/data/categories/SeqSet.yaml index b1d55c168..7b48195ef 100644 --- a/database/data/categories/SeqSet.yaml +++ b/database/data/categories/SeqSet.yaml @@ -36,13 +36,13 @@ unsatisfied_properties: - property: generator proof: >- - Suppose the category of sequences had a generator. Then, by this result, every subterminal object would be either initial or terminal. However, $0 \to 1 \to 1 \to \cdots$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0 \to 0 \to \cdots$ nor the terminal object $1 \to 1 \to 1 \to \cdots$. + Suppose the category of sequences had a generator. Then, by this result, every subterminal object would be either initial or terminal. However, $\varnothing \to \{\ast\} \to \{\ast\} \to \cdots$ is a subterminal object which is isomorphic to neither the initial object $\varnothing \to \varnothing \to \varnothing \to \cdots$ nor the terminal object $\{\ast\} \to \{\ast\} \to \{\ast\} \to \cdots$. special_objects: initial object: - description: the constant sequence $0 \to 0 \to \cdots$ + description: the constant sequence $\varnothing \to \varnothing \to \cdots$ terminal object: - description: the constant sequence $1 \to 1 \to \cdots$ + description: the constant sequence $\{\ast\} \to \{\ast\} \to \cdots$ coproducts: description: component-wise defined disjoint union products: diff --git a/database/data/categories/SeqSet_conn.yaml b/database/data/categories/SeqSet_conn.yaml index b49849968..99b781742 100644 --- a/database/data/categories/SeqSet_conn.yaml +++ b/database/data/categories/SeqSet_conn.yaml @@ -62,7 +62,7 @@ satisfied_properties: proof: >- Define the map ("truncated subtraction") $s : \IN \to \IN$ by $s(k) = \max(0,k-1)$. We claim that the sequence $$\Omega = \bigl(\IN \xrightarrow{s} \IN \xrightarrow{s} \IN \xrightarrow{s} \cdots\bigr)$$ - is a subobject classifier, where $\top : 1 \to \Omega$ is given by the elements $0 \in \IN$ in every degree. Clearly, $\Omega$ is connected. Consider a monomorphism $U \to X$. By the classification of monomorphisms below, we may assume that $U \subseteq X$ is a subsequence, i.e. $U_n \subseteq X_n$ for each $n$, and the transition maps $X_n \to X_{n+1}$ restrict to the transition maps $U_n \to U_{n+1}$. + is a subobject classifier, where $\top : T \to \Omega$ is defined on the terminal object $T$, the constant sequence with value $\{\ast\}$, by the elements $0 \in \IN$ in every degree. Clearly, $\Omega$ is connected. Consider a monomorphism $U \to X$. By the classification of monomorphisms below, we may assume that $U \subseteq X$ is a subsequence, i.e. $U_n \subseteq X_n$ for each $n$, and the transition maps $X_n \to X_{n+1}$ restrict to the transition maps $U_n \to U_{n+1}$. For $x_n \in X_n$, we claim that there is some $k \geq 0$ such that its image $x_{n+k} \in X_{n+k}$ belongs to $U_{n+k}$. In fact, there is some $r \geq 0$ such that an element $u_{n+r} \in U_{n+r}$ exists, and connectedness of $X$ yields some $k \geq r$ such that the image of $u_{n+r}$ in $X_{n+k}$ is equal to $x_{n+k}$. This image belongs to $U_{n+k}$. Therefore, the map $$\chi_n : X_n \to \IN, \quad x_n \mapsto \min \{k \geq 0 : x_{n+k} \in U_{n+k}\}$$ @@ -74,7 +74,7 @@ satisfied_properties: \end{CD}$$ commutes. In other words, if $k$ is the smallest number such that $x_{n+k} \in U_{n+k}$, then $s(k)$ is the smallest number $k'$ such that $x_{n+1+k'} \in U_{n+1+k'}$. If $k=0$, then $x_n \in U_n$, hence $x_{n+1} \in U_{n+1}$, so that $k'=0=s(k)$. Now assume $k > 0$, so that $s(k)=k-1$. Then $k'=k-1$, since $x_{n+1+(k-1)} \in U_{n+1+(k-1)}$ and, if $\ell < k-1$, then $\ell+1 < k$, so $x_{n+1+\ell} = x_{n+(\ell+1)} \notin U_{n+(\ell+1)}$ by the definition of $k$. - Thus, $\chi = (\chi_n) : X \to \Omega$ is a well-defined morphism of sequences. Since $\chi_n^*(\{0\}) = U_n$ for each $n$, the canonical morphism $U \to X \times_{\Omega} 1$ is an isomorphism. It remains to show that $\chi$ is unique with this property. + Thus, $\chi = (\chi_n) : X \to \Omega$ is a well-defined morphism of sequences. Since $\chi_n^*(\{0\}) = U_n$ for each $n$, the canonical morphism $U \to X \times_{\Omega} T$ is an isomorphism. It remains to show that $\chi$ is unique with this property. Let $\alpha : X \to \Omega$ be another morphism of sequences with $\alpha_n^*(\{0\}) = U_n$ for every $n$, and in particular $(\alpha_n)|_{U_n} = 0$. If $x_n \in X_n$ is any element, choose $k \geq 0$ minimal such that $x_{n+k} \in U_{n+k}$, where $x_{n+k}$ denotes the image of $x_n$ as before. We claim that $$\alpha_n(x_n) = k.$$ @@ -156,7 +156,7 @@ unsatisfied_properties: - property: binary copowers proof: >- - We show that the coproduct $1+1$ does not exist in $[(\IN,\leq),\Set]_{\conn}$, where $1$ denotes the terminal object, the constant sequence with value $\{\ast\}$. Since a morphism $1 \to X$ corresponds to an element of $X_0$, this would amount to a universal connected sequence of sets $X$ equipped with two elements $x,x' \in X_0$. Choose $k \geq 0$ such that their images in $X_k$ coincide. Then, by the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ must coincide. A counterexample is the sequence $Y$ defined by + We show that the coproduct $T+T$ does not exist in $[(\IN,\leq),\Set]_{\conn}$, where $T$ denotes the terminal object, the constant sequence with value $\{\ast\}$. Since a morphism $T \to X$ corresponds to an element of $X_0$, this would amount to a universal connected sequence of sets $X$ equipped with two elements $x,x' \in X_0$. Choose $k \geq 0$ such that their images in $X_k$ coincide. Then, by the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ must coincide. A counterexample is the sequence $Y$ defined by $$\{0,1\} \xrightarrow{\id} \cdots \xrightarrow{\id} \{0,1\} \xrightarrow{!} \{0\} \xrightarrow{!} \{0\} \xrightarrow{!} \cdots,$$ where $Y_k = \{0,1\}$ and $Y_{k+1}=\{0\}$. It is connected, but the elements $0,1 \in Y_0$ only become equal in $Y_{k+1}$. Another counterexample is the subobject classifier $\Omega$, whose elements $0,k+1 \in \Omega_0$ become equal only after $k+1$ steps. @@ -187,7 +187,7 @@ unsatisfied_properties: - property: natural numbers object proof: >- - Assume that a natural numbers object $(N,z,s)$ exists in $[(\IN,\leq),\Set]_{\conn}$. The morphism $z : 1 \to N$ corresponds to an element $z \in N_0$. The functor + Assume that a natural numbers object $(N,z,s)$ exists in $[(\IN,\leq),\Set]_{\conn}$. The morphism $z : T \to N$, where $T$ denotes the terminal object, the constant sequence with value $\{\ast\}$, corresponds to an element $z \in N_0$. The functor $$[(\IN,\leq),\Set]_{\conn} \to \Set, \quad X \mapsto X_0$$ has a right adjoint mapping a set $S$ to the connected sequence $$S \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$ @@ -195,7 +195,7 @@ unsatisfied_properties: For every $k \geq 0$ consider the connected sequence $X$ defined by $$N_0 \xrightarrow{\id} \cdots \xrightarrow{\id} N_0 \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$ - where the singleton sets start at index $k+1$. The element $z \in N_0 = X_0$ induces a morphism $z : 1 \to X$. We define the endomorphism $r : X \to X$ by using the map $s_0 : N_0 \to N_0$ at indices $0,\dotsc,k$ and the unique maps at indices $> k$. Since $(N,z,s)$ is a natural numbers object, there is a unique morphism of sequences $f : N \to X$ such that $f_0(z)=z$ and $r \circ f = f \circ s$. Evaluating this equation at index $0$ yields $s_0 \circ f_0 = f_0 \circ s_0$, so that $f_0 = \id_{N_0}$. Furthermore, naturality of $f : N \to X$ for $0 \to k$ shows that the diagram + where the singleton sets start at index $k+1$. The element $z \in N_0 = X_0$ induces a morphism $z : T \to X$. We define the endomorphism $r : X \to X$ by using the map $s_0 : N_0 \to N_0$ at indices $0,\dotsc,k$ and the unique maps at indices $> k$. Since $(N,z,s)$ is a natural numbers object, there is a unique morphism of sequences $f : N \to X$ such that $f_0(z)=z$ and $r \circ f = f \circ s$. Evaluating this equation at index $0$ yields $s_0 \circ f_0 = f_0 \circ s_0$, so that $f_0 = \id_{N_0}$. Furthermore, naturality of $f : N \to X$ for $0 \to k$ shows that the diagram $$\begin{CD} N_0 @>{N_{0 \to k}}>> N_k \\ @V{\id}VV @VV{f_k}V \\ diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 2cc18bd9f..77db3cea7 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -70,7 +70,7 @@ special_morphisms: proof: This is an elementary fact from set theory. monomorphisms: description: injective maps - proof: 'For the non-trivial direction, if $f : X \to Y$ is a monomorphism of sets and $a,b \in X$ satisfy $f(a) = f(b)$, then $f \circ a = f \circ b$ when we regard $a,b$ as morphisms $a,b : 1 \rightrightarrows X$. Hence, $a = b$. More generally, if $\C$ is a category that admits a faithful and representable functor $U : \C \to \Set$, then the monomorphisms in $\C$ are precisely the morphisms whose $U$-image is injective.' + proof: 'For the non-trivial direction, if $f : X \to Y$ is a monomorphism of sets and $a,b \in X$ satisfy $f(a) = f(b)$, then $f \circ a = f \circ b$ when we regard $a,b$ as morphisms $a,b : \{\ast\} \rightrightarrows X$. Hence, $a = b$. More generally, if $\C$ is a category that admits a faithful and representable functor $U : \C \to \Set$, then the monomorphisms in $\C$ are precisely the morphisms whose $U$-image is injective.' epimorphisms: description: surjective maps - proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' + proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of sets, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' diff --git a/database/data/categories/Set_arrow.yaml b/database/data/categories/Set_arrow.yaml index 08e10862f..fdf0d94cc 100644 --- a/database/data/categories/Set_arrow.yaml +++ b/database/data/categories/Set_arrow.yaml @@ -46,13 +46,13 @@ unsatisfied_properties: - property: generator proof: >- - Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $0 \to 1$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0$ nor the terminal object $1 \to 1$. + Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $\varnothing \to \{\ast\}$ is a subterminal object which is isomorphic to neither the initial object $\varnothing \to \varnothing$ nor the terminal object $\{\ast\} \to \{\ast\}$. special_objects: initial object: - description: the unique function $0 \to 0$ + description: the unique function $\varnothing \to \varnothing$ terminal object: - description: the unique function $1 \to 1$ + description: the unique function $\{\ast\} \to \{\ast\}$ coproducts: description: component-wise defined disjoint union, equipped with the disjoint union of the functions products: @@ -64,7 +64,7 @@ special_morphisms: proof: This is easy. monomorphisms: description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective - proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$. + proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $\{\ast\} \to \{\ast\}$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $\varnothing \to \{\ast\}$. epimorphisms: description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective proof: For the non-trivial direction, use the fact that the category is epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise. diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index f6f891358..1271489ac 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -51,7 +51,7 @@ satisfied_properties: proof: This follows from Lemma 11 here since $\Set$ is countably extensive (even infinitary extensive) and its full subcategory $\Set_\c$ is closed under pullbacks and countable coproducts in $\Set$. - property: effective congruences - proof: 'Let $R \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set$. Also, the quotient $(X/R)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set_\c$ as well.' + proof: 'Let $R \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $\{\ast\}$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set$. Also, the quotient $(X/R)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set_\c$ as well.' - property: regular proof: This follows from Lemma 7 here applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the regular category $\Set$ and the description of regular epimorphisms below. @@ -70,7 +70,7 @@ unsatisfied_properties: proof: Since the forgetful functor $\Set_\c \to \Set$ is representable, it preserves (countable) products. Therefore, if the power $\{0,1\}^{\IN}$ exists in $\Set_\c$, it must be the ordinary cartesian product, which however is uncountable. - property: ℵ₂-small copowers - proof: 'Assume that the copower $X \coloneqq I \otimes 1$ exists in $\Set_\c$. We will prove that $I$ is countable; in particular, $\aleph_1 \otimes 1$ does not exist. The copower is a countable set $X$ with a universal family of elements $(x_i)_{i \in I}$. For every $i \in I$ there is a map $X \to \{0,1\}$ defined by $x_i \mapsto 1$ and $x_j \mapsto 0$ for $j \neq i$. In particular, $x_i \neq x_j$ whenever $i \neq j$. Thus, $x : I \to X$ is an injective map, which proves that $I$ is countable.' + proof: 'Assume that the copower $X \coloneqq I \otimes \{\ast\}$ exists in $\Set_\c$. We will prove that $I$ is countable; in particular, $\aleph_1 \otimes \{\ast\}$ does not exist. The copower is a countable set $X$ with a universal family of elements $(x_i)_{i \in I}$. For every $i \in I$ there is a map $X \to \{0,1\}$ defined by $x_i \mapsto 1$ and $x_j \mapsto 0$ for $j \neq i$. In particular, $x_i \neq x_j$ whenever $i \neq j$. Thus, $x : I \to X$ is an injective map, which proves that $I$ is countable.' - property: ℵ₁-cofiltered limits proof: >- @@ -101,4 +101,4 @@ special_morphisms: proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. epimorphisms: description: surjective maps - proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of countable sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' + proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of countable sets, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' diff --git a/database/data/categories/Set_family.yaml b/database/data/categories/Set_family.yaml index f469d63af..233a4c959 100644 --- a/database/data/categories/Set_family.yaml +++ b/database/data/categories/Set_family.yaml @@ -50,7 +50,7 @@ unsatisfied_properties: proof: 'Assume that there is a generating collection $S$, which is in particular essentially small by convention. For $i \in I$, consider the family $X^i$ defined by $(X^i)_i = \{0,1\}$ and $(X^i)_j = \varnothing$ for $j \neq i$. There are (at least) two morphisms $X^i \rightrightarrows X^i$. Thus, there is some $G^i \in S$ and a morphism $G^i \to X^i$ that distinguishes the two morphisms. This is only possible when $(G^i)_i$ is non-empty, while $(G^i)_j$ is empty for all $j \neq i$. Thus, if we define the support of a family by $\supp(X) \coloneqq \{i \in I : X_i \neq \varnothing\}$, then $\supp(G^i) = \{i\}$. Therefore, using the axiom of choice, we get an injective map $I \to S$, $i \mapsto G^i$. Since $S$ is essentially small, it follows that $I$ is essentially small, which contradicts our assumption on $I$.' - property: well-powered - proof: The collection $\Sub(1)$ is isomorphic to the collection $P(I)$ of subcollections of $I$. In fact, if $J \subseteq I$ is a subcollection, we define $X \subseteq 1$ by $X_i = \varnothing$ for $i \in J$ and $X_i = 1$ for $i \notin J$. Every subobject of $1$ has this form. Since $P(I)$ is not essentially small (there is an injective map $I \hookrightarrow P(I)$), we conclude that $\Sub(1)$ is not essentially small. + proof: Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. The collection $\Sub(T)$ is isomorphic to the collection $P(I)$ of subcollections of $I$. In fact, if $J \subseteq I$ is a subcollection, we define $X \subseteq T$ by $X_i = \varnothing$ for $i \in J$ and $X_i = \{\ast\}$ for $i \notin J$. Every subobject of $T$ has this form. Since $P(I)$ is not essentially small (there is an injective map $I \hookrightarrow P(I)$), we conclude that $\Sub(T)$ is not essentially small. special_objects: initial object: diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml index 29d78fd86..96e09e1d5 100644 --- a/database/data/categories/Set_family_mostly_0.yaml +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -26,11 +26,11 @@ satisfied_properties: proof: The functor $\Set^{(I)}_0 \to \Set^+$, $X \mapsto \coprod_{i \in I} X_i$ is faithful. Since $\coprod_{i \in I} X_i \cong \coprod_{i \in \supp(X)} X_i$ is essentially small, it yields a faithful functor $\Set^{(I)}_0 \to \Set$. - property: cocomplete - proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is cocomplete with pointwise colimits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_0$ is closed under colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $C_i \cong \colim_{j \in \J} 0 \cong 0$. Thus, $\supp(C) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(C)$ is essentially small.' + proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is cocomplete with pointwise colimits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_0$ is closed under colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, $C_i$ is a colimit of empty sets and hence empty. Thus, $\supp(C) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(C)$ is essentially small.' check_redundancy: false - property: connected limits - proof: 'In fact, all non-empty limits exist. Since $\Set$ is complete, the product category $\Set^I$ is also complete with pointwise limits. It suffices to prove that $\Set^{(I)}_0$ is closed under non-empty limits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small non-empty diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $L_i \cong \lim_{j \in \J} 0 \cong 0$, where the last step uses the fact that $\J$ is non-empty. Thus, $\supp(L) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(L)$ is essentially small.' + proof: 'In fact, all non-empty limits exist. Since $\Set$ is complete, the product category $\Set^I$ is also complete with pointwise limits. It suffices to prove that $\Set^{(I)}_0$ is closed under non-empty limits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small non-empty diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, $L_i$ is a limit of empty sets indexed by the non-empty category $\J$ and hence empty. Thus, $\supp(L) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(L)$ is essentially small.' label: Set_family_mostly_0_non_empty_limits check_redundancy: false @@ -90,7 +90,7 @@ unsatisfied_properties: proof: Assume that a terminal object $X$ exists. For $i \in I$, define the family $Y$ by $Y_i = \{\ast\}$ and $Y_j = \varnothing$ for $j \neq i$. Then $\supp(Y) = \{i\}$, so $Y$ belongs to $\Set^{(I)}_0$. By assumption, there is a morphism $Y \to X$. In particular, we see that $X_i$ is non-empty. But then $\supp(X) = I$, which is not essentially small. - property: cofiltered-limit-stable epimorphisms - proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_0$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 0$ for indices $j \neq i$. This embedding is faithful and preserves non-empty limits and epimorphisms. Thus, by the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_0$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = \varnothing$ for indices $j \neq i$. This embedding is faithful and preserves non-empty limits and epimorphisms. Thus, by the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. - property: cogenerating collection proof: Assume that $S$ is a cogenerating collection. In particular, $S$ is essentially small (by definition). Since $\bigcup_{Q \in S} \supp(Q)$ is essentially small, but $I$ is not essentially small, there is some index $i \in I$ with $Q_i = \varnothing$ for all $Q \in S$. Consider the family $X \in \Set^{(I)}_0$ defined by $X_i = \{1,2\}$ and $X_j = \varnothing$ for all $j \neq i$. There are (at least) two morphisms $X \rightrightarrows X$. Thus, there is some $Q \in S$ and some morphism $X \to Q$ that distinguishes them. The component at $i$ is a map $X_i \to Q_i$, which cannot exist since $X_i$ is non-empty and $Q_i$ is empty. diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index cce361162..9380537f6 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -1,7 +1,7 @@ id: Set_family_mostly_1 name: category of large families of sets which are mostly singletons notation: $\Set^{(I)}_1$ -objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : X_i \not\cong 1\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' +objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : \card(X_i) \neq 1\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' morphisms: families of maps description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$. Most properties are immediately inherited from $\Set$, but there is no initial object. There are also many differences between this category and its variant $\Set^{(I)}_0$. nlab_link: null @@ -22,7 +22,7 @@ satisfied_properties: proof: For two families $X$ and $Y$, the collection $\Hom(X,Y) = \prod_{i \in I} \Hom(X_i,Y_i)$ is isomorphic to $\prod_{i \in S(Y)} \Hom(X_i,Y_i)$, which is essentially small since $S(Y)$ and each $\Hom(X_i,Y_i)$ are essentially small. - property: complete - proof: 'Since $\Set$ is complete, the product category $\Set^I$ is complete with pointwise limits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_1$ is closed under limits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $L_i \cong \lim_{j \in \J} 1 \cong 1$. Thus, $S(L) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(L)$ is essentially small.' + proof: 'Since $\Set$ is complete, the product category $\Set^I$ is complete with pointwise limits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_1$ is closed under limits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, $L_i$ is a limit of singletons and hence a singleton. Thus, $S(L) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(L)$ is essentially small.' - property: locally cartesian closed proof: >- @@ -30,12 +30,12 @@ satisfied_properties: $$\textstyle [Y \to X, Z \to X] = \coprod_{x \in X} \Hom(Y_x,Z_x),$$ where $Y_x$ denotes the fiber of $Y \to X$ over $x \in X$. It follows formally that, for every collection $I$, also $\Set^I$ is locally cartesian closed, with exponentials $$\textstyle [Y \to X, Z \to X]_i = \coprod_{x \in X_i} \Hom((Y_i)_x,(Z_i)_x).$$ - Thus, if $X_i \cong 1$ and $Z_i \cong 1$, then $[Y \to X, Z \to X]_i \cong 1$. In other words, + Thus, if $X_i$ and $Z_i$ are singletons, then $[Y \to X, Z \to X]_i$ is a singleton. In other words, $$S([Y \to X, Z \to X]) \subseteq S(X) \cup S(Z).$$ In particular, if $S(X)$ and $S(Z)$ are essentially small, then $S([Y \to X, Z \to X])$ is also essentially small. Thus, if $X \in \Set^{(I)}_1$, then the full subcategory $\Set^{(I)}_1 / X$ of $\Set^I / X$ is closed under exponentials and is therefore also cartesian closed. - property: connected colimits - proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is also cocomplete with pointwise colimits. It suffices to prove that $\Set^{(I)}_1$ is closed under connected colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small connected diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $C_i \cong \colim_{j \in \J} 1 \cong 1$, where the last step uses the fact that $\J$ is connected. Thus, $S(C) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(C)$ is essentially small.' + proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is also cocomplete with pointwise colimits. It suffices to prove that $\Set^{(I)}_1$ is closed under connected colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small connected diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, $C_i$ is a colimit of singletons indexed by the connected category $\J$ and hence a singleton. Thus, $S(C) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(C)$ is essentially small.' - property: exact filtered colimits proof: We already know that the category has connected, hence filtered, colimits, and that it has finite limits. These (co)limits are defined pointwise. Hence, the claim follows from the corresponding property of $\Set$. @@ -47,7 +47,7 @@ satisfied_properties: proof: Based on the pointwise descriptions of regular monomorphisms and pushouts, this follows from the corresponding property of $\Set$. - property: well-copowered - proof: The epimorphisms $X \to Y$ are precisely the morphisms that are pointwise surjective (see below). If $X_i \to Y_i$ is surjective and $X_i \cong 1$, then also $Y_i \cong 1$. It follows that the collection $\Quot(X) \cong \prod_{i \in S(X)} \Quot(X_i)$ is essentially small. + proof: The epimorphisms $X \to Y$ are precisely the morphisms that are pointwise surjective (see below). If $X_i \to Y_i$ is surjective and $X_i$ is a singleton, then $Y_i$ is a singleton as well. It follows that the collection $\Quot(X) \cong \prod_{i \in S(X)} \Quot(X_i)$ is essentially small. - property: effective congruences proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_1$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in $\Set$, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all limits) and coequalizers (in fact, all connected colimits) are constructed pointwise. @@ -69,42 +69,42 @@ unsatisfied_properties: - property: binary copowers proof: >- - We first observe that each evaluation functor $\ev_i : \Set^{(I)}_1 \to \Set$ is cocontinuous. This is because it has a right adjoint, which maps a set $T$ to the family $\widetilde{T}$ defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. - It follows that the inclusion functor $\Set^{(I)}_1 \hookrightarrow \Set^I$ is cocontinuous. In particular, a coproduct $X+Y$ exists in $\Set^{(I)}_1$ if and only if the pointwise coproduct $X+Y$ belongs to $\Set^{(I)}_1$. But this almost never happens. For example, if $X=Y=1$, then $S(1+1) = I$, which is not essentially small. Thus, the coproduct $1+1$ does not exist. + We first observe that each evaluation functor $\ev_i : \Set^{(I)}_1 \to \Set$ is cocontinuous. This is because it has a right adjoint, which maps a set $T$ to the family $\widetilde{T}$ defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = \{\ast\}$ for indices $j \neq i$. + It follows that the inclusion functor $\Set^{(I)}_1 \hookrightarrow \Set^I$ is cocontinuous. In particular, a coproduct $X+Y$ exists in $\Set^{(I)}_1$ if and only if the pointwise coproduct $X+Y$ belongs to $\Set^{(I)}_1$. But this almost never happens. For example, let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. Then $S(T+T) = I$, which is not essentially small. Thus, the coproduct $T+T$ does not exist. label: Set_family_mostly_1_colimits - property: natural numbers object - proof: 'Assume that $(N,z,s)$ is a natural numbers object. Since $z : 1 \to N$ is a morphism consisting of maps $z_i : 1 \to N_i$, we have $N_i \neq \varnothing$ for every $i \in I$. By Lemma 2 here, the coproduct $1 + N$ exists, and we have $N \cong 1 + N$. We have seen above that coproducts, if they exist, must be computed pointwise. Thus, for every $i \in I$, the set $N_i \cong 1 + N_i$ has at least $2$ elements. Hence, $S(N) = I$, which is not essentially small.' + proof: 'Assume that $(N,z,s)$ is a natural numbers object. Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. Since $z : T \to N$ is a morphism consisting of maps $z_i : \{\ast\} \to N_i$, we have $N_i \neq \varnothing$ for every $i \in I$. By Lemma 2 here, the coproduct $T + N$ exists, and we have $N \cong T + N$. We have seen above that coproducts, if they exist, must be computed pointwise. Thus, for every $i \in I$, the set $N_i \cong \{\ast\} + N_i$ has at least $2$ elements. Hence, $S(N) = I$, which is not essentially small.' references: - Set_family_mostly_1_colimits - property: cofiltered-limit-stable epimorphisms - proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. This embedding is faithful and preserves limits and epimorphisms. Thus, by the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = \{\ast\}$ for indices $j \neq i$. This embedding is faithful and preserves limits and epimorphisms. Thus, by the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. - property: Malcev proof: Again, we use the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, which extends a set by singletons. Take any set $X$ with a non-symmetric reflexive relation $R \hookrightarrow X \times X$. Then $\widetilde{R} \hookrightarrow \widetilde{X} \times \widetilde{X}$ is a non-symmetric reflexive relation. - property: disjoint finite products - proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. This embedding preserves products (in fact, it is right adjoint to $\ev_i$, as noted above). Take a non-empty set $T$. The projection $T \times \varnothing \to T$ is not surjective. It follows that the projection $\widetilde{T} \times \widetilde{\varnothing} \to \widetilde{T}$ is not an epimorphism, using the description of epimorphisms below. + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = \{\ast\}$ for indices $j \neq i$. This embedding preserves products (in fact, it is right adjoint to $\ev_i$, as noted above). Take a non-empty set $T$. The projection $T \times \varnothing \to T$ is not surjective. It follows that the projection $\widetilde{T} \times \widetilde{\varnothing} \to \widetilde{T}$ is not an epimorphism, using the description of epimorphisms below. references: - Set_family_mostly_1_colimits - property: well-powered - proof: The collection $\Sub(1)$ is isomorphic to the collection of essentially small subcollections of $I$. In fact, if $J \subseteq I$ is an essentially small subcollection, we define $X \subseteq 1$ by $X_i = \varnothing$ for $i \in J$ and $X_i = 1$ for $i \notin J$. Every subobject of $1$ has this form. Since for every $i \in I$ the collection $\{i\} \subseteq I$ is essentially small, we conclude that $\Sub(1)$ is not essentially small. + proof: Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. The collection $\Sub(T)$ is isomorphic to the collection of essentially small subcollections of $I$. In fact, if $J \subseteq I$ is an essentially small subcollection, we define $X \subseteq T$ by $X_i = \varnothing$ for $i \in J$ and $X_i = \{\ast\}$ for $i \notin J$. Every subobject of $T$ has this form. Since for every $i \in I$ the collection $\{i\} \subseteq I$ is essentially small, we conclude that $\Sub(T)$ is not essentially small. - property: concretizable proof: >- - We will show that Isbell's condition for concretizability fails. For every object $X$ there is a unique span $1 \leftarrow X \rightarrow 1$, where $1$ is the terminal object. A cospan $1 \xrightarrow{u} Y \xleftarrow{v} 1$ corresponds to a family of elements $u_i, v_i \in Y_i$ for $i \in I$. The span commutes with the cospan if and only if, for every $i \in I$, the diagram + We will show that Isbell's condition for concretizability fails. Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. For every object $X$ there is a unique span $T \leftarrow X \rightarrow T$. A cospan $T \xrightarrow{u} Y \xleftarrow{v} T$ corresponds to a family of elements $u_i, v_i \in Y_i$ for $i \in I$. The span commutes with the cospan if and only if, for every $i \in I$, the diagram $$\begin{CD} - X_i @>>> 1 \\ + X_i @>>> \{\ast\} \\ @VVV @VV{v_i}V \\ - 1 @>>{u_i}> Y_i + \{\ast\} @>>{u_i}> Y_i \end{CD}$$ commutes. In other words, we must have $$X_i \neq \varnothing \implies u_i = v_i.$$ - In particular, if we define $V(X) \coloneqq \{i \in I : X_i = \varnothing\}$, then $V(X)=V(X')$ implies that the spans for $X$ and $X'$ are equivalent, i.e., they commute with the same cospans. The converse also holds. To prove this, assume that the spans for $X$ and $X'$ are equivalent and that $i \in V(X)$. To show that $i \in V(X')$, consider the family $Y$ defined by $Y_i = \{1,2\}$ and $Y_j = \{\ast\}$ for $j \neq i$. Define $u,v : 1 \rightrightarrows Y$ by $u_i = 1$ and $v_i = 2$, and by taking the unique value for all indices $j \neq i$. Since $X_i = \varnothing$ and $u_j = v_j$ for all $j \neq i$, we see that the span for $X$ commutes with the cospan $(u,v)$. By assumption, the span for $X'$ also commutes with that cospan. Since $u_i \neq v_i$, this implies that $X'_i = \varnothing$. + In particular, if we define $V(X) \coloneqq \{i \in I : X_i = \varnothing\}$, then $V(X)=V(X')$ implies that the spans for $X$ and $X'$ are equivalent, i.e., they commute with the same cospans. The converse also holds. To prove this, assume that the spans for $X$ and $X'$ are equivalent and that $i \in V(X)$. To show that $i \in V(X')$, consider the family $Y$ defined by $Y_i = \{1,2\}$ and $Y_j = \{\ast\}$ for $j \neq i$. Define $u,v : T \rightrightarrows Y$ by $u_i = 1$ and $v_i = 2$, and by taking the unique value for all indices $j \neq i$. Since $X_i = \varnothing$ and $u_j = v_j$ for all $j \neq i$, we see that the span for $X$ commutes with the cospan $(u,v)$. By assumption, the span for $X'$ also commutes with that cospan. Since $u_i \neq v_i$, this implies that $X'_i = \varnothing$. - We have thus fully characterized the equivalence classes of spans $1 \leftarrow X \rightarrow 1$. For every $i \in I$, there is a family $X^i$ with $V(X^i) = \{i\}$, for example, $X^i_i = \varnothing$ and $X^i_j = \{\ast\}$ for $j \neq i$. For $i \neq i'$, the spans for $X^i$ and $X^{i'}$ are not equivalent since $V(X^i) \neq V(X^{i'})$. We conclude that the collection of equivalence classes is not essentially small. + We have thus fully characterized the equivalence classes of spans $T \leftarrow X \rightarrow T$. For every $i \in I$, there is a family $X^i$ with $V(X^i) = \{i\}$, for example, $X^i_i = \varnothing$ and $X^i_j = \{\ast\}$ for $j \neq i$. For $i \neq i'$, the spans for $X^i$ and $X^{i'}$ are not equivalent since $V(X^i) \neq V(X^{i'})$. We conclude that the collection of equivalence classes is not essentially small. special_objects: terminal object: diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index 392390a7d..831fe6c05 100644 --- a/database/data/categories/Set_ff.yaml +++ b/database/data/categories/Set_ff.yaml @@ -89,7 +89,7 @@ unsatisfied_properties: proof: This is trivial. - property: locally finite - proof: If $X$ is an infinite set, there are infinitely many maps $1 \to X$. They are injective and hence finite-to-one. + proof: If $X$ is an infinite set, there are infinitely many maps $\{\ast\} \to X$. They are injective and hence finite-to-one. - property: strongly connected proof: Already $\Set$ is not strongly connected. @@ -98,7 +98,7 @@ unsatisfied_properties: proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\ff$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' - property: countable copowers - proof: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' + proof: 'Assume that the copower $X \coloneqq \IN \otimes \{\ast\}$ exists. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to \{\ast\}$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' - property: filtered proof: 'Consider the maps $f,g : \IN \rightrightarrows \IN$ defined by $f(x)=x$ and $g(x)=2x$. They are injective, hence finite-to-one. If a map $h : \IN \to X$ coequalizes them, we have $h(x)=h(2x)$, in particular $h(1)=h(2^n)$ for all $n \in \IN$. Thus, $h$ is not finite-to-one.' @@ -107,7 +107,7 @@ unsatisfied_properties: proof: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\ff$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. - property: cogenerating collection - proof: 'Suppose that $S$ is an essentially small collection of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$, giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.' + proof: 'Suppose that $S$ is an essentially small collection of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$, giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : \{\ast\} \rightrightarrows \kappa$.' special_objects: initial object: @@ -124,4 +124,4 @@ special_morphisms: proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the singleton), hence preserves monomorphisms. epimorphisms: description: surjective maps with finite fibers - proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' + proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 28ef0f5d8..df1f05a5f 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -78,7 +78,7 @@ unsatisfied_properties: proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ are equalized by no map $X \to \{0\}$ in this category. - property: sequential limits - proof: Assume that the sequence of inclusions $\cdots \to \IN_{\geq 2} \to \IN_{\geq 1} \to \IN_{\geq 0} = \IN$ has a limit $X$, consisting of maps $X \to \IN_{\geq n}$. Since $X$ is non-empty, there is a map $1 \to X$. This corresponds to a family of compatible maps $1 \to \IN_{\geq n}$, i.e. to compatible elements in $\IN_{\geq n}$. But the set $\bigcap_{n \geq 0} \IN_{\geq n}$ is empty. + proof: Assume that the sequence of inclusions $\cdots \to \IN_{\geq 2} \to \IN_{\geq 1} \to \IN_{\geq 0} = \IN$ has a limit $X$, consisting of maps $X \to \IN_{\geq n}$. Since $X$ is non-empty, there is a map $\{\ast\} \to X$. This corresponds to a family of compatible maps $\{\ast\} \to \IN_{\geq n}$, i.e. to compatible elements in $\IN_{\geq n}$. But the set $\bigcap_{n \geq 0} \IN_{\geq n}$ is empty. - property: ℵ₁-cofiltered limits proof: 'Since the forgetful functor $\Setne \to \Set$ is representable, it preserves limits. Thus it suffices to find an $\aleph_1$-cofiltered diagram of non-empty sets whose limit in $\Set$ is empty. Let $R$ be an uncountable set (such as $\IR$) and consider the poset $P$ of subsets $A \subseteq R$ whose complement $R \setminus A$ is countable; in particular, every such $A$ is non-empty. Then $P$ is $\aleph_1$-cofiltered, since a countable union of countable sets is countable. The limit of the diagram $P \to \Setne$, $A \mapsto A$, in $\Set$ is the intersection $\bigcap_{A \in P} A$ in $R$, which is empty, because for every $r \in R$ we have $r \notin R \setminus \{r\} \in P$.' diff --git a/database/data/categories/Sh(X).yaml b/database/data/categories/Sh(X).yaml index 7d243d172..1fada67e3 100644 --- a/database/data/categories/Sh(X).yaml +++ b/database/data/categories/Sh(X).yaml @@ -35,7 +35,7 @@ unsatisfied_properties: - property: generator proof: >- Suppose $\Sh(X)$ had a generator. Then by this result, every subterminal object would be either initial or terminal. On the other hand, the subterminal objects of $\Sh(X)$ are of the form $y_U \coloneqq \Hom({-}, U)$ for $U$ open. (Alternative descriptions of $y_U$ include: - $$y_U(V) = \begin{cases} 1, & V \subseteq U; \\ \varnothing & \text{otherwise} \end{cases}$$ + $$y_U(V) = \begin{cases} \{\ast\}, & V \subseteq U; \\ \varnothing & \text{otherwise} \end{cases}$$ with the unique restriction maps; and $y_U$ represents the functor $\Gamma(U, {-})$ of sections over $U$.) Therefore, the lemma implies that every open set of $X$ is either $\varnothing$ or $X$, contradicting our assumption that $X$ does not have the indiscrete topology. special_objects: diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml index c0d298571..e0d44006d 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -22,7 +22,7 @@ satisfied_properties: proof: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of degree $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since $\FinSet$ is an elementary topos and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18. - property: cogenerator - proof: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' + proof: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $\{\ast\} \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' - property: ℵ₁-accessible proof: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable; see here. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible. @@ -35,7 +35,7 @@ unsatisfied_properties: proof: This is trivial. - property: locally finite - proof: If $1$ denotes the terminal species, there are infinitely many morphisms $1 \to 1 \sqcup 1$ since they correspond to functions $\IN \to \{1,2\}$. + proof: If $T$ denotes the terminal species, there are infinitely many morphisms $T \to T \sqcup T$ since they correspond to functions $\IN \to \{1,2\}$. - property: locally small proof: Since $\FinSet$ is not small, this follows exactly like Lemma 2 here; but this result is not really relevant; all that matters is that $\Sp$ is locally essentially small. @@ -53,13 +53,13 @@ unsatisfied_properties: Alternatively, the claim follows from this result. - 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 combinatorial species $N$ with this property, since evaluating this isomorphism at, say, $\varnothing$, would yield a finite set $N$ with this property. + proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong T \sqcup N$, where $T$ denotes the terminal species. But there is no combinatorial species $N$ with this property, since evaluating this isomorphism at, say, $\varnothing$, would yield a finite set $N$ with this property. special_objects: initial object: description: species $X$ with $X_n = \varnothing$ terminal object: - description: species $X$ with $X_n = 1$ + description: species $X$ with $X_n = \{\ast\}$ coproducts: description: '[finite case] pointwise finite disjoint union' products: diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index c3ffed922..c8678cb62 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -92,7 +92,7 @@ unsatisfied_properties: label: Top_not_co-malcev - property: effective cocongruences - proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' + proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{\ast\} \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z \to \{\ast\}$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' label: Top_no_effective_cocongruences - property: extremal generating collection @@ -121,7 +121,7 @@ special_morphisms: proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. epimorphisms: description: surjective continuous maps - proof: The proof works exactly as for the category of sets, where we endow $2$ with the indiscrete topology. + proof: The proof works exactly as for the category of sets, where we endow $\{0,1\}$ with the indiscrete topology. regular monomorphisms: description: embeddings proof: 'Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the indiscrete topology.' diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index f5cfe1122..424a0a316 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -101,7 +101,7 @@ unsatisfied_properties: - Set_*_not_conormal - property: coaccessible - proof: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Adámek–Rosický, Prop. 4.7. However, since $\Set_*$ is not coaccessible, this is a contradiction.' + proof: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,\ast\}$ be the pointed topological space such that $\{\ast\}$ is the only non-trivial open set, and let $S_1=\{x,\ast\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,\ast\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Adámek–Rosický, Prop. 4.7. However, since $\Set_*$ is not coaccessible, this is a contradiction.' references: - Top_not_coaccessible @@ -112,7 +112,7 @@ unsatisfied_properties: proof: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case. - property: effective cocongruences - proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$, respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' + proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ \ast, a, b \}$ with topology $\{ \varnothing, \{ \ast \}, \{ a, b \}, \{ \ast, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ \ast, a \} \rightrightarrows I$ on the discrete space $\{ \ast, a \}$, where the maps are $\ast \mapsto \ast, a \mapsto a$ and $\ast \mapsto \ast, a \mapsto b$, respectively. However, this cannot be effective: if we have $h : Z \to \{ \ast, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $\ast$. But that means the cokernel pair of $h$ is the discrete space on $\{ \ast, a, b \}$.' references: - Top_no_effective_cocongruences diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 8eb4cee3b..fc884d013 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -121,16 +121,16 @@ unsatisfied_properties: proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Unif$ which equips a set $X$ with the indiscrete uniform structure having $X \times X$ as its only entourage. This functor is right adjoint to the forgetful functor and therefore preserves cofiltered limits. - property: effective cocongruences - proof: 'The proof is very similar to $\Top$. Consider the indiscrete uniform space $I$ on two points whose only entourage is $I \times I$. This represents the functor which maps a uniform space $X$ to the set of pairs of points $(x,y) \in X$ that are indistinguishable, i.e. every entourage of $X$ contains $(x,y)$. This is an equivalence relation on $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: If a uniform map $h : Z \to 1$ equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete uniform space on two points.' + proof: 'The proof is very similar to $\Top$. Consider the indiscrete uniform space $I$ on two points whose only entourage is $I \times I$. This represents the functor which maps a uniform space $X$ to the set of pairs of points $(x,y) \in X$ that are indistinguishable, i.e. every entourage of $X$ contains $(x,y)$. This is an equivalence relation on $X$. Therefore, we get a cocongruence $\{\ast\} \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: If a uniform map $h : Z \to \{\ast\}$ equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete uniform space on two points.' references: - Top_no_effective_cocongruences - property: parametrized natural numbers object proof: >- - We equip $[0,1]$ with the usual metric, which induces a uniform structure in the usual way: for $\varepsilon > 0$, we have the basic entourage $U_{\varepsilon} \coloneqq \{(r,s) \in [0,1]^2 : |r-s| < \varepsilon\}$. We equip the set $\IN$ with the discrete uniform structure (i.e., every reflexive relation is an entourage). This uniform space is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} 1$. + We equip $[0,1]$ with the usual metric, which induces a uniform structure in the usual way: for $\varepsilon > 0$, we have the basic entourage $U_{\varepsilon} \coloneqq \{(r,s) \in [0,1]^2 : |r-s| < \varepsilon\}$. We equip the set $\IN$ with the discrete uniform structure (i.e., every reflexive relation is an entourage). This uniform space is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} \{\ast\}$. If there were a parametrized natural numbers object, then by Lemma 4 here, the canonical map - $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \coprod_{n \in \IN} 1 \cong [0,1] \times \IN$$ + $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \coprod_{n \in \IN} \{\ast\} \cong [0,1] \times \IN$$ would be an isomorphism. Choose any sequence of positive numbers $\varepsilon_n > 0$ converging to $0$. Then $\coprod_{n \in \IN} U_{\varepsilon_n}$ is an entourage of $\coprod_{n \in \IN} [0,1]$. Its image in $[0,1] \times \IN$ consists of all $((r,n),(s,m))$ such that $n=m$ and $|r-s| < \varepsilon_n$. Assume, for a contradiction, that this set is an entourage of the product. Then it contains $(p_1 \times p_1)^*(U_\delta) \cap (p_2 \times p_2)^*(\Delta_{\IN})$ for some $\delta > 0$. In other words, $|r-s| < \delta$ implies $|r-s| < \varepsilon_n$ for all $n \in \IN$ and $r,s \in [0,1]$. Taking $s=0$ and $r=\delta/2$, we see that the sequence $(\varepsilon_n)$ is bounded below by $\delta/2$, contradicting the assumption that it converges to $0$. diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index a170d7d80..763106270 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -54,7 +54,7 @@ unsatisfied_properties: proof: See MO/390611 for example. - property: cartesian closed - proof: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small; see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda, which simplifies to $\Hom(1,[F,G]) \cong \Hom(1 \times F,G) \cong \Hom(F,G)$, a contradiction.' + proof: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small; see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda. Since $\Hom(\IZ,-)$ is the terminal object $T$, this simplifies to $\Hom(T,[F,G]) \cong \Hom(T \times F,G) \cong \Hom(F,G)$, a contradiction.' - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor. diff --git a/database/data/categories/cocompletion-discrete-pair-join.yaml b/database/data/categories/cocompletion-discrete-pair-join.yaml index 2759656ed..8331d8ce4 100644 --- a/database/data/categories/cocompletion-discrete-pair-join.yaml +++ b/database/data/categories/cocompletion-discrete-pair-join.yaml @@ -46,7 +46,7 @@ satisfied_properties: label: cocompletion-discrete-pair-join_terminal_presheaf_small proof: >- It suffices to check that the terminal presheaf is small. This follows immediately from the description of small presheaves, since in fact, for every set $X$, the diagram - $$1 ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ 1 \xrightarrow{u_X^*} 1$$ + $$\{\ast\} ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{\ast\} \xrightarrow{u_X^*} \{\ast\}$$ is a coequalizer diagram. Alternatively, one can easily check that the terminal presheaf is a coequalizer of $f_*,g_* : \Hom(-,A) \rightrightarrows \Hom(-,B)$, which directly implies that it is small. - property: epi-regular @@ -83,7 +83,7 @@ unsatisfied_properties: - property: well-powered references: - cocompletion-discrete-pair-join_terminal_presheaf_small - proof: We already know that the terminal presheaf $1$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to 1$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(1)$ is not essentially small. + proof: We already know that the terminal presheaf $T$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to T$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(T)$ is not essentially small. - property: well-copowered proof: >- @@ -157,7 +157,7 @@ unsatisfied_properties: # - property: cofiltered-limit-stable epimorphisms # references: # - cocompletion-discrete-pair-join_terminal_presheaf_small - # proof: We already know that the terminal presheaf $1$ is small. Now consider for $n \in \IN$ the copower $\IN_{\geq n} \otimes 1$ and for $n < m$ the morphism $\IN_{\geq m} \otimes 1 \to \IN_{\geq n} \otimes 1$ induced by the inclusion $\IN_{\geq m} \subseteq \IN_{\geq n}$. This sequence has a limit, the empty presheaf; this can easily be deduced from $\bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$ in $\IN$. Therefore, the unique morphisms $\IN_{\geq n} \otimes 1 \to 1$ are epimorphisms, but their limit $0 \to 1$ is not. + # proof: We already know that the terminal presheaf $T$ is small. Now consider for $n \in \IN$ the copower $\IN_{\geq n} \otimes T$ and for $n < m$ the morphism $\IN_{\geq m} \otimes T \to \IN_{\geq n} \otimes T$ induced by the inclusion $\IN_{\geq m} \subseteq \IN_{\geq n}$. This sequence has a limit, the empty presheaf; this can easily be deduced from $\bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$ in $\IN$. Therefore, the unique morphisms $\IN_{\geq n} \otimes T \to T$ are epimorphisms, but their limit, the morphism from the empty presheaf to $T$, is not. - property: concretizable proof: >- @@ -171,9 +171,9 @@ unsatisfied_properties: special_objects: initial object: - description: constant presheaf with value $0$ + description: constant presheaf with value $\varnothing$ terminal object: - description: constant presheaf with value $1$ + description: constant presheaf with value $\{\ast\}$ coproducts: description: objectwise defined disjoint union of presheaves diff --git a/database/data/categories/forked_commutative_square.yaml b/database/data/categories/forked_commutative_square.yaml index 4f3000855..baaf8afd0 100644 --- a/database/data/categories/forked_commutative_square.yaml +++ b/database/data/categories/forked_commutative_square.yaml @@ -59,15 +59,15 @@ satisfied_properties: $$\textstyle L : \ForkSquare^{\op} \to \Set, \, X \mapsto \lim_{i \in \I} \Hom(X,F(i))$$ is representable. - Since $A$ is initial and $\I$ is connected, we have $L(A)=1$ (the singleton set). + Since $A$ is initial and $\I$ is connected, we have $L(A)=\{\ast\}$. - Case 1: $F$ hits $A$. Then $L(X)= \varnothing$ for every $X \neq A$, since it maps to $\Hom(X,A) = \varnothing$. Moreover, we have $L(A)=1$. Therefore, $L \cong \Hom(-,A)$. + Case 1: $F$ hits $A$. Then $L(X)= \varnothing$ for every $X \neq A$, since it maps to $\Hom(X,A) = \varnothing$. Moreover, we have $L(A)=\{\ast\}$. Therefore, $L \cong \Hom(-,A)$. Case 2: $F$ hits $B$, but does not hit $A$. We claim that $F$ then does not hit $C$. In fact, if $F(i)=B$ and $F(j)=C$, since $\I$ is cosifted, there is a span $$i \leftarrow k \rightarrow j,$$ which induces a span $$B \leftarrow F(k) \rightarrow C.$$ - But then $F(k)=A$ is forced, contradicting our assumption that $F$ does not hit $A$. Therefore, $F$ takes values in $\{B,D,E\}$. Since $B$ has a unique morphism to each of these objects and $\I$ is connected, we see that $L(B)=1$. Moreover, we have $L(C)=\varnothing$ since it maps to $\Hom(C,B)=\varnothing$, and for the same reason we have $L(D)=\varnothing$ and $L(E)=\varnothing$. From these values, it is clear that $L \cong \Hom(-,B)$. (There is a bijection for each object, and naturality is automatic since we are only dealing with sets with at most one element.) + But then $F(k)=A$ is forced, contradicting our assumption that $F$ does not hit $A$. Therefore, $F$ takes values in $\{B,D,E\}$. Since $B$ has a unique morphism to each of these objects and $\I$ is connected, we see that $L(B)=\{\ast\}$. Moreover, we have $L(C)=\varnothing$ since it maps to $\Hom(C,B)=\varnothing$, and for the same reason we have $L(D)=\varnothing$ and $L(E)=\varnothing$. From these values, it is clear that $L \cong \Hom(-,B)$. (There is a bijection for each object, and naturality is automatic since we are only dealing with sets with at most one element.) Case 3: $F$ hits $C$, but does not hit $A$. This is symmetric to Case 2 and leads to $L \cong \Hom(-,C)$. In fact, there is an automorphism of $\ForkSquare$ that swaps $B$ and $C$. @@ -75,7 +75,7 @@ satisfied_properties: Case 5: $F$ takes values in $\{D,E\}$ and hits $D$. In this case, we will show that $L \cong \Hom(-,D)$. Choose $i_0 \in \I$ with $$F(i_0)=D.$$ - Since there is no morphism $E \to D = F(i_0)$, we have $L(E) = \varnothing$. We already know $L(A)=1$. Since $B$ has a unique morphism to each value of $F$ and $\I$ is connected, we see that $L(B)=1$. For the same reason, we have $L(C)=1$. Therefore, it remains to show that $L(D)=1$. + Since there is no morphism $E \to D = F(i_0)$, we have $L(E) = \varnothing$. We already know $L(A)=\{\ast\}$. Since $B$ has a unique morphism to each value of $F$ and $\I$ is connected, we see that $L(B)=\{\ast\}$. For the same reason, we have $L(C)=\{\ast\}$. Therefore, it remains to show that $L(D)=\{\ast\}$. We first show that $L(D)$ has at most one element. Assume that $x,y \in L(D)$. For every $i \in \I$ we have morphisms $x_i,y_i : D \rightrightarrows F(i)$. Since $D$ has only one endomorphism, namely the identity, we must have $x_{i_0} = \id_D = y_{i_0}$. Since $\I$ is connected, it therefore remains to show that $$x_i = y_i \iff x_j = y_j$$ diff --git a/database/data/categories/omega-Set.yaml b/database/data/categories/omega-Set.yaml index 8caf6addc..407877fe9 100644 --- a/database/data/categories/omega-Set.yaml +++ b/database/data/categories/omega-Set.yaml @@ -41,7 +41,7 @@ satisfied_properties: proof: If $(X, R_X) \twoheadrightarrow (Y, R_Y)$ is an epimorphism, then by the description below, this implies the underlying function $X \to Y$ is surjective. Therefore, if $E$ is the kernel pair of this underlying function, then we can find an equivalent quotient object $(X / E, R_{X / E})$ by transporting $R_X$ to $X / E$. The collection of possible equivalence relations $E$ is then small, and for each $E$, the collection of possible $R_{X / E}$ is also small. - property: terminal object - proof: 'The $\omega$-set $\nabla 1 = (1, \IN \times 1)$ is terminal, since $\nabla$ is a right adjoint and therefore preserves terminal objects.' + proof: 'The $\omega$-set $\nabla \{\ast\} = (\{\ast\}, \IN \times \{\ast\})$ is terminal, since $\nabla$ is a right adjoint and therefore preserves terminal objects.' check_redundancy: false - property: binary products @@ -124,7 +124,7 @@ satisfied_properties: - property: regular subobject classifier proof: >- - We claim that $\Omega \coloneqq \nabla 2 = (2, \IN \times 2)$ is a regular subobject classifier, with $\top : 1 \to \Omega$ being the morphism whose underlying set function is $0 \mapsto 1$. To see this, note that from the construction of equalizers above, any regular subobject of $(X, R_X)$ is equivalent to $(X', R_X \cap (\IN \times X'))$ for some $X' \subseteq X$. It is then straightforward to check that the characteristic function $\chi_{X'} : X \to 2$ induces a morphism $(X, R_X) \to \Omega$, and that $(X', R_X \cap (\IN \times X'))$ is also the pullback of $\chi_{X'}$ and $\top$. For the uniqueness of $\chi_{X'}$, observe that for each morphism $\chi : X \to \Omega$, the pullback of $\chi$ and $\top$ has underlying set $\chi^*(\{ 1 \})$ and the morphism to $(X, R_X)$ is the inclusion map. Thus, each morphism $\chi : (X, R_X) \to \Omega$ induces a distinct subobject of $X$ as the pullback of $\chi$ and $\top$. + We claim that $\Omega \coloneqq \nabla \{0,1\} = (\{0,1\}, \IN \times \{0,1\})$ is a regular subobject classifier, with $\top : \nabla \{\ast\} \to \Omega$ being the morphism whose underlying set function is $\ast \mapsto 1$. To see this, note that from the construction of equalizers above, any regular subobject of $(X, R_X)$ is equivalent to $(X', R_X \cap (\IN \times X'))$ for some $X' \subseteq X$. It is then straightforward to check that the characteristic function $\chi_{X'} : X \to \{0,1\}$ induces a morphism $(X, R_X) \to \Omega$, and that $(X', R_X \cap (\IN \times X'))$ is also the pullback of $\chi_{X'}$ and $\top$. For the uniqueness of $\chi_{X'}$, observe that for each morphism $\chi : X \to \Omega$, the pullback of $\chi$ and $\top$ has underlying set $\chi^*(\{ 1 \})$ and the morphism to $(X, R_X)$ is the inclusion map. Thus, each morphism $\chi : (X, R_X) \to \Omega$ induces a distinct subobject of $X$ as the pullback of $\chi$ and $\top$. - property: disjoint finite coproducts proof: >- @@ -137,7 +137,7 @@ satisfied_properties: which is empty since the images of $\iota_1$ and $\iota_2$ are disjoint. Since the realization relation of an $\omega$-set is a subset of $\IN$ times its underlying set, the realization relation of the pullback is empty as well. Hence the pullback is the initial object $(\varnothing, \varnothing)$ constructed above. - property: generator - proof: The terminal object $(1, \IN \times 1)$ represents the forgetful functor $\omegaSet \to \Set$ which is clearly faithful. (For the non-trivial direction of the isomorphism between $\Hom_{\omegaSet}((1, \IN \times 1), (X, R_X))$ and $X$, suppose we have $x \in X$. Then there exists $n \in \IN$ such that $n$ realizes $x$; therefore, the total recursive function given by the constant function with image $n$ forms a realizer tracker compatible with the corresponding function $1 \to X$.) + proof: The terminal object $(\{\ast\}, \IN \times \{\ast\})$ represents the forgetful functor $\omegaSet \to \Set$ which is clearly faithful. (For the non-trivial direction of the isomorphism between $\Hom_{\omegaSet}((\{\ast\}, \IN \times \{\ast\}), (X, R_X))$ and $X$, suppose we have $x \in X$. Then there exists $n \in \IN$ such that $n$ realizes $x$; therefore, the total recursive function given by the constant function with image $n$ forms a realizer tracker compatible with the corresponding function $\{\ast\} \to X$.) - property: extremal generating collection proof: >- @@ -155,15 +155,15 @@ satisfied_properties: - property: extremal cogenerator proof: >- - We first claim that $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $\nabla 2$ of the family. Note that - $$\Hom_{\omegaSet}({-}, \nabla 2) \cong \Hom_{\Set}(U{-}, 2),$$ - where $U : \omegaSet \to \Set$ is the forgetful functor. Therefore, $\Hom_{\omegaSet}({-}, \nabla 2)$ is isomorphic to the composition of $U$ and the power set functor $P : \Set^{\op} \to \Set$, both of which are faithful. This shows that $\nabla 2$ is a cogenerator, so the collection is also a cogenerating collection. + We first claim that $\nabla \{0,1\}$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $\nabla \{0,1\}$ of the family. Note that + $$\Hom_{\omegaSet}({-}, \nabla \{0,1\}) \cong \Hom_{\Set}(U{-}, \{0,1\}),$$ + where $U : \omegaSet \to \Set$ is the forgetful functor. Therefore, $\Hom_{\omegaSet}({-}, \nabla \{0,1\})$ is isomorphic to the composition of $U$ and the power set functor $P : \Set^{\op} \to \Set$, both of which are faithful. This shows that $\nabla \{0,1\}$ is a cogenerator, so the collection is also a cogenerating collection. To show the collection is an extremal cogenerating collection, suppose we have a morphism $f : (X, R_X) \to (Y, R_Y)$ such that ${-} \circ f$ induces bijections of morphism sets to both members of the collection. From the first assumption that - $${-} \circ f : \Hom((Y, R_Y), \nabla 2) \to \Hom((X, R_X), \nabla 2)$$ + $${-} \circ f : \Hom((Y, R_Y), \nabla \{0,1\}) \to \Hom((X, R_X), \nabla \{0,1\})$$ is a bijection, we see that - $${-} \circ f : \Hom_{\Set}(Y, 2) \to \Hom_{\Set}(X, 2)$$ - is a bijection. Since $2$ is an extremal cogenerator of $\Set$, we conclude that the underlying function of $f$ is a bijection. + $${-} \circ f : \Hom_{\Set}(Y, \{0,1\}) \to \Hom_{\Set}(X, \{0,1\})$$ + is a bijection. Since $\{0,1\}$ is an extremal cogenerator of $\Set$, we conclude that the underlying function of $f$ is a bijection. Now, consider the morphism $$g : (X, R_X) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$ @@ -171,14 +171,14 @@ satisfied_properties: $$h : (Y, R_Y) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$ such that $g = h \circ f$. Choose a compatible realizer tracker $\code{h} : \IN \dashrightarrow \IN$. Then for any $x\in X$, if $n$ realizes $f(x)$, then $\code{h}(n)$ exists and $\code{h}(n)$ realizes $h(f(x)) = g(x)$. Thus, by definition of $g$, $\code{h}(n)$ is in the set of realizers of $x$, i.e. $\code{h}(n)$ realizes $x$. From the characterization of isomorphisms below, this implies that $f$ is an isomorphism. - Finally, since $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ both have non-empty underlying sets, they form a strongly connected family (see the proof above that $\omegaSet$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator. + Finally, since $\nabla \{0,1\}$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ both have non-empty underlying sets, they form a strongly connected family (see the proof above that $\omegaSet$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator. references: - omega_Set_ssc - Set_extremal_cogenerator - property: parametrized natural numbers object proof: >- - We claim that $N \coloneqq (\IN, \Delta_{\IN})$, where $\Delta_{\IN}$ is the diagonal, is a parametrized natural numbers object. (In other words, the realization relation is that $m$ realizes $n$ if and only if $m = n$.) First, the zero function $z : 1 \to \IN$ and the successor function $s : \IN \to \IN$ clearly induce morphisms of $\omega$-sets $z : 1 \to N$ and $s : N \to N$. Now, suppose we have $f : (A, R_A) \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$. Choose compatible realizer trackers $\code{f}, \code{g} : \IN \dashrightarrow \IN$. Also, let $\Phi : A \times \IN \to X$ be the function $(a, n) \mapsto g^n(f(a))$. Then since the collection of partial recursive functions is closed under primitive recursion, we can also construct a partial recursive function $\code{\Phi}$ such that + We claim that $N \coloneqq (\IN, \Delta_{\IN})$, where $\Delta_{\IN}$ is the diagonal, is a parametrized natural numbers object. (In other words, the realization relation is that $m$ realizes $n$ if and only if $m = n$.) First, the zero function $z : \{\ast\} \to \IN$ and the successor function $s : \IN \to \IN$ clearly induce morphisms of $\omega$-sets $z : \nabla \{\ast\} \to N$ and $s : N \to N$. Now, suppose we have $f : (A, R_A) \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$. Choose compatible realizer trackers $\code{f}, \code{g} : \IN \dashrightarrow \IN$. Also, let $\Phi : A \times \IN \to X$ be the function $(a, n) \mapsto g^n(f(a))$. Then since the collection of partial recursive functions is closed under primitive recursion, we can also construct a partial recursive function $\code{\Phi}$ such that $$\code{\Phi}(\langle b, 0 \rangle) = \code{f}(b)$$ and $$\code{\Phi}(\langle b, n+1 \rangle) = \code{g}(\code{\Phi}(\langle b, n \rangle)).$$ @@ -196,7 +196,7 @@ unsatisfied_properties: - property: locally finite proof: >- The right adjoint $\nabla : \Set \to \omegaSet$ to the forgetful functor is fully faithful. Therefore, for example, - $$\Hom_{\omegaSet}(\nabla 1, \nabla \IN) \cong \Hom_{\Set}(1, \IN)$$ + $$\Hom_{\omegaSet}(\nabla \{\ast\}, \nabla \IN) \cong \Hom_{\Set}(\{\ast\}, \IN)$$ is infinite. - property: balanced @@ -205,7 +205,7 @@ unsatisfied_properties: - property: co-Malcev proof: >- - Consider the two possible morphisms $j_1, j_2 : \nabla 1 \rightrightarrows \nabla 2$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set + Consider the two possible morphisms $j_1, j_2 : \nabla \{\ast\} \rightrightarrows \nabla \{0,1\}$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set $$\bigl(\{0,1,2\}, \{ (0, 0), (0, 1), (1, 1), (1, 2) \}\bigr),$$ the elements $0$ and $1$ have a common realizer, as do $1$ and $2$; but $0$ and $2$ do not have a common realizer. @@ -213,8 +213,8 @@ unsatisfied_properties: proof: >- Let $N \coloneqq (\IN, \Delta_{\IN})$ be the natural numbers object. Then for any $\omega$-set $(X, R_X)$, we claim $\Hom_{\omegaSet}((X, R_X), N)$ is countable. This follows from the fact that any unary partial recursive function $\varphi : \IN \dashrightarrow \IN$ can be a compatible realizer tracker for at most one function $f : X \to \IN$, since any $x\in X$ is realized by some $n\in \IN$, and then we must have that $\varphi(n)$ is defined and $f(x) = \varphi(n)$. Therefore, we get a surjective function from a subset of the unary partial recursive functions to $\Hom_{\omegaSet}((X, R_X), N)$. - From this, we see that for every infinite set $S$, there is no $S$-indexed copower of $1$, since if $(X, R_X)$ were such a copower, we would have - $$\textstyle\Hom_{\omegaSet}((X, R_X), N) \cong \prod_{s \in S} \Hom_{\omegaSet}(1, N) \cong \IN^S,$$ + From this, we see that for every infinite set $S$, there is no $S$-indexed copower of $\nabla \{\ast\}$, since if $(X, R_X)$ were such a copower, we would have + $$\textstyle\Hom_{\omegaSet}((X, R_X), N) \cong \prod_{s \in S} \Hom_{\omegaSet}(\nabla \{\ast\}, N) \cong \IN^S,$$ which is uncountable. check_redundancy: false @@ -222,7 +222,7 @@ unsatisfied_properties: proof: >- Let $N \coloneqq (\IN, \Delta_{\IN})$ be the natural numbers object. For any $\omega$-set $(X, R_X)$ with a sequence of morphisms $f_n : (X, R_X) \to N$, we can define a function $g : X \to \IN^{\IN}$ which sends $x \in X$ to the sequence $(f_n(x))_{n\in \IN}$. We claim that $g$ has countable image. To see this, choose realizer trackers $\code{f_n} : \IN \dashrightarrow \IN$ compatible with $f_n$. Now let $x \in X$. Then there exists $m \in \IN$ such that $m$ realizes $x$. It follows that $\code{f_n}(m)$ is defined and $\code{f_n}(m) = f_n(x)$ for each $n$. Therefore, the image of $g$ is contained in the set of sequences $(\code{f_n}(m))_{n\in \IN}$ where $m \in \IN$ is such that $\code{f_n}(m)$ is defined for each $n$. - From this, we see that there is no $\IN$-indexed power of $N$. Suppose $(X, R_X)$ were such a power, with projections $p_n : (X, R_X) \to N$, and let $g : X \to \IN^{\IN}$ be the function associated to $(p_n)_{n \in \IN}$ as above. For any sequence $(a_n) \in \IN^{\IN}$, the morphisms $a_n : 1 \to N$ induce a morphism $1 \to (X, R_X)$, that is, an element $x \in X$ with $p_n(x) = a_n$ for all $n$. Then $g(x) = (a_n)$. Thus, $g$ is surjective, which contradicts the countability of its image, since $\IN^{\IN}$ is uncountable. + From this, we see that there is no $\IN$-indexed power of $N$. Suppose $(X, R_X)$ were such a power, with projections $p_n : (X, R_X) \to N$, and let $g : X \to \IN^{\IN}$ be the function associated to $(p_n)_{n \in \IN}$ as above. For any sequence $(a_n) \in \IN^{\IN}$, the morphisms $a_n : \nabla \{\ast\} \to N$ induce a morphism $\nabla \{\ast\} \to (X, R_X)$, that is, an element $x \in X$ with $p_n(x) = a_n$ for all $n$. Then $g(x) = (a_n)$. Thus, $g$ is surjective, which contradicts the countability of its image, since $\IN^{\IN}$ is uncountable. - property: ℵ₁-filtered colimits proof: >- @@ -290,7 +290,7 @@ special_objects: initial object: description: $(\varnothing, \varnothing)$ terminal object: - description: $(1, \IN \times 1)$ + description: $(\{\ast\}, \IN \times \{\ast\})$ coproducts: description: '[binary case] The binary coproduct of $(X, R_X)$ and $(Y, R_Y)$ is $X \sqcup Y$ with realization relation $$R_{X\sqcup Y} \coloneqq \{ (2n, x) \mid (n, x) \in R_X \} \cup \{ (2n+1, y) \mid (n, y) \in R_Y \}.$$' products: @@ -302,7 +302,7 @@ special_morphisms: proof: This is easy, since the condition on the existence of $\psi$ just says that the set-level inverse of $f$ is also a morphism in $\omegaSet$. monomorphisms: description: Morphisms of $\omega$-sets whose underlying set function is injective - proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ is clearly faithful, and it is representable by the terminal object $(1, \IN \times 1)$. + proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ is clearly faithful, and it is representable by the terminal object $(\{\ast\}, \IN \times \{\ast\})$. regular monomorphisms: description: 'A morphism $f : (X, R_X) \to (Y, R_Y)$ is a regular monomorphism if and only if the underlying function $X \to Y$ is injective, and there exists a partial recursive function $\psi : \IN \dashrightarrow \IN$ such that whenever we have $n\in \IN$ and $x\in X$ such that $n$ realizes $f(x) \in Y$, then $\psi(n)$ exists and $\psi(n)$ realizes $x\in X$' proof: 'Following the constructions above, we can see that for any morphism $f : (X, R_X) \to (Y, R_Y)$, the equalizer of the cokernel pair of $f$ is $(\im(f), R_Y \cap (\IN \times \im(f)))$; and the condition above is equivalent to the condition that the canonical map $X \to \im(f)$ induces an isomorphism of $\omega$-sets $(X, R_X) \to (\im(f), R_Y \cap (\IN \times \im(f)))$.' diff --git a/database/data/categories/sSet.yaml b/database/data/categories/sSet.yaml index 07f4019f6..e8b1cdff7 100644 --- a/database/data/categories/sSet.yaml +++ b/database/data/categories/sSet.yaml @@ -42,7 +42,7 @@ special_objects: initial object: description: simplicial set $X$ with $X_n = \varnothing$ terminal object: - description: simplicial set $X$ with $X_n = 1$ + description: simplicial set $X$ with $X_n = \{\ast\}$ coproducts: description: pointwise disjoint union products: diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index f99c81e31..e3d5aa1a1 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -62,7 +62,7 @@ - one-sorted finitary algebraic conclusions: - extremal generator - proof: Pick an algebraic theory that represents the category. The free algebra $F(1)$ on one generator is an extremal generator since it represents the underlying set functor, which is faithful and conservative. + proof: Pick an algebraic theory that represents the category. The free algebra $F(\{\ast\})$ on one generator is an extremal generator since it represents the underlying set functor, which is faithful and conservative. - id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set assumptions: diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index ed65a6a76..19c1de577 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -48,7 +48,7 @@ - trivial conclusions: - coreflector - proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.' + proof: 'Let $F : \C \to \1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : \1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.' - id: reflector_preserves_terminal_objects assumptions: diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index 374cb021d..306ace84e 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -220,7 +220,7 @@ - trivial conclusions: - continuous - proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to 1$ into the trivial category is continuous. This is easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.' + proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to \1$ into the trivial category is continuous. This is easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.' - id: automatically_preserve_equalizers assumptions: [] diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 86cf97da0..432ce438d 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -110,7 +110,7 @@ - trivial conclusions: - right-invertible - proof: 'Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.' + proof: 'Let $\C$ be an inhabited category and let $F : \C \to \1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : \1 \to \C$ satisfies $F \circ X = \id_{\1}$.' - id: full_functor_to_trivial_category # TODO: add the converse once we have category_conclusions @@ -122,7 +122,7 @@ - trivial conclusions: - full - proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to 1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.' + proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to \1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.' - id: functor_conservative_on_groupoids assumptions: [] diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index 3806b6fd4..add60fa96 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/database/data/functors/binary_coproduct_sets.yaml @@ -20,7 +20,7 @@ related: satisfied_properties: - property: right-invertible - proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,0)$ provides a right inverse since $X + 0 \cong X$. + proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,\varnothing)$ provides a right inverse since $X + \varnothing \cong X$. - property: preserves equalizers proof: This can be checked with a straightforward calculation. @@ -44,4 +44,4 @@ unsatisfied_properties: proof: The canonical map $(X_1 \times X_2) + (Y_1 \times Y_2) \to (X_1 + Y_1) \times (X_2 + Y_2)$ is injective, but misses the "mixed terms" $X_1 \times Y_2$ and $Y_1 \times X_2$ in the codomain, hence is not surjective when $X_1,Y_2$ (or $Y_1,X_2$) are non-empty. - property: essentially injective - proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$. + proof: Both $(\{\ast\},\varnothing)$ and $(\varnothing,\{\ast\})$ are mapped to $\{\ast\}$. diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml index dff238106..707d93a42 100644 --- a/database/data/functors/binary_product_sets.yaml +++ b/database/data/functors/binary_product_sets.yaml @@ -20,7 +20,7 @@ related: satisfied_properties: - property: right-invertible - proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,1)$ provides a right inverse since $X \times 1 \cong X$. + proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,\{\ast\})$ provides a right inverse since $X \times \{\ast\} \cong X$. - property: preserves initial objects proof: This is obvious. @@ -44,7 +44,7 @@ unsatisfied_properties: proof: 'If $f,g : A \rightrightarrows B$ are two maps, we always have $f \times \id_{\varnothing} = g \times \id_{\varnothing} : A \times \varnothing \rightrightarrows B \times \varnothing$.' - property: essentially injective - proof: Both $(1,0)$ and $(0,1)$ are mapped to $0$. + proof: Both $(\{\ast\},\varnothing)$ and $(\varnothing,\{\ast\})$ are mapped to $\varnothing$. - property: preserves coequalizers proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the squaring functor, of which we already know that it does not preserve coequalizers.' diff --git a/database/data/functors/continuous_functions.yaml b/database/data/functors/continuous_functions.yaml index ddeea2b27..29790ffff 100644 --- a/database/data/functors/continuous_functions.yaml +++ b/database/data/functors/continuous_functions.yaml @@ -34,8 +34,8 @@ unsatisfied_properties: - property: full proof: >- Every continuous function $\omega_1 \to \IR$ is eventually constant, where $\omega_1$ denotes the first uncountable ordinal equipped with the order topology. We obtain a homomorphism - $$\varphi : C(\omega_1) \to \IR \cong C(1)$$ - mapping each continuous function $\omega_1 \to \IR$ to its eventual value. Assume that it is induced by a continuous map $1 \to \omega_1$. This corresponds to an ordinal $\alpha < \omega_1$ such that $\varphi(u) = u(\alpha)$ for all $u \in C(\omega_1)$. But the continuous function + $$\varphi : C(\omega_1) \to \IR \cong C(\{\ast\})$$ + mapping each continuous function $\omega_1 \to \IR$ to its eventual value. Assume that it is induced by a continuous map $\{\ast\} \to \omega_1$. This corresponds to an ordinal $\alpha < \omega_1$ such that $\varphi(u) = u(\alpha)$ for all $u \in C(\omega_1)$. But the continuous function $$u(\beta) \coloneqq \begin{cases} 0 & \beta \leq \alpha \\ 1 & \beta > \alpha \end{cases}$$ satisfies $\varphi(u) = u(\alpha + 1) \neq u(\alpha)$. diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml index 1dacb2ebe..8cbbb762e 100644 --- a/database/data/functors/countable_copower_sets.yaml +++ b/database/data/functors/countable_copower_sets.yaml @@ -36,7 +36,7 @@ satisfied_properties: unsatisfied_properties: - property: preserves terminal objects - proof: We have $\IN \times 1 \cong \IN \not\cong 1$. + proof: We have $\IN \times \{\ast\} \cong \IN \not\cong \{\ast\}$. - property: preserves binary products proof: The canonical map $\IN \times (X \times Y) \to (\IN \times X) \times (\IN \times Y)$ is given by $(n,(x,y)) \mapsto ((n,x),(n,y))$. It is clearly not surjective when $X$ and $Y$ are non-empty. diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml index d4dae2026..1366f1b6e 100644 --- a/database/data/functors/nerve.yaml +++ b/database/data/functors/nerve.yaml @@ -31,7 +31,7 @@ satisfied_properties: unsatisfied_properties: - property: preserves regular epimorphisms proof: >- - Consider the thin categories $\C = \{0 \to 1, \, 1' \to 2\}$ and $\D = \{0 \to 1 \to 2\}$. There is a regular epimorphism $P : \C \to \D$ that identifies $1$ with $1'$. In fact, it is the coequalizer of the two functors $\{*\} \rightrightarrows \C$ whose images are $1$ and $1'$, respectively. + Consider the thin categories $\C = \{0 \to 1, \, 1' \to 2\}$ and $\D = \{0 \to 1 \to 2\}$. There is a regular epimorphism $P : \C \to \D$ that identifies $1$ with $1'$. In fact, it is the coequalizer of the two functors $\{\ast\} \rightrightarrows \C$ whose images are $1$ and $1'$, respectively. Notice that the map $\Mor(P) : \Mor(\C) \to \Mor(\D)$ is not surjective, as the morphism $0 \to 2$ in $\D$ has no preimage in $\C$. In other words, the map $N_1(P) : N_1(\C) \to N_1(\D)$ is not surjective. Therefore, $N(P)$ is not an epimorphism. - property: dominant diff --git a/database/data/functors/power_set_contravariant.yaml b/database/data/functors/power_set_contravariant.yaml index 84eca828c..331d22c93 100644 --- a/database/data/functors/power_set_contravariant.yaml +++ b/database/data/functors/power_set_contravariant.yaml @@ -19,7 +19,7 @@ related: satisfied_properties: - property: representable - proof: This is because there are natural bijections $P(X) \cong \Hom(X,2)$, sending a subset to its characteristic function. + proof: This is because there are natural bijections $P(X) \cong \Hom(X,\{0,1\})$, sending a subset to its characteristic function. - property: conservative proof: >- @@ -71,7 +71,7 @@ unsatisfied_properties: proof: Consider the sequence of truncation maps $\cdots \twoheadrightarrow \{0,1\}^2 \twoheadrightarrow \{0,1\}^1$. Its limit in $\Set$ (i.e. colimit in $\Set^{\op}$) is $\{0,1\}^{\IN}$, which is uncountable, so that $P(\{0,1\}^{\IN})$ is also uncountable. But the colimit of the induced diagram $P(\{0,1\}^1) \hookrightarrow P(\{0,1\}^2) \hookrightarrow \cdots$ is countable since each set $P(\{0,1\}^n)$ is finite. - property: left-invertible - proof: 'Assume for a contradiction that there is a functor $F : \Set \to \Set^{\op}$ with (natural) isomorphisms $X \cong F(P(X))$. For any non-empty set $X$ there is a map $1 \to X$, which yields a map $F(X) \to F(1)$. Since $F(1) \cong F(P(0)) \cong 0$ is empty, it follows that also $F(X)$ is empty. Since this holds for every non-empty set, it also follows that $X \cong F(P(X)) \cong 0$, which is a contradiction.' + proof: 'Assume for a contradiction that there is a functor $F : \Set \to \Set^{\op}$ with (natural) isomorphisms $X \cong F(P(X))$. For any non-empty set $X$ there is a map $\{\ast\} \to X$, which yields a map $F(X) \to F(\{\ast\})$. Since $F(\{\ast\}) \cong F(P(\varnothing)) \cong \varnothing$ is empty, it follows that also $F(X)$ is empty. Since this holds for every non-empty set, it also follows that $X \cong F(P(X)) \cong \varnothing$, which is a contradiction.' undecidable_properties: - property: essentially injective diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml index fe3da3394..021ff8a82 100644 --- a/database/data/functors/power_set_covariant.yaml +++ b/database/data/functors/power_set_covariant.yaml @@ -73,9 +73,9 @@ unsatisfied_properties: proof: >- Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms $$\alpha_X : X \to F(P(X)).$$ - By the Yoneda lemma, there is some element $u \in F(P(1))$ (where $1$ is the singleton set as usual) such that $\alpha_X$ is given by - $$\alpha_X(x) = F(P(x : 1 \to X))(u).$$ - The map $P(x) : P(1) \to P(X)$ is given by $\varnothing \mapsto \varnothing$ and $1 \mapsto \{x\}$. It factors through the map $e : X + 1 \to P(X)$ which maps $a \in X$ to $\{a\}$ and the unique element of $1$ to $\varnothing$. Since $\alpha_X$ is surjective, it follows that also $F(e) : F(X + 1) \to F(P(X))$ is surjective. Since $e$ is a split monomorphism, also $F(e)$ is a split monomorphism. Hence, $F(e)$ must be an isomorphism. But then $F(X+1) \cong F(P(X)) \cong X$ for all sets $X$. If $X$ is a finite non-empty set, we conclude $\card(F(X)) = \card(X) - 1$. But then + By the Yoneda lemma, there is some element $u \in F(P(\{\ast\}))$ such that $\alpha_X$ is given by + $$\alpha_X(x) = F(P(x : \{\ast\} \to X))(u).$$ + The map $P(x) : P(\{\ast\}) \to P(X)$ is given by $\varnothing \mapsto \varnothing$ and $\{\ast\} \mapsto \{x\}$. It factors through the map $e : X \sqcup \{\ast\} \to P(X)$ which maps $a \in X$ to $\{a\}$ and $\ast$ to $\varnothing$. Since $\alpha_X$ is surjective, it follows that also $F(e) : F(X \sqcup \{\ast\}) \to F(P(X))$ is surjective. Since $e$ is a split monomorphism, also $F(e)$ is a split monomorphism. Hence, $F(e)$ must be an isomorphism. But then $F(X \sqcup \{\ast\}) \cong F(P(X)) \cong X$ for all sets $X$. If $X$ is a finite non-empty set, we conclude $\card(F(X)) = \card(X) - 1$. But then $$\card(X) = \card(F(P(X))) = \card(P(X)) - 1 = 2^{\card(X)} - 1$$ yields a contradiction when $\card(X) > 1$. diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml index d7e170056..f51ad3822 100644 --- a/database/data/functors/rational_product.yaml +++ b/database/data/functors/rational_product.yaml @@ -57,4 +57,4 @@ unsatisfied_properties: Based on the description of regular epimorphisms as surjective quotient maps, this amounts to finding a surjective quotient map $p : X \to Y$ such that the map $p \times \IQ : X \times \IQ \to Y \times \IQ$ (which is certainly surjective) is not a quotient map. The standard example is the projection $p : \IQ \to \IQ / \IZ$ (where $\IZ$ is collapsed to a point); see Brown's Topology and Groupoids, the Example after Theorem 4.3.2 on p. 111. A weaker statement, namely that coequalizers are not preserved, is proven in MSE/2969372. - property: essentially injective - proof: By Sierpiński's theorem on metric spaces, there is a homeomorphism between $\IQ$ and the coproduct $\IQ \sqcup \IQ$. Alternatively, this can be deduced from Cantor's isomorphism theorem on dense linear orders. Thus, $1 \times \IQ \cong 2 \times \IQ$, but of course $1 \not\cong 2$, where $2 = 1 \sqcup 1$ is the discrete space with two points. + proof: By Sierpiński's theorem on metric spaces, there is a homeomorphism between $\IQ$ and the coproduct $\IQ \sqcup \IQ$. Alternatively, this can be deduced from Cantor's isomorphism theorem on dense linear orders. Thus, $\{0\} \times \IQ \cong \{0,1\} \times \IQ$, but of course $\{0\} \not\cong \{0,1\}$, where $\{0,1\}$ carries the discrete topology. diff --git a/database/data/functors/sequences_sets.yaml b/database/data/functors/sequences_sets.yaml index 8698498d3..9ad76feae 100644 --- a/database/data/functors/sequences_sets.yaml +++ b/database/data/functors/sequences_sets.yaml @@ -40,7 +40,7 @@ unsatisfied_properties: proof: A finite set with at least $2$ elements is not contained in the essential image. - property: essentially injective - proof: There is an isomorphism $2^{\IN} \cong 2^{2 \cdot \IN} \cong 4^{\IN}$. There are also counterexamples for infinite sets, such as $\IN^{\IN} \cong 2^{\IN} \cong \IR \cong \IR^{\IN}$. + proof: We have $\{0,1\}^{\IN} \cong \{0,1\}^{\IN \sqcup \IN} \cong (\{0,1\} \times \{0,1\})^{\IN}$, but $\{0,1\} \not\cong \{0,1\} \times \{0,1\}$. There are also counterexamples for infinite sets, such as $\IN^{\IN} \cong \{0,1\}^{\IN} \cong \IR \cong \IR^{\IN}$, but $\IN \not\cong \IR$. - property: finitary proof: >- diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml index b9af8a6c9..d3e857836 100644 --- a/database/data/functors/simple_group_probing.yaml +++ b/database/data/functors/simple_group_probing.yaml @@ -26,7 +26,7 @@ satisfied_properties: unsatisfied_properties: - property: right adjoint # TODO: refactor this once functor implications may have category equality assumptions - proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U \coloneqq G(1)$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.' + proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U \coloneqq G(\{\ast\})$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.' # TODO: refactor this once functor implications may have category_conclusions # here: if a functor preserves terminal objects, and the domain is pointed, diff --git a/database/data/functors/squaring_sets.yaml b/database/data/functors/squaring_sets.yaml index e2226b864..35d276272 100644 --- a/database/data/functors/squaring_sets.yaml +++ b/database/data/functors/squaring_sets.yaml @@ -59,7 +59,7 @@ unsatisfied_properties: proof: >- Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms $$\alpha_X : X \to F(X^2).$$ - By the Yoneda lemma, there is some $u \in F(1)$ such that $\alpha_X$ is given by - $$\alpha_X(x) = F((x,x) : 1 \to X^2)(u)$$ - for $x \in X$. Since $(x,x)$ factors through the diagonal $\Delta_X : X \to X^2$, and $\alpha_X$ is surjective, it follows that $F(\Delta_X) : F(X) \to F(X^2)$ is surjective. It is also injective since $\Delta_X$ is a split monomorphism. Hence, $F(\Delta_X)$ is an isomorphism. + By the Yoneda lemma, there is some $u \in F(\{\ast\}^2)$ such that $\alpha_X$ is given by + $$\alpha_X(x) = F(x \times x)(u)$$ + for $x \in X$, where we regard $x$ as a map $x : \{\ast\} \to X$. Since $x \times x : \{\ast\}^2 \to X^2$ factors through the diagonal $\Delta_X : X \to X^2$, and $\alpha_X$ is surjective, it follows that $F(\Delta_X) : F(X) \to F(X^2)$ is surjective. It is also injective since $\Delta_X$ is a split monomorphism. Hence, $F(\Delta_X)$ is an isomorphism. Thus, $X \cong F(X^2) \cong F(X)$. But then also $X \cong F(X^2) \cong X^2$, and we obtain a contradiction. diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml index 3fe018218..d404a6921 100644 --- a/database/data/functors/trivial_BG.yaml +++ b/database/data/functors/trivial_BG.yaml @@ -6,7 +6,7 @@ associated: codomain: '1' left_adjoint: null right_adjoint: null -description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' +description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' nlab_link: null tags: diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml index ef8537ddc..245fb5721 100644 --- a/database/data/functors/trivial_Idem.yaml +++ b/database/data/functors/trivial_Idem.yaml @@ -6,7 +6,7 @@ associated: codomain: '1' left_adjoint: null right_adjoint: null -description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.' +description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.' nlab_link: null tags: @@ -25,8 +25,8 @@ unsatisfied_properties: - property: left adjoint # TODO: refactor this once functor implications support category_conclusions - proof: A functor $1 \to \Idem$ which is right adjoint to $\Idem \to 1$ provides a terminal object in $\Idem$, which does not exist. + proof: A functor $\1 \to \Idem$ which is right adjoint to $\Idem \to \1$ provides a terminal object in $\Idem$, which does not exist. - property: right adjoint # TODO: refactor this once functor implications support category_conclusions - proof: A functor $1 \to \Idem$ which is left adjoint to $\Idem \to 1$ provides an initial object in $\Idem$, which does not exist. + proof: A functor $\1 \to \Idem$ which is left adjoint to $\Idem \to \1$ provides an initial object in $\Idem$, which does not exist. diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index ef8ee8eb0..4b9f8e50d 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -6,7 +6,7 @@ associated: codomain: '1' left_adjoint: null right_adjoint: null -description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.' +description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.' nlab_link: null tags: diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index 766ff861d..e5dc1cdf8 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -6,7 +6,7 @@ associated: codomain: '1' left_adjoint: null right_adjoint: null -description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' +description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' nlab_link: null tags: diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml index 2a6d2e583..dd065f52d 100644 --- a/database/data/functors/walking_morphism_representation.yaml +++ b/database/data/functors/walking_morphism_representation.yaml @@ -6,7 +6,7 @@ associated: codomain: Set left_adjoint: null right_adjoint: null -description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. +description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{\ast\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. nlab_link: null tags: @@ -29,7 +29,7 @@ satisfied_properties: unsatisfied_properties: - property: preserves epimorphisms - proof: The universal morphism $0 \to 1$ is an epimorphism in $I$ (simply because $I$ is thin), but its image $\varnothing \to \{*\}$ in $\Set$ is not an epimorphism. + proof: The universal morphism $0 \to 1$ is an epimorphism in $I$ (simply because $I$ is thin), but its image $\varnothing \to \{\ast\}$ in $\Set$ is not an epimorphism. - property: dominant proof: This is trivial. diff --git a/database/data/morphisms/terminal-map.yaml b/database/data/morphisms/terminal-map.yaml index 09d6cb10d..838adc586 100644 --- a/database/data/morphisms/terminal-map.yaml +++ b/database/data/morphisms/terminal-map.yaml @@ -3,7 +3,7 @@ name: map into the singleton set notation: $!$ associated: category: Set -description: 'For every set $X$ there is a unique map $! : X \to 1$, where $1$ is the singleton set. In this entry, we require that $X$ has at least $2$ elements.' +description: 'For every set $X$ there is a unique map $! : X \to \{\ast\}$. In this entry, we require that $X$ has at least $2$ elements.' nlab_link: null keywords: - terminal map @@ -15,14 +15,14 @@ related: [] satisfied_properties: - property: split epimorphism - proof: 'Take any element $x \in X$. The corresponding map $x : 1 \to X$ is a section of $! : X \to 1$.' + proof: 'Take any element $x \in X$. The corresponding map $x : \{\ast\} \to X$ is a section of $! : X \to \{\ast\}$.' - property: constant - proof: This is clear because $1$ is terminal; see also Lemma 4 here. + proof: This is clear because $\{\ast\}$ is terminal; see also Lemma 4 here. unsatisfied_properties: - property: monomorphism proof: Since $X$ has two different elements by assumption, which trivially have the same image, the map is not injective. - property: coconstant - proof: 'A direct proof is possible, but we can also argue as follows: Since the map is an epimorphism, if it were coconstant, by the dual of Lemma 5 here, $1$ would be co-subterminal, which is absurd.' + proof: 'A direct proof is possible, but we can also argue as follows: Since the map is an epimorphism, if it were coconstant, by the dual of Lemma 5 here, $\{\ast\}$ would be co-subterminal, which is absurd.' diff --git a/database/data/symmetric_monoidal_categories/1_tensor.yaml b/database/data/symmetric_monoidal_categories/1_tensor.yaml index 278f4eccf..245824b2b 100644 --- a/database/data/symmetric_monoidal_categories/1_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/1_tensor.yaml @@ -1,9 +1,9 @@ id: 1_tensor name: trivial symmetric monoidal category -notation: $(1,\times,0)$ +notation: $(\1,\times,0)$ associated: underlying_category: '1' -description: This is the terminal symmetric monoidal category. It is the trivial category $1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$. +description: This is the terminal symmetric monoidal category. It is the trivial category $\1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$. nlab_link: null tags: diff --git a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml index 3a007e744..226b14b37 100644 --- a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml @@ -1,6 +1,6 @@ id: Cat_cartesian name: cartesian symmetric monoidal category of small categories -notation: $(\Cat,\times,1)$ +notation: $(\Cat,\times,\1)$ associated: underlying_category: Cat description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Cat$ of small categories. diff --git a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml index bcc599a32..789ec1a34 100644 --- a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml @@ -1,6 +1,6 @@ id: Set_cartesian name: cartesian symmetric monoidal category of sets -notation: $(\Set,\times,1)$ +notation: $(\Set,\times,\{\ast\})$ associated: underlying_category: Set description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Set$. diff --git a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml index ddfd1f32d..d6f7260d1 100644 --- a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml @@ -1,6 +1,6 @@ id: Set_cocartesian name: cocartesian symmetric monoidal category of sets -notation: $(\Set,\sqcup,0)$ +notation: $(\Set,\sqcup,\varnothing)$ associated: underlying_category: Set description: Every category with finite coproducts (also called a cocartesian category) can be endowed with a symmetric monoidal structure, where the monoidal unit is the initial object and $\otimes$ is the coproduct $\sqcup$. In this case, we apply this to the category $\Set$. diff --git a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml index a40203abf..cd4667fb0 100644 --- a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml @@ -1,6 +1,6 @@ id: Top_cartesian name: cartesian symmetric monoidal category of topological spaces -notation: $(\Top,\times,1)$ +notation: $(\Top,\times,\{\ast\})$ associated: underlying_category: Top description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Top$. diff --git a/database/data/symmetric_monoidal_category-properties/strict.yaml b/database/data/symmetric_monoidal_category-properties/strict.yaml index dd6084fbc..409a2d6d2 100644 --- a/database/data/symmetric_monoidal_category-properties/strict.yaml +++ b/database/data/symmetric_monoidal_category-properties/strict.yaml @@ -1,6 +1,6 @@ id: strict relation: is -description: 'A symmetric monoidal category is called strict when its associator, symmetry, left unitor, and right unitor are identities. A strict symmetric monoidal category is simply a commutative monoid object in $(\Cat^+,\times,1)$.' +description: 'A symmetric monoidal category is called strict when its associator, symmetry, left unitor, and right unitor are identities. A strict symmetric monoidal category is simply a commutative monoid object in $(\Cat^+,\times,\1)$.' nlab_link: https://ncatlab.org/nlab/show/strict+monoidal+category invariant_under_equivalences: false dual: strict