diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 1ffea278..62a990a5 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -17,6 +17,8 @@ related: - Set_ff - B - FinGrp + - FinSet_even + - 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..910d9923 --- /dev/null +++ b/database/data/categories/FinSet_even.yaml @@ -0,0 +1,135 @@ +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 + +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 indicator 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$, for which we know that 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_power_3.yaml b/database/data/categories/FinSet_power_3.yaml new file mode 100644 index 00000000..cce921c1 --- /dev/null +++ b/database/data/categories/FinSet_power_3.yaml @@ -0,0 +1,115 @@ +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 + +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 exponentiation (we have $(3^n)^{3^m} = 3^{n 3^m}$), 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, also $E$ is 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 cocongruence 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}$. + +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\} \to \{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 that 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 mentioned set 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: reflexive coequalizers + proof: 'We already know that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous, so that it suffices to find a reflexive pair in $\FinSet_{3^\bullet}$ whose coequalizer in $\Set$ is not contained in $\FinSet_{3^\bullet}$. Consider the maps $f,g : \{1,2,3,4,5,6,7,8,9\} \rightrightarrows \{1,2,3\}$ defined by $f(x)=g(x)=x$ for $x \in \{1,2,3\}$, $f(4)=2$, $g(4)=3$, and $f(x)=g(x)=1$ for $x \geq 5$. The inclusion map from $\{1,2,3\}$ into $\{1,2,3,4,5,6,7,8,9\}$ provides a common section of $f,g$. The coequalizer of $f,g$ in $\Set$ is the quotient of $\{1,2,3\}$ modulo $2 \sim 3$. Its cardinality is $2$, which is not a power of $3$.' + references: + - FinSet_power_3_inclusion_cocontinuous + + - 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 that 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. + +special_objects: + initial object: + description: empty set + 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$, for which we know that 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), 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..5045d276 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -50,6 +50,7 @@ \Ob: \operatorname{Ob} \id: \operatorname{id} \ev: \operatorname{ev} +\even: \operatorname{even} \card: \operatorname{card} \colim: \operatorname{colim} \im: \operatorname{im}