diff --git a/.cspell.json b/.cspell.json index 07bb5018..03cf0642 100644 --- a/.cspell.json +++ b/.cspell.json @@ -125,6 +125,7 @@ "coproducts", "coprojection", "coprojections", + "coquotient", "coquotients", "coreflection", "coreflective", diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 1ffea278..b55f78c7 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -17,6 +17,9 @@ related: - Set_ff - B - FinGrp + - FinSet_even + - FinSet_odd + - FinSet_power_3 satisfied_properties: - property: locally small diff --git a/database/data/categories/FinSet_even.yaml b/database/data/categories/FinSet_even.yaml new file mode 100644 index 00000000..43e01092 --- /dev/null +++ b/database/data/categories/FinSet_even.yaml @@ -0,0 +1,136 @@ +id: FinSet_even +name: category of finite sets of even cardinality +notation: $\FinSet_{\even}$ +objects: finite sets of even cardinality +morphisms: maps +description: This is the full subcategory of $\FinSet$ consisting of finite sets with even cardinality, for example $\varnothing$ and $\{0,1\}$, but not $\{1\}$. We have included this category only because of its interesting property combinations. +nlab_link: null + +tags: + - set theory + +related: + - FinSet + - FinSet_power_3 + - FinSet_odd + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\FinSet$, which is locally small. + + - property: locally finite + proof: This property is inherited from $\FinSet$. + + - property: essentially countable + proof: This property is inherited from $\FinSet$. + + - property: semi-strongly connected + proof: This property is inherited from $\FinSet$. + + - property: disjoint finite coproducts + proof: A finite disjoint union of finite sets of even cardinality is again finite and has even cardinality, since a finite sum of even natural numbers is even. Moreover, coproducts are disjoint just as in $\FinSet$. + + - property: binary products + proof: This follows from the fact that the product of two even natural numbers is again even. + + - property: strict initial object + proof: The empty set is clearly a strict initial object, just as in $\FinSet$. + + - property: kernel pairs + proof: >- + If $f : X \to Y$ is a map of finite sets with even cardinality, then we claim that its kernel pair in $\FinSet$, the set $\{(x,x') \in X \times X : f(x) = f(x')\}$, also has even cardinality. It decomposes into the diagonal $\{(x,x): x \in X\} \cong X$, which has even cardinality, and the set of pairs $(x,x')$ with $x \neq x'$ and $f(x) = f(x')$. The latter has even cardinality since $C_2$ acts on it via $(x,x') \mapsto (x',x)$ without fixed points. + label: FinSet_even_kernel_pairs + + - property: epi-regular + proof: The epimorphisms are the surjective maps (see below). In $\FinSet$, a surjective map is the coequalizer of its kernel pair, and we have just seen that $\FinSet_{\even}$ is closed under kernel pairs in $\FinSet$. + references: + - FinSet_even_kernel_pairs + + - property: mono-regular + proof: 'If $f : X \to Y$ is a monomorphism, i.e. an injective map (see below), then $f$ is the equalizer of two maps $Y \rightrightarrows \{0,1\}$ in $\Set$, and therefore also in $\FinSet_{\even}$.' + + - property: extremal generator + proof: The two-element set is an extremal generator even in $\Set$ because the squaring functor $X \mapsto X^2$ is faithful and conservative. Now apply Lemma 10 here. + + - property: extremal cogenerator + proof: The two-element set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. + + - property: ℵ₁-filtered + proof: In fact, every small diagram has a cocone in $\FinSet_{\even}$. We take the colimit in $\Set$ and then map it to $\{0,1\}$ via a constant map. + + - property: effective congruences + proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{\even}$. This means that the induced map of sets $E \to X \times X$ is a monomorphism, i.e. injective, and that for every test object $T$ of $\FinSet_{\even}$, the induced injective map $\Hom(T,E) \to \Hom(T,X) \times \Hom(T,X)$ is an equivalence relation in $\Set$. By applying this to $T = \{0,1\}$ and constant maps, it is easy to check that $E \rightrightarrows X$ is a congruence in $\Set$. It is therefore the kernel pair of the projection $X \twoheadrightarrow X/E$ in $\Set$, and hence also in $\FinSet$. If $X/E$ has even cardinality, this remains true in $\FinSet_{\even}$, and we are done. If not, we simply compose the projection with the inclusion $X/E \hookrightarrow X/E + \{\ast\}$. The resulting map $X \to X/E + \{\ast\}$ is a morphism in $\FinSet_{\even}$ with kernel pair $E \rightrightarrows X$. (The last step is also an indication that quotients of congruences do not exist in general, which we will prove later.) + references: + - FinSet_even_no_kernel_pair_quotients + + - property: effective cocongruences + proof: Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{\even}$. In particular, it is a coreflexive corelation. Then $X+X \to Q$ is an epimorphism, hence surjective. It follows that $X \rightrightarrows Q$ is also a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. We have $\card(Q) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is even. Hence, $Q \cong X \sqcup_Y X$ remains true in $\FinSet_{\even}$. + label: FinSet_even_effective_cocongruences + + - property: coquotients of cocongruences + proof: We have just seen that every cocongruence in $\FinSet_{\even}$ is of the form $X \rightrightarrows X \sqcup_Y X$ for some subset $Y \subseteq X$ of even cardinality. The equalizer in $\Set$ is the inclusion $Y \hookrightarrow X$. Since this morphism lies in $\FinSet_{\even}$, it is also the equalizer in $\FinSet_{\even}$. + references: + - FinSet_even_effective_cocongruences + +unsatisfied_properties: + - property: skeletal + proof: The two sets $\{0,1\}$ and $\{2,3\}$ are isomorphic but not equal. + + - property: small + proof: Even the collection of all two-element sets is not a set. + + - property: countable + proof: Even the collection of all two-element sets is not countable. + + - property: strongly connected + proof: There is no map $\{0,1\} \to \varnothing$. + + - property: terminal object + proof: Assume that $T$ is a terminal object, say with $n$ elements. Then $\Hom(\{0,1\},T)$ has $n^2$ elements, but also just one element. Thus, $n = 1$. But then $T$ is not a valid object. + + - property: Cauchy complete + proof: 'The constant map $e : \{0,1\} \to \{0,1\}$, $x \mapsto 0$ is idempotent and does not split in $\FinSet_{\even}$, since a splitting $\{0,1\} \to X \to \{0,1\}$ would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e) = \{0\}$.' + label: FinSet_even_not_cauchy_complete + + - property: extensive + proof: >- + We will show that pullbacks along coproduct inclusions do not exist in general. First, we observe that the inclusion functor $\FinSet_{\even} \hookrightarrow \Set$ is continuous. This follows from the dual of Lemma 1 here since $\FinSet_{\even}$ contains the extremal generator $\{0,1\}$ of $\Set$. + Now consider the inclusion map $\{0,2\} \to \{0,1,2,3\} = \{0,1\} \sqcup \{2,3\}$. Assume that the pullback of this map along the coproduct inclusion from $\{0,1\}$ exists in $\FinSet_{\even}$. Since the inclusion functor to $\Set$ preserves pullbacks, we can compute it as the pullback in $\Set$, which is simply the intersection $\{0,2\} \cap \{0,1\} = \{0\}$. But this is not an object of $\FinSet_{\even}$. + label: FinSet_even_inclusion_continuous + + - property: cokernel pairs + proof: >- + First, the inclusion functor $\FinSet_{\even} \hookrightarrow \Set$ is cocontinuous. This follows from Lemma 1 here since $\FinSet_{\even}$ contains the extremal cogenerator $\{0,1\}$ of $\Set$. + Now consider the constant map $e : \{0,1\} \to \{0,1\}$, $x \mapsto 0$. If it has a cokernel pair in $\FinSet_{\even}$, this must be the cokernel pair in $\Set$, i.e. $\{0,1\} \sqcup_{\{0\}} \{0,1\} \cong \{0,1,1'\}$, whose cardinality, however, is odd. + label: FinSet_even_inclusion_cocontinuous + + - property: coequalizers of kernel pairs + proof: 'We already know that the inclusion functor $\FinSet_{\even} \hookrightarrow \Set$ is continuous and cocontinuous. Moreover, the coequalizer of the kernel pair of a map of sets is simply its image. Thus, it suffices to note that the image of, say, $e : \{0,1\} \to \{0,1\}$, $x \mapsto 0$, does not have even cardinality.' + label: FinSet_even_no_kernel_pair_quotients + references: + - FinSet_even_inclusion_continuous + - FinSet_even_inclusion_cocontinuous + + - property: multi-cocomplete + proof: 'Assume that $D : \I \to \FinSet_{\even}$ is a small diagram. If $(D(i) \to X)_{i \in \I}$ is any cocone, then the constant map $0 : X \to \{0,1\}$ is a morphism of cocones from $(D(i) \to X)_{i \in \I}$ to the cocone $(0 : D(i) \to \{0,1\})_{i \in \I}$. Therefore, the category of cocones under $D$ is connected; it has a weakly terminal object. Thus, if a multi-colimit of $D$ exists, it is necessarily a colimit of $D$. But since we already know that $\FinSet_{\even}$ is not cocomplete (for example, since it is not Cauchy complete), we are done.' + references: + - FinSet_even_not_cauchy_complete + +special_objects: + initial object: + description: empty set + coproducts: + description: '[finite case] disjoint unions' + products: + description: '[non-empty, finite case] direct products' + +special_morphisms: + isomorphisms: + description: bijective maps + proof: It is a full subcategory of $\Set$, in which isomorphisms are bijective maps. + monomorphisms: + description: injective maps + proof: 'For the non-trivial direction, assume that $f : X \to Y$ is a monomorphism and let $a,b \in X$ satisfy $f(a)=f(b)$. Consider the constant maps $a,b : \{0,1\} \to X$ with values $a$ and $b$, respectively. Then $f \circ a = f \circ b$. Thus, $a = b$.' + epimorphisms: + description: surjective maps + proof: Use the same proof as for (finite) sets since there we have only used an auxiliary two-element set, which thus belongs to the given category. diff --git a/database/data/categories/FinSet_odd.yaml b/database/data/categories/FinSet_odd.yaml new file mode 100644 index 00000000..287f6979 --- /dev/null +++ b/database/data/categories/FinSet_odd.yaml @@ -0,0 +1,126 @@ +id: FinSet_odd +name: category of finite sets of odd cardinality +notation: $\FinSet_{\odd}$ +objects: finite sets of odd cardinality +morphisms: maps +description: This is the full subcategory of $\FinSet$ consisting of finite sets of odd cardinality, for example $\{0\}$ and $\{0,1,2\}$, but not $\varnothing$. We have included this category only because of its interesting property combinations. +nlab_link: null + +tags: + - set theory + +related: + - FinSet + - FinSet_even + - FinSet_power_3 + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\FinSet$, which is locally small. + + - property: locally finite + proof: This property is inherited from $\FinSet$. + + - property: essentially countable + proof: This property is inherited from $\FinSet$. + + - property: strongly connected + proof: Use constant maps. + + - property: cartesian closed + proof: This follows from the fact that the product of finitely many odd natural numbers is again odd. Hence, powers of odd numbers are also odd. + + - property: kernel pairs + proof: >- + If $f : X \to Y$ is a map of finite sets with odd cardinality, then we claim that its kernel pair in $\FinSet$, the set $\{(x,x') \in X \times X : f(x) = f(x')\}$, also has odd cardinality. It decomposes into the diagonal $\{(x,x): x \in X\} \cong X$, which has odd cardinality, and the set of pairs $(x,x')$ with $x \neq x'$ and $f(x) = f(x')$. The latter has even cardinality since $C_2$ acts on it via $(x,x') \mapsto (x',x)$ without fixed points. Now use that "odd + even = odd". + label: FinSet_odd_kernel_pairs + + - property: epi-regular + proof: The epimorphisms are the surjective maps (see below). In $\FinSet$, a surjective map is the coequalizer of its kernel pair, and we have just seen that $\FinSet_{\odd}$ is closed under kernel pairs in $\FinSet$. + references: + - FinSet_odd_kernel_pairs + + - property: mono-regular + proof: 'If $f : X \to Y$ is a monomorphism in $\FinSet_{\odd}$, i.e. an injective map (see below), then $f$ is the equalizer of two maps $Y \rightrightarrows \{0,1\}$ in $\Set$, and therefore also of two maps $Y \rightrightarrows \{0,1,2\}$, which thus belong to $\FinSet_{\odd}$.' + + - property: extremal generator + proof: The set $\{0\}$ is an extremal generator even in $\Set$. Now apply Lemma 10 here. + references: + - set_extremal_generator + + - property: extremal cogenerator + proof: The set $\{0,1,2\}$ is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. + + - property: effective congruences + proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{\odd}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $E$ and $X$ are finite sets of odd cardinality. The finite set $X/E$ embeds into a finite set $Q$ of odd cardinality (either $X/E$ or $X/E + \{\ast\}$). Then $E \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/E \hookrightarrow Q$ in $\FinSet_{\odd}$. + + - property: effective cocongruences + proof: >- + Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{\odd}$. The induced map + $$\Hom(Q,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$ + is injective, which implies that $X+X \to Q$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{\odd}$). It follows that $X \rightrightarrows Q$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. We have $\card(Q) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is odd. Hence, $Q \cong X \sqcup_Y X$ remains true in $\FinSet_{\odd}$. + label: FinSet_odd_effective_cocongruences + + - property: coquotients of cocongruences + proof: We have just seen that every cocongruence in $\FinSet_{\odd}$ is of the form $X \rightrightarrows X \sqcup_Y X$ for some subset $Y \subseteq X$ of odd cardinality. The equalizer in $\Set$ is the inclusion $Y \hookrightarrow X$. Since this morphism lies in $\FinSet_{\odd}$, it is also the equalizer in $\FinSet_{\odd}$. + references: + - FinSet_odd_effective_cocongruences + +unsatisfied_properties: + - property: skeletal + proof: The two sets $\{0\}$ and $\{1\}$ are isomorphic but not equal. + + - property: small + proof: Even the collection of all singleton sets is not a set. + + - property: countable + proof: Even the collection of all singleton sets is not countable. + + - property: Cauchy complete + 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}$.' + + - property: binary copowers + proof: A direct proof is possible, but (also for the remaining proofs) 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. + label: FinSet_odd_inclusion_cocontinuous + + - property: cokernel pairs + proof: >- + We already know that the inclusion functor $\FinSet_{\odd} \hookrightarrow \Set$ is cocontinuous. Now consider any map $e : \{0,1,2\} \to \{0,1,2\}$ with image $\{0,1\}$. It is a morphism in $\FinSet_{\odd}$. If it has a cokernel pair in $\FinSet_{\odd}$, this must be the cokernel pair in $\Set$, i.e. $\{0,1,2\} \sqcup_{\{0,1\}} \{0,1,2\} \cong \{0,1,2,2'\}$, whose cardinality, however, is even. + references: + - FinSet_odd_inclusion_cocontinuous + + - property: quotients of congruences + proof: >- + Partition a finite set $X$ of cardinality $3$ into sets of cardinalities $1,2$. This yields an equivalence relation $E \subseteq X \times X$ with + $$\card(E) = 1^2 + 2^2 = 5.$$ + Thus, $E \rightrightarrows X$ is a congruence in $\FinSet_{\odd}$. We already know that the inclusion functor $\FinSet_{\odd} \hookrightarrow \Set$ is cocontinuous, so a quotient in $\FinSet_{\odd}$ must be the quotient taken in $\Set$. However, since there are $2$ equivalence classes, the set $X/E$ has cardinality $2$. Thus, the quotient does not exist in $\FinSet_{\odd}$. + references: + - FinSet_odd_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. + + - property: multi-complete + proof: The same proof as for $\FinSet_{3^\bullet}$ works here. + references: + - FinSet_power_3_not_multi-complete + +special_objects: + terminal object: + description: singleton set + products: + description: '[finite case] direct products' + +special_morphisms: + isomorphisms: + description: bijective maps + proof: It is a full subcategory of $\Set$, in which isomorphisms are bijective maps. + monomorphisms: + description: injective maps + proof: 'The non-trivial direction follows since the inclusion functor to $\Set$ is representable (by the singleton set), and hence preserves monomorphisms.' + epimorphisms: + description: surjective maps + proof: For the non-trivial direction, the inclusion functor to $\Set$ is cocontinuous by Lemma 1 here since $\FinSet_{\odd}$ contains the extremal cogenerator $\{0,1,2\}$ of $\Set$. In particular, it preserves epimorphisms. diff --git a/database/data/categories/FinSet_power_3.yaml b/database/data/categories/FinSet_power_3.yaml new file mode 100644 index 00000000..1b91f9ce --- /dev/null +++ b/database/data/categories/FinSet_power_3.yaml @@ -0,0 +1,130 @@ +id: FinSet_power_3 +name: category of finite sets of cardinality a power of 3 +notation: $\FinSet_{3^\bullet}$ +objects: finite sets whose cardinality is a power of $3$ +morphisms: maps +description: 'This is the full subcategory of $\FinSet$ consisting of finite sets whose cardinality is $3^k$ for some $k \in \IN$. We have included this category only because of its interesting property combinations.' +nlab_link: null + +tags: + - set theory + +related: + - FinSet + - FinSet_even + - FinSet_odd + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\FinSet$, which is locally small. + + - property: locally finite + proof: This property is inherited from $\FinSet$. + + - property: essentially countable + proof: This property is inherited from $\FinSet$. + + - property: strongly connected + proof: Use constant maps. + + - property: cartesian closed + proof: 'We use that $\FinSet$ is cartesian closed. Since $\{3^n : n \geq 0\}$ is closed under finite products (we have $3^0=1$ and $3^n 3^m = 3^{n+m}$) and thus under exponentiation, it follows that $\FinSet_{3^\bullet}$ is closed under finite cartesian products and exponential objects in $\FinSet$.' + + - property: mono-regular + proof: 'If $f : X \to Y$ is a monomorphism in $\FinSet_{3^\bullet}$, i.e. an injective map (see below), then $f$ is the equalizer of two maps $Y \rightrightarrows \{0,1\}$ in $\Set$, and therefore also of two maps $Y \rightrightarrows \{0,1,2\}$, which thus belong to $\FinSet_{3^\bullet}$.' + + - property: epi-regular + proof: 'Let $f : X \to Y$ be an epimorphism in $\FinSet_{3^\bullet}$, i.e. a surjective map (see below). In $\FinSet$, we know that $f$ is the coequalizer of its kernel pair $E \rightrightarrows X$. Since $X$ is non-empty, $E$ is also non-empty. Thus, there is a finite set $F$ whose cardinality is a power of $3$ with a surjection $F \twoheadrightarrow E$. Then $f$ is the coequalizer of $F \rightrightarrows X$ in $\FinSet$, and hence also in $\FinSet_{3^\bullet}$.' + + - property: extremal generator + proof: The set $\{0,1,2\}$ is an extremal generator even in $\Set$. Now apply Lemma 10 here. + + - property: extremal cogenerator + proof: The set $\{0,1,2\}$ is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. + + - property: effective congruences + proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{3^\bullet}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $E$ and $X$ are finite sets of cardinality a power of $3$. Since for every $n \in \IN$ we have $n \leq 3^n$, the finite set $X/E$ embeds into a finite set $Q$ of cardinality a power of $3$. Then $E \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/E \hookrightarrow Q$ in $\FinSet_{3^\bullet}$. + + - property: effective cocongruences + proof: >- + We will prove that, in fact, every cocongruence is trivial. Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{3^\bullet}$. The induced map + $$\Hom(Q,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$ + is injective, which implies that $X+X \to Q$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{3^\bullet}$). It follows that $X \rightrightarrows Q$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. If $X$ has cardinality $3^n$, the cardinality of $Q$ lies in the interval $[3^n,2 \cdot 3^n]$ and is a power of $3$. Thus, $Q$ also has cardinality $3^n$. It follows that $Y=X$ and that the cocongruence is isomorphic to $\id_X,\id_X : X \rightrightarrows X$. In particular, it is the kernel pair of $\id_X : X \to X$. + label: FinSet_power_3_trivial_cocongruences + + - property: coquotients of cocongruences + proof: We have just seen that every cocongruence is trivial and therefore has a coquotient. + references: + - FinSet_power_3_trivial_cocongruences + +unsatisfied_properties: + - property: skeletal + proof: The two sets $\{0\}$ and $\{1\}$ are isomorphic but not equal. + + - property: small + proof: Even the collection of all singleton sets is not a set. + + - property: countable + proof: Even the collection of all singleton sets is not countable. + + - property: Cauchy complete + 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\}$ 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$.' + + - property: binary copowers + proof: >- + First, notice that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous. This follows from Lemma 1 here since $\FinSet_{3^\bullet}$ contains the extremal cogenerator $\{0,1,2\}$ of $\Set$. Therefore, if a binary copower $X+X$ exists in $\FinSet_{3^\bullet}$, and $X$ has $3$ elements, $X+X$ must be the disjoint union, which, however, has $6$ elements, which is not a power of $3$. + + Remark: If we instead consider finite sets of cardinality a power of $2$, then binary copowers do exist, but binary coproducts still do not exist, since $2^0+2^1=3$ is not a power of $2$. + label: FinSet_power_3_inclusion_cocontinuous + + - property: cokernel pairs + proof: We already know that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous, so it suffices to find an example of a map in $\FinSet_{3^\bullet}$ whose cokernel pair in $\Set$ is not contained in $\FinSet_{3^\bullet}$. Take the inclusion map $\{0\} \to \{0,1,2\}$. Then in $\Set$ we compute $\{0,1,2\} \sqcup_{\{0\}} \{0,1,2\} \cong \{0,1,2,1',2'\}$, which has $5$ elements, which is not a power of $3$. + references: + - FinSet_power_3_inclusion_cocontinuous + + - property: kernel pairs + proof: >- + First, notice that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is continuous since it is representable. Therefore, if a map $f : X \to Y$ has a kernel pair in $\FinSet_{3^\bullet}$, it must be the set $\{(x,x') \in X \times X : f(x)=f(x')\}$. + But consider the map $f : \{0,1,2\} \to \{0,1,2\}$ defined by $f(0)=0$, $f(1)=1$, $f(2)=1$. Then the set in question is given by + $$\{(0,0), (1,1), (2,2), (1,2), (2,1) \}.$$ + It has cardinality $5$, which, however, is not a power of $3$. + + - property: quotients of congruences + proof: >- + Partition a finite set $X$ of cardinality $9$ into sets of cardinalities $1,1,3,4$. This yields an equivalence relation $E \subseteq X \times X$ with + $$\card(E) = 1^2 + 1^2 + 3^2 + 4^2 = 27 = 3^3.$$ + Thus, $E \rightrightarrows X$ is a congruence in $\FinSet_{3^\bullet}$. We already know that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous, so a quotient in $\FinSet_{3^\bullet}$ must be the quotient taken in $\Set$. However, since there are $4$ equivalence classes, the set $X/E$ has cardinality $4$. Thus, the quotient does not exist in $\FinSet_{3^\bullet}$. + references: + - 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. + + - property: multi-complete + proof: >- + Let $I$ be an infinite set and, for every $i \in I$, let $A_i$ be a set of cardinality $3$. Assume that the multi-product of the family $(A_i)_{i \in I}$ exists in $\FinSet_{3^\bullet}$, i.e. that the category of cones has a multi-terminal object. Here, a cone can be identified with a map + $$\textstyle f : X \to \prod_{i \in I} A_i,$$ + where $X \in \FinSet_{3^\bullet}$ and the product is taken in $\Set$. Therefore, there is a family of cones $(p_j : P_j \to \prod_{i \in I} A_i)_{j \in J}$ such that for every cone $f : X \to \prod_{i \in I} A_i$ there is a unique index $j \in J$ and a unique map $g : X \to P_j$ such that $p_j \circ g = f$. Applying this to $X = \{0\}$, we see that the maps $p_j$ induce a bijective map + $$\textstyle\coprod_{j \in J} P_j \to \prod_{i \in I} A_i.$$ + In particular, the images of the maps $p_j$ are pairwise disjoint. Since $\prod_{i \in I} A_i$ is an infinite set, $J$ is infinite. In particular, there are distinct indices $j_1,j_2 \in J$. Choose elements $y_1 \in P_{j_1}$ and $y_2 \in P_{j_2}$. There is a map $f : \{0,1,2\} \to \prod_{i \in I} A_i$ with image $\{p_{j_1}(y_1), p_{j_2}(y_2)\}$. By assumption, there is some (unique) index $k \in J$ such that $f$ factors through $p_k$. But then both $p_{j_1}(y_1)$ and $p_{j_2}(y_2)$ are contained in the image of $p_k$, so that $j_1 = k = j_2$, which is a contradiction. + label: FinSet_power_3_not_multi-complete + +special_objects: + terminal object: + description: singleton set + products: + description: '[finite case] direct products' + +special_morphisms: + isomorphisms: + description: bijective maps + proof: It is a full subcategory of $\Set$, in which isomorphisms are bijective maps. + monomorphisms: + description: injective maps + proof: The non-trivial direction follows since the forgetful functor to $\Set$ is representable (by the singleton set), and hence preserves monomorphisms. + epimorphisms: + description: surjective maps + proof: For the non-trivial direction, the forgetful functor to $\Set$ is cocontinuous by Lemma 1 here since $\FinSet_{3^\bullet}$ contains the extremal cogenerator $\{0,1,2\}$ of $\Set$. In particular, it preserves epimorphisms. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 6eaf4808..f90e0a2c 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -50,6 +50,8 @@ \Ob: \operatorname{Ob} \id: \operatorname{id} \ev: \operatorname{ev} +\even: \operatorname{even} +\odd: \operatorname{odd} \card: \operatorname{card} \colim: \operatorname{colim} \im: \operatorname{im}