diff --git a/content/generator_construction.md b/content/generator_construction.md index a7cef4c6..b2a31f77 100644 --- a/content/generator_construction.md +++ b/content/generator_construction.md @@ -1,13 +1,19 @@ --- title: Construction of Generators description: How to construct a generator from a generating set -author: Martin Brandenburg +authors: + - Martin Brandenburg + - Daniel Schepler --- ## Construction of Generators ::: Lemma -In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected) (between any two objects in $S$ there is a morphism). If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. +In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator. ::: -_Proof._ This is a straight forward generalization of [this result](/category-implication/generator_via_coproduct). We remark that the assumption about $S$ implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$. $\square$ +_Proof._ We remark that the assumption on $S$ implies that each coprojection $i_G : G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f \circ \bar a = g \circ \bar a$ for all $\bar a : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $f \circ a = g \circ a$ holds for all morphisms $a : G \to A$ with $G \in S$. Since $S$ is a generating set, this implies $f = g$. + +Similarly, for the case where $S$ is an extremal generating set, suppose we have a morphism $f : A \to B$ such that $f \circ {-} : \Hom(U, A) \to \Hom(U, B)$ is a bijection. In particular, because it is injective and $U$ is a generator, we can conclude that $f$ is a monomorphism, so $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is injective for each $G \in S$. Now suppose $b \in \Hom(G, B)$ for $G \in S$. Then $b$ extends to a morphism $\bar b : U \to B$. By assumption, there exists $\bar a : U \to A$ such that $f \circ \bar a = \bar b$. Composing with the coprojection $i_G : G \to U$, we see +$$f \circ \bar a \circ i_G = \bar b \circ i_G = b.$$ +This shows that $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is also surjective for each $G \in S$. Since $S$ is an extremal generating set, this implies $f$ is an isomorphism. $\square$ diff --git a/content/subcategories.md b/content/subcategories.md index 977fb09b..34040feb 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -116,3 +116,9 @@ $$ $$ is a composition of faithful functors, hence faithful. $\square$ + +::: Lemma 10 +Any fully faithful functor reflects extremal generating sets (and therefore, by duality, it also reflects extremal cogenerating sets). In other words, if $U : \C \to \D$ is a fully faithful functor, and $S$ is a set of objects such that $U(S)$ is an extremal generating set of $\D$, then $S$ is an extremal generating set of $\C$. +::: + +_Proof:_ Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative. $\square$ diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md new file mode 100644 index 00000000..fd20f49e --- /dev/null +++ b/content/thin_extremal_generator.md @@ -0,0 +1,23 @@ +--- +title: Thin Category with an Extremal Generator +description: A result restricting which thin categories can have an extremal generator +author: Daniel Schepler +--- + +# Thin Category with an Extremal Generator + +::: Lemma +Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism. +::: + +_Proof._ ($\Rightarrow$) Since the category is thin, $\Hom(G, X)$ is either a singleton or empty. In the first case, let $f \in \Hom(G, X)$. Then $f \circ {-} : \Hom(G, G) \to \Hom(G, X)$ is automatically a bijection since $\Hom(G, G) = \{ \id_G \}$ is also a singleton, implying that $f$ is an isomorphism. + +In the second case, suppose we have a morphism $g : Y \to X$. Then $g \circ {-} : \Hom(G, Y) \to \Hom(G, X)$ is a function with empty codomain, so it is automatically a bijection, implying that $g$ is an isomorphism. + +($\Leftarrow$) Since the category is thin, any object is automatically a generator. Now suppose we have a morphism $f : X \to Y$ such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then by assumption, either $Y \cong G$ or every morphism with codomain $Y$ is an isomorphism. In the first case, $\Hom(G, Y)$ is non-empty, so $\Hom(G, X)$ is also non-empty. We also have $\Hom(Y, G)$ is non-empty. Therefore, $\Hom(Y, X)$ is non-empty, and the (necessarily unique) morphism $Y \to X$ is automatically an inverse to $f$. In the second case, $f$ is already a morphism with codomain $Y$ so it is an isomorphism. $\square$ + +::: Corollary +For a poset $P$, the corresponding thin category has an extremal generator if and only if $P$ is non-empty and it has at most one non-minimal element. In particular, if this is the case, then either the poset is discrete, in which case any element gives an extremal generator; or otherwise, there is exactly one non-minimal element which is the unique extremal generator. +::: + +_Proof._ In a thin category coming from a poset, the condition in the previous lemma that every morphism with codomain $X$ is an isomorphism is equivalent to the corresponding element of the poset being minimal. $\square$ diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index 7ab864bd..41588e5b 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/database/data/categories/Ab_fg.yaml @@ -21,8 +21,8 @@ satisfied_properties: - property: abelian proof: This follows from the fact for abelian groups and the fact that subgroups of finitely generated abelian groups are also finitely generated. - - property: generator - proof: The group $\IZ$ is a generator since it represents the forgetful functor to $\Set$. + - property: extremal generator + proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor to $\Set$ which is faithful and conservative. - property: essentially countable proof: Every finitely generated abelian group is isomorphic to a group of the form $\IZ^n / U$, where $n \in \IN$ and $U$ is a subgroup of $\IZ^n$. Since $\IZ^n$ is Noetherian as a $\IZ$-module, $U$ is finitely generated, hence the category $\Ab_\fg$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \IZ^n / U$ and $B \cong \IZ^m / T$, the hom-set $\Hom(A,B)$ is countable. Indeed, precomposition with the quotient map yields an injection $\Hom(A,B) \hookrightarrow \Hom(\IZ^n, B) \cong B^n$, and $B^n$ is countable. diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml index f42a8899..15e6a078 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -20,9 +20,6 @@ satisfied_properties: proof: The trivial Banach space $\{0\}$ is a zero object. check_redundancy: false - - property: cogenerator - proof: The Hahn-Banach theorem implies that $\IC$ is a cogenerator. - - property: CIP proof: This is immediate from the concrete description of coproducts and products. @@ -35,6 +32,10 @@ satisfied_properties: - property: cocartesian cofiltered limits proof: 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\Ban \to \Vect$ preserves finite coproducts and all limits, and $\Vect$ has the claimed property (see here), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.' + - property: extremal cogenerator + proof: >- + The Hahn-Banach theorem implies that $\IC$ is a cogenerator. We claim that it is in fact an extremal cogenerator. Thus, suppose $f : X \to Y$ is a morphism such that ${-} \circ f : \Hom(Y, \IC) \to \Hom(X, \IC)$ is bijective on the underlying sets. Then for any non-zero $x \in X$, by the Hahn-Banach theorem, there exists $\varphi \in X^*$ such that $|\varphi| = 1$ and $\varphi(x) = |x|$. Since $|\varphi| = 1$, we see that $\varphi$ is a morphism $X \to \IC$ in $\Ban$; so by the assumption, there exists a morphism $\psi : Y \to \IC$ such that $\varphi = \psi \circ f$. Therefore, $|x| = |\psi(f(x))| \le |f(x)|$; and conversely, since $f$ is a morphism, $|f(x)| \le |x|$. On the other hand, if $x = 0$, then certainly $|f(x)| = |x| = 0$. This shows that $f$ is isometric and therefore a regular monomorphism (see below). On the other hand, since $\IC$ is a cogenerator and ${-} \circ f$ is injective, we have $f$ is also an epimorphism. Hence, $f$ is an isomorphism. + - property: regular proof: >- It suffices to prove that regular epimorphisms are stable under pullbacks. We will use their classification via open unit balls below. diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 58c86d4f..ac10a69c 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -27,12 +27,15 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty category is weakly terminal (by using constant functors). - - property: generator - proof: 'The walking morphism $I$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $I$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms.' - - property: infinitary extensive proof: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' + - property: extremal generator + proof: >- + The walking morphism $I$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $I$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms. + + In fact, $I$ is an extremal generator: suppose $F : \C \to \D$ is a functor which induces a bijection $\Mor(\C) \to \Mor(\D)$. By considering the images of identity morphisms in $\C$, we see that $F$ is injective on objects; and then by considering the preimages of identity morphisms in $\D$, we see that $F$ is surjective on objects. By assumption, $F$ is also bijective on morphisms, so $F$ is an isomorphism of categories. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index 2c8930b4..fb79a8b1 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -33,11 +33,11 @@ satisfied_properties: - property: strongly connected proof: For all $n,m$ there are morphisms $[n] \to [0] \to [m]$. - - property: generator - proof: The ordered set $[0] = \{0\}$ is a generator. + - property: extremal generator + proof: The ordered set $[1] = \{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. - - property: cogenerator - proof: The ordered set $[1] = \{0 < 1\}$ is a cogenerator, even for $\Pos$. + - property: extremal cogenerator + proof: The ordered set $[1] = \{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. - property: skeletal proof: 'If $f : [n] \to [m]$ is an isomorphism, then $n + 1 = m + 1$ by comparing the cardinalities, hence $n = m$.' diff --git a/database/data/categories/FI.yaml b/database/data/categories/FI.yaml index 0db4df27..21c676b8 100644 --- a/database/data/categories/FI.yaml +++ b/database/data/categories/FI.yaml @@ -26,8 +26,8 @@ satisfied_properties: - property: left cancellative proof: This is trivial. - - property: generator - proof: The one-point set is a generator since it represents the forgetful functor $\FI \to \Set$. + - property: extremal generator + proof: The one-point set is a generator since it represents the forgetful functor $\FI \to \Set$, which is faithful and conservative. - property: essentially countable proof: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$. diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index c5415c43..7defa5b1 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -28,9 +28,6 @@ satisfied_properties: - property: right cancellative proof: This is trivial. - - property: cogenerator - proof: 'We prove that $\{0,1\}$ is a cogenerator: The surjective maps $X \to \{0,1\}$ correspond to the non-empty proper subsets of $X$. If $a,b \in X$ are elements that have the same image under each surjective map $X \to \{0,1\}$, it therefore means that they lie in the same non-empty proper subsets of $X$. This implies $a=b$: If $X = \{a\}$, this is trivial. Otherwise, use the subset $\{a\}$.' - - property: coequalizers proof: We construct coequalizers as in $\FinSet$ (or $\Set$) and observe that the universal property still holds when we restrict to surjective maps. @@ -40,6 +37,12 @@ satisfied_properties: - property: epi-regular proof: 'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\FinSet$, but also in $\FS$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\FS$, we can use this finite set here.' + - property: extremal cogenerator + proof: >- + We prove that $\{0,1\}$ is an extremal cogenerator. First, to prove it is a cogenerator: The surjective maps $X \to \{0,1\}$ correspond to the non-empty proper subsets of $X$. If $a,b \in X$ are elements that have the same image under each surjective map $X \to \{0,1\}$, it therefore means that they lie in the same non-empty proper subsets of $X$. This implies $a=b$: If $X = \{a\}$, this is trivial. Otherwise, use the subset $\{a\}$. + + Now, suppose we have a surjective map $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty proper subsets, and it certainly also maps $\varnothing \mapsto \varnothing$ and $Y \mapsto X$. Therefore, since the contravariant powerset functor is conservative, that implies $f$ is an isomorphism. + - property: multi-complete proof: >- Let $D : \I \to \FS$ be a small diagram. Let $L \subseteq \prod_{i \in \I} D(i)$ be the limit object of the corresponding diagram in $\Set$. Consider the set of all finite subsets $R \subseteq L$ with the property that $p_i(R) = D(i)$ for every $i \in \I$. For each of these, $(R \xrightarrow{p_i|_R} D(i))_{i \in \I}$ is a cone in $\FS$. We claim that the set of these cones is universal: diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 29d7ae93..8eef9bf8 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -47,6 +47,19 @@ satisfied_properties: - property: cogenerator proof: It is straightforward to check that the vector space $K$ equipped with the maximal filtration $F^n(K) \coloneqq K$ is a cogenerator. + check_redundancy: false + + - property: extremal cogenerating set + proof: >- + Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space equipped with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V^*$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. + + First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, G)$ such that + $${-} \circ f : \Hom((W, G), K_\infty) \to \Hom((V, F), K_\infty)$$ + is a bijection. This implies that $f^* : W^* \to V^*$ is a bijection of the dual vector spaces, and therefore an isomorphism. By standard linear algebra, this implies that $f : V \to W$ is an isomorphism of vector spaces. + + It remains to show that if $f$ also induces a bijection + $${-} \circ f : \Hom((W, G), K_n) \to \Hom(V, F), K_n)$$ + for each $n$, then $f$ induces an isomorphism of the filtrations. For this step, we may assume without loss of generality that $f = \id_V : V \to V$. By the observations above, this implies that $F_n(V)^\perp = G_n(V)^\perp$. By standard linear algebra, we conclude $F_n(V) = G_n(V)$. - property: finitely accessible proof: >- diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index ff171468..20626dd9 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -34,11 +34,11 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty totally ordered set is weakly terminal (by using constant maps). - - property: generator - proof: The one-point finite ordered set is a generator since it represents the forgetful functor $\FinOrd \to \Set$. + - property: extremal generator + proof: The ordered set $\{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. - - property: cogenerator - proof: The ordered set $\{0 < 1\}$ is a cogenerator, even for $\Pos$. + - property: extremal cogenerator + proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. - property: equalizers proof: Take the equalizer in $\FinSet$ and restrict the order. diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index be7aa454..193a2eb6 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -26,11 +26,11 @@ satisfied_properties: - property: essentially countable proof: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$. - - property: generator - proof: The one-point set is a generator since it represents the forgetful functor $\FinSet \to \Set$. + - property: extremal generator + proof: The one-point set is an extremal generator even in $\Set$. Now apply Lemma 10 here. - - property: cogenerator - proof: The two-element set is a cogenerator. + - property: extremal cogenerator + proof: The two-element set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. - property: semi-strongly connected proof: Every non-empty finite set is weakly terminal (by using constant maps). diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 02db896f..98cb1cb4 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -23,8 +23,8 @@ satisfied_properties: - property: essentially countable proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a countable set. - - property: generator - proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_f.yaml b/database/data/categories/FinVect_f.yaml index 78006a99..7fa859c9 100644 --- a/database/data/categories/FinVect_f.yaml +++ b/database/data/categories/FinVect_f.yaml @@ -26,8 +26,8 @@ satisfied_properties: - property: locally finite proof: Each hom-set $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is finite by assumption. - - property: generator - proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index c7734fc3..49fb75b9 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -23,8 +23,8 @@ satisfied_properties: - property: essentially small proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a set. - - property: generator - proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index ab65e1fd..e27292b7 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -23,8 +23,8 @@ satisfied_properties: - property: coproducts proof: This is is because free abelian groups are closed under direct sums of abelian groups. - - property: generator - proof: As for $\Ab$, the group $\IZ$ is a generator. + - property: extremal generator + proof: The group $\IZ$ is an extremal generator even in $\Grp$. Now apply Lemma 10 here. - property: cogenerator proof: It is easy to check that $\IZ$ is a cogenerator for free abelian groups. diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 68fe0c40..0ffee152 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -39,6 +39,10 @@ satisfied_properties: - property: effective cocongruences proof: A proof can be found here. + - property: extremal generator + proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor $\Grp \to \Set$, which is faithful and conservative. + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 7b2f8593..da6d60f2 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -25,8 +25,8 @@ satisfied_properties: proof: The trivial group is countable and is a zero object. check_redundancy: false - - property: generator - proof: The countable group $\IZ$ is a generator because it represents the forgetful functor $\Grp_\c \to \Set$. + - property: extremal generator + proof: The countable group $\IZ$ is an extremal generator even in $\Grp$. Now use Lemma 10 here. - property: finite products proof: This is because $\Grp$ has finite (in fact, all) products, and $\Grp_\c \hookrightarrow \Grp$ is closed under finite products. This is because a finite product of countable sets is again countable. diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 130249be..02687dc5 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -53,9 +53,6 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: balanced - proof: The inclusion $\IQ \hookrightarrow \IR$ is a counterexample; it is an epimorphism since $\IQ$ is dense in $\IR$. - - property: Malcev proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff). @@ -74,9 +71,6 @@ unsatisfied_properties: $$(-\infty, -1/n] \cup [1/n, \infty) \hookrightarrow \IR$$ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \IR$ in the colimit, which is not a monomorphism. - - property: accessible - proof: In fact, it does not have any small colimit-dense subcategory by MSE/4097315. - - property: cogenerator # cspell: disable-next-line proof: 'Assume that $Q$ is a cogenerator. Since $Q$ is Hausdorff, $Q$ is $T_1$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X$ with $\geq 2$ points such that every continuous map $X \to Q$ is constant. (The author only states that $X$ is regular, but actually, $X$ is regular and $T_1$, hence Hausdorff.) But since $Q$ is a cogenerator, this implies that all maps $1 \rightrightarrows X$ are equal, i.e. that $X$ has just one point. This is a contradiction.' @@ -91,6 +85,9 @@ unsatisfied_properties: Let $C \coloneqq \{1,2\}$ be the discrete two-point space. The map $f : A \to C$ defined by $f(a)=1$ for $a \in A_1$ and $f(a)=2$ for $a \in A_2$ is continuous, since $A$ is discrete. The pushout $C \sqcup_A \Gamma$ in $\Haus$ is the Hausdorff reflection of the pushout $Q$ in $\Top$. Notice that $Q$ is the quotient space of $\Gamma$ in which $A_1$ and $A_2$ are each collapsed to a point, denoted by $[A_1]$ and $[A_2]$. The canonical map $C \to Q$ is given by $i \mapsto [A_i]$. Now, $[A_1]$ and $[A_2]$ cannot be separated by disjoint open neighborhoods in $Q$, since such neighborhoods would pull back to disjoint open neighborhoods of $A_1$ and $A_2$ in $\Gamma$. Thus, they are identified in the Hausdorff reflection. This shows that the canonical map $C \to C \sqcup_A \Gamma$ is not injective and hence not a regular monomorphism. + - property: extremal generating set + 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. + special_objects: initial object: description: empty space diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index e3e6a664..5e4eeacd 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -22,12 +22,6 @@ satisfied_properties: proof: In short, this follows from the corresponding statement for topological spaces and $\IR^n \times \IR^m \cong \IR^{n+m}$. check_redundancy: false - - property: generator - proof: The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Top \to \Set$. - - - property: cogenerator - proof: 'The manifold $\IR$ is a cogenerator, since for every smooth manifold $M$ and points $p \neq q$ in $M$ there is a smooth function $f : M \to \IR$ with $f(p) = 1$ and $f(q) = 0$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25).' - - property: semi-strongly connected proof: Every non-empty manifold is weakly terminal (by using constant maps). @@ -52,6 +46,24 @@ satisfied_properties: - property: effective cocongruences proof: 'From the proof that $\Man$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.' + - 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. + + 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. + + - property: extremal cogenerator + proof: >- + The manifold $\IR$ is a cogenerator, since for every smooth manifold $M$ and points $p \neq q$ in $M$ there is a smooth function $f : M \to \IR$ with $f(p) = 1$ and $f(q) = 0$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25). + + In fact, $\IR$ is an extremal cogenerator. To see this, suppose we have a smooth map $f : M \to N$ such that ${-} \circ f : \Hom(N, \IR) \to \Hom(M, \IR)$ is a bijection. Then using bump maps as before to separate points of $M$, we can see that $f$ must be injective on underlying sets. Also, since $\IR$ is a cogenerator and ${-} \circ f$ is injective, we get that $f$ is an epimorphism, so it has dense image (see below). We claim that in fact, $f$ is surjective. To see this, suppose we had $q \in N \setminus \im(f)$. Then there is a smooth function $\varphi : N \to \IR$ such that $\varphi^*(\{0\}) = \{q\}$ (John Lee, Introduction to Smooth Manifolds, Thm. 2.29). But then we can construct a smooth function $\psi : M \to \IR$ by + $$\psi(p) \coloneqq \frac{1}{\varphi(f(p))}.$$ + Let $\xi : N \to \IR$ be the corresponding smooth function such that $f^* \xi = \psi$. Then $\varphi \cdot \xi$ must take value $1$ at any point in the image of $f$. Since the image of $f$ is dense, that implies that $\varphi \cdot \xi$ is the constant function with value 1, contradicting the fact that $\varphi(q) = 0$. + + Now, recall that the tangent space $T_p(M)$ of $M$ at a point $p$ is defined as the space of $\IR$-linear functions $\partial : C^\infty(M) \to \IR$ such that $\partial(gh) = g(p) \partial(h) + h(p) \partial(g)$; and similarly for the tangent space of $N$ at $f(p)$. Also, the push-forward $f_* : T_p(M) \to T_{f(p)}(N)$ is defined by precomposition with $f^* : C^\infty(N) \to C^\infty(M)$. But by assumption, $f^* : C^\infty(N) \to C^\infty(M)$ is a bijection. Also, $f^* : C^\infty(N) \to C^\infty(M)$ is a homomorphism of $\IR$-algebras, so its inverse function $(f^*)^{-1} : C^\infty(M) \to C^\infty(N)$ is also a homomorphism of $\IR$-algebras. Furthermore, + $$(f^*)^{-1}(g)(f(p)) = f^*((f^*)^{-1}(g))(p) = g(p)$$ + for each $g \in C^\infty(M)$. Therefore, we see that for each $\partial \in T_{f(p)}(N)$, $\partial \circ (f^*)^{-1} \in T_p(M)$, and this defines an inverse to $f_* : T_p(M) \to T_{f(p)}(N)$. Thus, by the inverse function theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index d7221d06..aa3256ba 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -25,9 +25,6 @@ satisfied_properties: - property: generator proof: The one-point measurable space (with the unique $\sigma$-algebra) is a generator since it represents the forgetful functor $\Meas \to \Set$. - - property: cogenerator - proof: 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$. - - property: well-powered proof: This follows from the fact that monomorphisms are injective in this category. @@ -49,13 +46,18 @@ satisfied_properties: - property: regular subobject classifier proof: The set $\{0,1\}$ with the trivial $\sigma$-algebra is a regular subobject classifier since measurable maps $X \to \{0,1\}$ correspond to subsets of $X$. + - 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$. + + 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 set. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that $f \circ {-} : \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. + + Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$. + unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: balanced - proof: Take a set $X$ with two different $\sigma$-algebras $\A \subset \B$ (for example, $\A = \{\varnothing,X\}$ and $\B = P(X)$ when $X$ has at least $2$ elements), then the identity map $(X,\B) \to (X,\A)$ provides a counterexample. - - property: cartesian filtered colimits proof: See MSE/5027218. @@ -68,6 +70,16 @@ unsatisfied_properties: - property: regular proof: A proof can be found here. + - property: extremal generating set + proof: >- + The proof is similar to the one for $\Top$. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$. + + Now, suppose $S$ is a set of measurable spaces, and let $\kappa$ be an uncountable regular cardinal greater than $\card(G)$ for each $G \in S$. We claim that the bijective measurable map + $$(\kappa+1, M_\kappa') \to (\kappa+1, \M_\kappa), \, \alpha \mapsto \alpha,$$ + which is not an isomorphism, induces a bijection + $$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$ + for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. + special_objects: initial object: description: empty set with the unique $\sigma$-algebra diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index c6d342cc..c1b63ead 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -22,12 +22,6 @@ satisfied_properties: - property: strict initial object proof: The empty metric space is initial and clearly strict. - - property: generator - proof: The one-point metric space is a generator since it represents the forgetful functor $\Met \to \Set$. - - - property: cogenerator - proof: 'We claim that $\IR$ with the usual metric is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR$. This applies in particular to $f(x) \coloneqq d(a,x)$ and shows that $0=d(a,a)=d(a,b)$, so that $a=b$.' - - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). @@ -65,6 +59,43 @@ satisfied_properties: - property: well-copowered 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: >- + 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$, then $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*} + d(x_1, x_2) &= d(\psi(0), \psi(\varepsilon)) \\ + & \le d(0, \varepsilon) \\ + & = \varepsilon \\ + & = d(f(x_1), f(x_2)) \\ + & \le d(x_1, x_2). + \end{align*}$$ + This shows that $f$ is isometric. + + - property: extremal cogenerator + # Note: $\IR$ is not an extremal cogenerator. This is because for example the non-isomorphism $(0, 1) \hookrightarrow [0, 1]$ induces a bijection $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$. To see this, suppose we have a non-expansive map $f : (0, 1) \to \IR$. Then since $f$ is uniformly continuous in particular, it is well known that $\lim_{x\to 0^+} f(x)$ and $\lim_{x\to 1^-} f(x)$ both exist and are finite. If we extend $f$ with these values at 0 and 1 respectively, then it is straightforward to check that the resulting function is still non-expansive. This shows that $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is surjective; and since $(0, 1) \hookrightarrow [0, 1]$ is an epimorphism, $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is also injective. (The same proof also shows that $\IR_{\ge 0}$ is not an extremal cogenerator.) + proof: >- + We claim that $\IR_+$ (where $0 \notin \IR+$) with metric inherited from the usual metric on $\IR$ is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR_+$. This applies in particular to $f(x) \coloneqq d(a,x)+1$ and shows that $1=d(a,a)+1=d(a,b)+1$, so that $a=b$. + + In fact, $\IR_+$ is an extremal cogenerator. To see this, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that ${-} \circ f : \Hom(Y, \IR_+) \to \Hom(X, \IR_+)$ is a bijection. First of all, since ${-} \circ f$ is injective and $\IR_+$ is a cogenerator, $f$ is an epimorphism, so it has dense image (see below). Now for each $x \in X$, we have a non-expansive map + $$\varphi : X \to \IR_+, \,x' \mapsto d(x, x') + 1.$$ + By the assumption, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. Therefore, + $$\begin{align*} + d(x, x') &= |d(x, x') - d(x, x)| \\ + & = |\varphi(x') - \varphi(x)| \\ + & = |\psi(f(x')) - \psi(f(x))| \\ + & \le d(f(x), f(x')) \\ + & \le d(x,x'). + \end{align*}$$ + This shows that $f$ is isometric, which in particular implies $f$ is injective on underlying sets. + + It remains to show $f$ is surjective on underlying sets. To see this, suppose to the contrary that we have $y \in Y \setminus f(X)$. Then we have a non-expansive map + $$\varphi : X \to \IR_+,\, x \mapsto d(y, f(x)).$$ + By the assumption on $f$, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. However, since $\psi$ (seen as a function with codomain $\IR$) and $d(y, {-})$ are two continuous functions $Y \to \IR$ which agree on the dense subset $f(X)$, they must be the same function. Thus, $\psi(y) = d(y, y) = 0$, giving a contradiction. + - property: ℵ₁-accessible proof: >- For $\alpha=n$ or $\alpha=\infty$, let $I_\alpha$ denote the metric space (with $\infty$ allowed) consisting of exactly two points at distance $\alpha$. diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 69df4746..ac174589 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -32,12 +32,6 @@ satisfied_properties: proof: See MSE/5004389. check_redundancy: false - - property: generator - proof: The one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$. - - - property: cogenerator - proof: The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator. - - property: well-powered proof: This follows easily from the fact that monomorphisms are injective in this category. @@ -50,6 +44,29 @@ satisfied_properties: - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_c$.' + - 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.' + + - property: extremal cogenerator + proof: >- + The space $\IR$ with the usual metric is a cogenerator. To see this, suppose we have $x, y \in X$ with $f(x) = f(y)$ for each continuous $f : X \to \IR$. In particular, this folds for $f(z) \coloneqq d(x, z)$, implying that + $$d(x, y) = f(y) = f(x) = d(x, x) = 0,$$ + so $x = y$. + + In fact, $\IR$ is an extremal cogenerator. To see this, suppose $f : X \to Y$ is a continuous function of metric spaces such that ${-} \circ f : \Hom(Y, \IR) \to \Hom(X, \IR)$ is a bijection. We first show that $f$ is injective on the underlying sets. Thus, suppose we have $x_1, x_2 \in X$ with $f(x_1) = f(x_2)$. Then the function $d(x_1, {-}) : X \to \IR$ is continuous, so there exists a continuous function $\varphi : Y \to \IR$ such that $d(x_1, x) = \varphi(f(x))$ for each $x \in X$. In particular, + $$d(x_1, x_2) = \varphi(f(x_2)) = \varphi(f(x_1)) = d(x_1, x_1) = 0,$$ + so $x_1 = x_2$. + + Now, the fact that ${-} \circ f$ is a bijection, and $\IR$ is a cogenerator, implies that $f$ is an epimorphism, i.e. its image is dense in $Y$. We claim that in fact $f$ is surjective on underlying sets. Suppose, for the sake of contradiction, that we had $y \in Y \setminus \im(f)$. Then we can define a continuous function + $$X \to \IR, \, x \mapsto \frac{1}{d(f(x), y)}.$$ + By the assumption on $f$, there exists continuous $\varphi : Y \to \IR$ such that + $$\varphi(f(x)) = \frac{1}{d(f(x), y)}$$ + for each $x \in X$. However, since $f$ has dense image, there is a sequence $(x_n)_{n=1}^\infty$ of points of $X$ such that $f(x_n) \to y$, while + $$\lim_{n\to \infty} \varphi(f(x_n)) = \lim_{n\to \infty} \frac{1}{d(f(x_n), y)} = \infty.$$ + This makes it impossible for $\varphi$ to be continuous at $y$, giving a contradiction. + + Finally, since we have shown $f$ is bijective on underlying sets, to show $f$ is a homeomorphism, it suffices to show that $f$ is closed. Thus, let $F \subseteq X$ be closed. Then $d({-}, F) : X \to \IR$ is a continuous function, so there exists $\varphi : Y \to \IR$ such that $\varphi(f(x)) = d(x, F)$ for each $x\in X$. That implies that $f_*(F) = \{ y\in Y : \varphi(y) = 0 \}$ is closed. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index f77f1e5b..af097ab0 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -17,12 +17,6 @@ satisfied_properties: - property: locally small proof: There is a forgetful functor $\Met_{\infty} \to \Set$ and $\Set$ is locally small. - - property: generator - proof: The singleton metric space $1$ is a generator, since morphisms $1 \to X$ correspond to the elements of $X$. - - - property: cogenerator - proof: 'The proof is similar to $\Met$, a cogenerator is given by $\IR \cup \{\infty\}$ with the metric in which $d(a,\infty)=\infty$ for $a \in \IR$. Then one checks that the maps $d(a,-) : X \to \IR \cup \{\infty\}$ are non-expansive and finishes as for $\Met$.' - - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). @@ -35,6 +29,12 @@ satisfied_properties: - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the restricted metric. If $f$ is non-expansive, each $f_i$ is non-expansive, and for $x_i \in Y_i$ and $i \neq j$ we have $d_Y(x_i,x_j) \geq d_X(f(x_i),f(x_j)) = \infty$, so that $Y = \coprod_i Y_i$ holds as metric spaces.' + - property: extremal generator + proof: A similar proof to the one for $\Met$ shows that $[0, \infty]$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\Met_{\infty}$. + + - property: extremal cogenerator + proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric extending the usual metric on $\IR_+$ by defining $d(a,\infty) \coloneqq \infty$ for $a \in \IR_+$. Then one checks that the maps $1 + d(a,{-}) : X \to \IR_+ \cup \{\infty\}$ (assigning the value $\infty$ if $d(a,x) = \infty$) are non-expansive and finishes as for $\Met$.' + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index b4099c13..c5548cd5 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -4,7 +4,7 @@ notation: $\Mono$ objects: >- pairs $(X, X')$ where $X$ is a set and $X' \subseteq X$ is a subset morphisms: >- - a morphism $(X, X') \to (Y, Y')$ is a function $f : X \to Y$ such that $f(X') \subseteq Y'$ + a morphism $(X, X') \to (Y, Y')$ is a function $f : X \to Y$ such that $f_*(X') \subseteq Y'$, or equivalently $X' \subseteq f^*(Y')$ description: >- This is equivalent to the full subcategory of objects $(X, Y, f)$ of $\Set^{\rightarrow}$ where $f : X \to Y$ is an injective function, i.e. a monomorphism. This explains our notation. nlab_link: https://ncatlab.org/nlab/show/M-category#def @@ -29,33 +29,39 @@ satisfied_properties: proof: >- The object $(1, 0)$ is a generator. This is because it represents the functor taking an object $(X, X')$ to $X$, and taking a morphism $f : (X, X') \to (Y, Y')$ to the function $f : X \to Y$. - - property: cogenerator - proof: >- - Consider the forgetful functor $U : \Mono \to \Set$, $(X, X') \mapsto X$. This has right adjoint $R : \Set \to \Mono$, $X \mapsto (X, X)$. Therefore, by the dual of Lemma 9 here, $R$ preserves cogenerators; and in particular, since $\Set$ has a cogenerator, so does $\Mono$. - - property: complete proof: >- The component-wise limit gives a pair of a set and a subset, and this pair forms the limit in $\Mono$. - More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with limit cone $p_i : \lim_{i\in\I} X_i \to X_i$ in $\Set$. Then the limit in $\Mono$ is $(\lim_{i\in\I} X_i, \bigcap_{i\in\I} p_i^{-1}(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly initial set of objects of $\I$.) + More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with limit cone $p_i : \lim_{i\in\I} X_i \to X_i$ in $\Set$. Then the limit in $\Mono$ is $(\lim_{i\in\I} X_i, \bigcap_{i\in\I} p_i^*(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly initial set of objects of $\I$.) check_redundancy: false - property: cocomplete proof: >- We have that $\Mono$ is a reflective subcategory of $\Set^{\rightarrow}$, with the reflector taking a function $f : X \to Y$ to the pair $(Y, \im(f))$. Therefore, the result follows from the fact that $\Set^{\rightarrow}$ is cocomplete. - More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with colimit cone $c_i : X_i \to \colim_{i\in\I} X_i$ in $\Set$. Then the colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} c_i(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly terminal set of objects of $\I$.) + More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with colimit cone $c_i : X_i \to \colim_{i\in\I} X_i$ in $\Set$. Then the colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} (c_i)_*(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly terminal set of objects of $\I$.) check_redundancy: false - property: disjoint coproducts proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts. + - property: extremal cogenerator + proof: >- + Consider the forgetful functor $U : \Mono \to \Set$, $(X, X') \mapsto X$. This has right adjoint $R : \Set \to \Mono$, $X \mapsto (X, X)$. Therefore, by the dual of Lemma 9 here, $R$ preserves cogenerators; and in particular, since $\Set$ has a cogenerator, so does $\Mono$. In other words, $(\{0,1\}, \{0,1\})$ is a cogenerator of $\Mono$. + + We now claim that adding $(\{0,1\}, \{1\})$ gives an extremal cogenerating set. To see this, suppose we have $f : (X, X') \to (Y, Y')$ such that ${-} \circ f$ induces bijections of morphisms both to $(\{0,1\}, \{0,1\})$ and to $(\{0,1\}, \{0\})$. Then since the first object represents the functor taking $(X, X')$ to $\Hom_{\Set}(X, \{ 0, 1 \})$, and $\{ 0, 1 \}$ is an extremal cogenerator of $\Set$, the bijection of morphisms for the first object implies that $f$ is a bijection $X \to Y$. On the other hand, the second object represents the functor taking $(X, X')$ to the collection of subsets of $X$ which contain $X'$; and under the Yoneda embedding, the monomorphism $(\{0,1\}, \{1\}) \hookrightarrow (\{0,1\}, \{0,1\})$ corresponds to the natural inclusion $\{ S\in P(X) : X' \subseteq S \} \hookrightarrow P(X)$. Therefore, if $f$ also induces a bijection of morphisms to the second object, then in particular there is a set $S$ with $Y' \subseteq S \subseteq Y$ with $f^*(S) = X'$. However, since $f$ is bijective, we also have $f^*(f_*(X')) = X'$ and $f^* : P(Y) \to P(X)$ is bijective, so $S = f_*(X')$. In other words, + $$Y' \subseteq S = f_*(X') \subseteq Y',$$ + so $f_*(X') = Y'$. + + Finally, since the collection of two objects is strongly connected (e.g. using the constant maps with image 1 in both directions), this result implies that their product is an extremal cogenerator. + - property: locally cartesian closed proof: >- - For any object $(S, S')$ of $\Mono$, we can view objects of the slice $\Mono / (S, S')$ as indexed families $(\bigsqcup_{s\in S} X_s, \bigsqcup_{s\in S'} X'_s)$ where $X'_s \subseteq X_s$ for each $s\in S'$. Given any two such objects $X = (\bigsqcup_{s\in S} X_s, \bigsqcup_{s\in S'} X'_s)$ and $Y = (\bigsqcup_{s\in S} Y_s, \bigsqcup_{s\in S'} Y'_s)$, observe that $\Hom_{\Mono / (S, S')}(X, Y)$ is equivalent to the tuples of functions $f \in \prod_{s\in S} \Hom_{\Set}(X_s, Y_s)$ such that whenever $s \in S'$, then $f_s(X_s ') \subseteq Y_s '$. We claim that $\Mono$ has a relative exponential given by + For any object $(S, S')$ of $\Mono$, we can view objects of the slice $\Mono / (S, S')$ as indexed families $(\bigsqcup_{s\in S} X_s, \bigsqcup_{s\in S'} X'_s)$ where $X'_s \subseteq X_s$ for each $s\in S'$. Given any two such objects $X = (\bigsqcup_{s\in S} X_s, \bigsqcup_{s\in S'} X'_s)$ and $Y = (\bigsqcup_{s\in S} Y_s, \bigsqcup_{s\in S'} Y'_s)$, observe that $\Hom_{\Mono / (S, S')}(X, Y)$ is equivalent to the tuples of functions $f \in \prod_{s\in S} \Hom_{\Set}(X_s, Y_s)$ such that whenever $s \in S'$, then $(f_s)_*(X_s ') \subseteq Y_s '$. We claim that $\Mono$ has a relative exponential given by $$[X, Y]_S \coloneqq \left(\bigsqcup_{s\in S} [X_s, Y_s], \bigsqcup_{s\in S'} [X_s, Y_s]' \right)$$ where - $$[X_s, Y_s]' \coloneqq \{ f \in [X_s, Y_s] : f(X_s ') \subseteq Y_s ' \}.$$ + $$[X_s, Y_s]' \coloneqq \{ f \in [X_s, Y_s] : f_*(X_s ') \subseteq Y_s ' \}.$$ To check that this works, suppose we have a test object $U = (\bigsqcup_{s\in S} U_s, \bigsqcup_{s\in S'} U_s ')$. Then $U \times_S X = (\bigsqcup_{s\in S} (U_s \times X_s), \bigsqcup_{s\in S'} (U_s ' \times X_s '))$. Given a morphism $g : U \times_S X \to Y$ in $\Mono / (S, S')$, we define the corresponding morphism $h : U \to [X, Y]_S$ to have $s$-component given by $u \mapsto (x \mapsto g_s(u, x))$. To check this is a valid morphism in $\Mono / (S, S')$, suppose that $s \in S'$ and $u \in U_s '$; then for every $x \in X_s '$, we have $(u, x) \in U_s ' \times X_s '$, so $g_s(u, x) \in Y_s '$. This shows that $h_s(u) \in [X_s, Y_s]'$. Conversely, given a morphism $h : U \to [X, Y]_S$ in $\Mono / (S, S')$, we define the corresponding morphism $g : U \times_S X \to Y$ to have $s$-component given by $(u, x) \mapsto h_s(u)(x)$. To check this is a valid morphism in $\Mono / (S, S')$, suppose that $s \in S'$ and $(u, x) \in U_s ' \times X_s '$; then $u \in U_s '$ so $h_s(u) \in [X_s, Y_s]'$. Furthermore, $x \in X_s '$, so $h_s(u)(x) \in Y_s '$. It is easy to check these give inverse operations which are natural in $U$ (in fact, the details are exactly the same as the details of an explicit proof that $\Set$ is locally cartesian closed), completing the proof. @@ -71,7 +77,7 @@ satisfied_properties: @V \id VV @VV f VV \\ X @>> f > Y. \end{CD}$$ - Alternately, we already know $\Mono$ is cocomplete. We claim that both $(1, 0)$ and $(1, 1)$ are finitely presentable objects of $\Mono$. For the first, $(1, 0)$ represents the forgetful functor $(X, X') \mapsto X$; and this functor has a right adjoint $X \mapsto (X, X)$ so it preserves filtered colimits (in fact all colimits). For the second, $(1, 1)$ represents the functor $(X, X') \mapsto X'$. Now by the previous description of colimits, for a filtered diagram $((X_i, X_i'))_{i\in\I}$, first form the filtered colimit of $X_i$ in $\Set$ with cocone $c_i : X_i \to \colim_{i\in\I} X_i$. Then the filtered colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} c_i(X_i'))$. This makes it easy to see that the canonical function + Alternately, we already know $\Mono$ is cocomplete. We claim that both $(1, 0)$ and $(1, 1)$ are finitely presentable objects of $\Mono$. For the first, $(1, 0)$ represents the forgetful functor $(X, X') \mapsto X$; and this functor has a right adjoint $X \mapsto (X, X)$ so it preserves filtered colimits (in fact all colimits). For the second, $(1, 1)$ represents the functor $(X, X') \mapsto X'$. Now by the previous description of colimits, for a filtered diagram $((X_i, X_i'))_{i\in\I}$, first form the filtered colimit of $X_i$ in $\Set$ with cocone $c_i : X_i \to \colim_{i\in\I} X_i$. Then the filtered colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} (c_i)_*(X_i'))$. This makes it easy to see that the canonical function $$\colim_{i\in\I} \Hom((1,1), (X_i,X_i')) \to \Hom((1,1), \colim_{i\in\I} (X_i,X_i'))$$ is surjective. To see it is injective, use the fact that the unique morphism $(1, 0) \to (1, 1)$ is an epimorphism (see below), and we have already seen that the corresponding function for $(1,0)$ is injective. @@ -79,7 +85,7 @@ satisfied_properties: - property: co-Malcev proof: >- - Suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is a surjective function. Since $\Set$ is co-Malcev, it follows that $E \cong X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is an element of $E$ and hence is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $x = r(i_1(x)) \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. + Suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is a surjective function. Since $\Set$ is co-Malcev, it follows that $E \cong X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = (i_1)_*(X') \cup (i_2)_*(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, (i_1)_*(X') \cup (i_2)_*(X')) \to (E, E')$ induced by $p$, we must have $(i_1)_*(X') \cup (i_2)_*(X') \subseteq E'$. On the other hand, any element of $E'$ is an element of $E$ and hence is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $x = r(i_1(x)) \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. - property: effective cocongruences proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.' @@ -88,13 +94,18 @@ unsatisfied_properties: - property: skeletal proof: Consider the objects $(X, X)$ and $(Y, Y)$ for isomorphic but non-equal sets $X$ and $Y$. - - property: balanced - proof: The unique morphism from $(1, 0)$ to $(1, 1)$ is both a monomorphism and an epimorphism, but not an isomorphism (see descriptions below). - - 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 \Mono$ which sends a set $X$ to the pair $(X, X)$. + - property: extremal generator + proof: >- + Let $(G, G')$ be any object. Then if $G'$ is empty, the unique morphism $(1, 0) \to (1, 1)$ induces a bijection + $$\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (1, 1))$$ + because both sides are singletons. On the other hand, if $G'$ is non-empty, then for either choice of morphism $(1, 0) \to (2, 0)$, the induced map + $$\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (2, 0))$$ + is bijective because both sides are empty. Thus, in either case, $(G,G')$ is not an extremal generator. + special_objects: initial object: description: $(0, 0)$ @@ -108,7 +119,7 @@ special_objects: special_morphisms: isomorphisms: description: >- - morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a bijection between $X$ and $Y$, and $f(X') = Y'$ + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a bijection between $X$ and $Y$, and $f_*(X') = Y'$ proof: This is easy. monomorphisms: description: >- @@ -122,19 +133,19 @@ special_morphisms: For the non-trivial direction, use the fact that the forgetful functor $\Mono \to \Set$, $(X, X') \mapsto X$, has a right adjoint given by $X \mapsto (X, X)$. Therefore, the forgetful functor preserves epimorphisms; so if $f : (X, X') \to (Y, Y')$ is an epimorphism in $\Mono$, then $f : X \to Y$ is an epimorphism in $\Set$ and therefore surjective. regular monomorphisms: description: >- - morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$, and $f^{-1}(Y') = X'$ (in particular, if $f : X \to Y$ is an inclusion map, then this is equivalent to $X' = X \cap Y'$) + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$, and $f^*(Y') = X'$ (in particular, if $f : X \to Y$ is an inclusion map, then this is equivalent to $X' = X \cap Y'$) proof: >- - To show any regular monomorphism satisfies this condition, suppose we have a parallel pair $g, h : (Y, Y') \rightrightarrows (Z, Z')$. To form the equalizer in $\Mono$, first we form the equalizer $f : X \hookrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of limits in the proof of completeness above, the equalizer in $\Mono$ is $(X, f^{-1}(Y'))$. Thus, we see that $f^{-1}(Y') = X'$. + To show any regular monomorphism satisfies this condition, suppose we have a parallel pair $g, h : (Y, Y') \rightrightarrows (Z, Z')$. To form the equalizer in $\Mono$, first we form the equalizer $f : X \hookrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of limits in the proof of completeness above, the equalizer in $\Mono$ is $(X, f^*(Y'))$. Thus, we see that $f^*(Y') = X'$. For the other direction, suppose we are given a morphism $f : (X, X') \to (Y, Y')$ satisfying this condition. We can then construct an equalizer diagram $$\begin{CD} (X, X') @> f >> (Y, Y') @> \chi_{f(X)} > \top_Y > (\{ \top, \bot \}, \{ \top, \bot \}). \end{CD}$$ - Here $\chi_{f(X)} : Y \to \{ \top, \bot \}$ is the characteristic function of the subset $f(X) \subseteq Y$, and $\top_Y$ is the constant function on $Y$ with value $\top$. + Here $\chi_{\im(f)} : Y \to \{ \top, \bot \}$ is the characteristic function of the subset $\im(f) \subseteq Y$, and $\top_Y$ is the constant function on $Y$ with value $\top$. regular epimorphisms: description: >- - morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$, and $f(X') = Y'$ + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$, and $f_*(X') = Y'$ proof: >- - To show any regular epimorphism satisfies this condition, suppose we have a parallel pair $g, h : (Z, Z') \rightrightarrows (X, X')$. To form the coequalizer in $\Mono$, first we form the coequalizer $f : X \twoheadrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of colimits in the proof of cocompleteness above, the coequalizer in $\Mono$ is $(Y, f(X'))$. Thus, we see that $f(X') = Y'$. + To show any regular epimorphism satisfies this condition, suppose we have a parallel pair $g, h : (Z, Z') \rightrightarrows (X, X')$. To form the coequalizer in $\Mono$, first we form the coequalizer $f : X \twoheadrightarrow Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of colimits in the proof of cocompleteness above, the coequalizer in $\Mono$ is $(Y, f_*(X'))$. Thus, we see that $f_*(X') = Y'$. - To show any morphism $f : (X, X') \to (Y, Y')$ satisfying this condition is a regular epimorphism, note that the kernel pair of $f$ can be computed component-wise. Therefore, in general the coequalizer of the kernel pair of $f$ is $(f(X), f(X'))$; and with the given assumptions on $f$, this is isomorphic to $(Y, Y')$. + To show any morphism $f : (X, X') \to (Y, Y')$ satisfying this condition is a regular epimorphism, note that the kernel pair of $f$ can be computed component-wise. Therefore, in general the coequalizer of the kernel pair of $f$ is $(\im(f), f_*(X'))$; and with the given assumptions on $f$, this is isomorphic to $(Y, Y')$. diff --git a/database/data/categories/N.yaml b/database/data/categories/N.yaml index bf1af687..45add20b 100644 --- a/database/data/categories/N.yaml +++ b/database/data/categories/N.yaml @@ -45,6 +45,12 @@ unsatisfied_properties: - property: countable coproducts proof: The numbers $0,1,2,\dotsc$ have no supremum, i.e. no coproduct. + - property: extremal generator + proof: The poset $(\IN,\leq)$ has infinitely many non-minimal elements $1, 2, \dotsc$. Therefore, by the corollary here, an extremal generator cannot exist. + + - property: extremal cogenerator + proof: The poset $\IN$ has infinitely many non-maximal elements $0, 1, 2, \dotsc$. Therefore, by the corollary here, an extremal generator cannot exist. + special_objects: initial object: description: $0$ diff --git a/database/data/categories/N_oo.yaml b/database/data/categories/N_oo.yaml index 7303fcb0..ecd3999c 100644 --- a/database/data/categories/N_oo.yaml +++ b/database/data/categories/N_oo.yaml @@ -43,8 +43,11 @@ unsatisfied_properties: - property: inverse proof: Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$. - - property: finitary algebraic - proof: This follows from this lemma. + - property: extremal generator + proof: The poset $\IN_\infty$ has infinitely many non-minimal elements $1, 2, \dotsc, \infty$. Therefore, by the corollary here, an extremal generator cannot exist. + + - property: extremal cogenerator + proof: The poset $\IN_\infty$ has infinitely many non-maximal elements $0, 1, 2, \dotsc$. Therefore, by the corollary here, an extremal cogenerator cannot exist. special_objects: initial object: diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 9ceac19e..2045bdaf 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -16,12 +16,6 @@ satisfied_properties: - property: locally small proof: There is a forgetful functor $\PMet \to \Set$ and $\Set$ is locally small. - - property: generator - proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. - - - property: cogenerator - proof: The set $\{0,1\}$ equipped with the pseudo-metric $d(0,1)=0$ is a cogenerator since every map into is automatically non-expansive and since $\{0,1\}$ is a cogenerator in $\Set$. - - property: strict initial object proof: The empty (pseudo-)metric space is initial and clearly strict. @@ -59,6 +53,32 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: The proof is identical to the one for $\Met$. + - property: extremal generator + 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$, then $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*} + d(x_1, x_2) &= d(\psi(0'), \psi(\varepsilon)) \\ + & \le d(0', \varepsilon) \\ + & = \varepsilon \\ + & = d(f(x_1), f(x_2)) \\ + & \le d(x_1, x_2). + \end{align*}$$ + This shows that $f$ is isometric. + + - property: extremal cogenerator + proof: >- + Let $Q$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric extending the usual metric on $\IR_{\ge 0}$ with $d(x, 0') = x$ for $x \in \IR_{\ge 0}$. Then $Q$ is an extremal cogenerator. + + First, to see $Q$ is a cogenerator, note that the subspace $\{ 0, 0' \}$ is a cogenerator since every map into it is automatically non-expansive and since $\{0,0'\}$ is a cogenerator in $\Set$. Therefore, since $\{ 0, 0' \} \hookrightarrow Q$ is a monomorphism, we have that $Q$ is also a cogenerator. + + To see $Q$ is in fact an extremal cogenerator, suppose we have a non-expansive map $f : X \to Y$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection. First of all, any function $Y \to Q$ which factors through $\{ 0, 0' \}$ is automatically non-expansive; and the injectivity of $f^*$ on such maps implies that $f$ is surjective on underlying sets, since $\{ 0, 0' \}$ is a cogenerator of $\Set$. From this, we can conclude that $f^*$ in fact induces a bijection on the functions $Y\to Q$ and $X\to Q$, respectively, which factor through $\{ 0, 0' \}$. Since $\{ 0, 0' \}$ is in fact an extremal cogenerator of $\Set$, we conclude that in fact, $f$ is a bijection on underlying sets. + + From here, the proof that $f$ is isometric is similar to the one for $\Met$, using the fact that $d(x, {-}) : X \to \IR_{\ge 0} \hookrightarrow Q$ induces a non-expansive map $Y \to Q$. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index a8cfd553..cf87efac 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -27,18 +27,21 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty poset is weakly terminal (by using constant maps). - - property: generator - proof: The singleton poset $1$ is a generator, since morphisms $1 \to P$ correspond to the elements of $P$. - - - property: cogenerator - proof: 'We prove that the poset $\{0 < 1\}$ is a cogenerator: Let $P$ be a poset and $a,b \in P$ be two elements such that $f(a) = f(b)$ for all order-preserving maps $f : P \to \{0 < 1 \}$. This means that $a$ and $b$ lie in the same upper sets. In particular, $b$ lies in the upper set generated by $a$, meaning $a \leq b$, and similarly we deduce $b \leq a$. Thus, $a = b$.' - - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.' - property: coregular proof: See MSE/5130295. + - property: extremal generator + proof: We have that $\{0<1\}$ is an extremal generator even in $\PreOrd$. Now apply Lemma 10 here. + + - property: extremal cogenerator + proof: >- + We prove that the poset $\{0 < 1\}$ is an extremal cogenerator. First, to prove it is a cogenerator: Let $P$ be a poset and $a,b \in P$ be two elements such that $f(a) = f(b)$ for all order-preserving maps $f : P \to \{0 < 1 \}$. This means that $a$ and $b$ lie in the same upper sets. In particular, $b$ lies in the upper set generated by $a$, meaning $a \leq b$, and similarly we deduce $b \leq a$. Thus, $a = b$. + + Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that $f$ induces a bijection of upper sets implies that $f$ is also injective on the underlying sets, and also that $f(a_1) \le f(a_2)$ implies $a_1 \le a_2$. Therefore, $f$ is an isomorphism. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 2bd97f7b..7799b52b 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -23,12 +23,6 @@ satisfied_properties: - property: cartesian closed proof: For preordered sets $P,Q$ we endow $\Hom(P,Q)$ with the preorder in which $f \leq g$ holds iff $f(p) \leq g(p)$ for all $p \in P$. The universal evaluation map is $\Hom(P,Q) \times P \to Q$, $(f,p) \mapsto f(p)$, it is order-preserving, and it satisfies the universal property. - - property: generator - proof: The singleton preordered set $1$ is a generator, since morphisms $1 \to P$ correspond to the elements of $P$. - - - property: cogenerator - proof: Endow the set $\{ 0,1 \}$ with the preorder $0 \leq 1$, $1 \leq 0$ (which is not a partial order). Then every map $P \to \{0,1\}$ is order-preserving. Now the claim follows since the set $\{ 0,1 \}$ is a cogenerator in $\Set$. - - property: semi-strongly connected proof: Every non-empty preordered set is weakly terminal (by using constant maps). @@ -41,6 +35,17 @@ satisfied_properties: - property: regular subobject classifier 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.' + + - property: extremal cogenerator + proof: >- + Endow the set $\{ 0,1 \}$ with the preorder $0 \leq 1$, $1 \leq 0$ (which is not a partial order), and call this object $\{0,1\}_c$. Then every map $P \to \{0,1\}$ is order-preserving. Therefore, $\{0,1\}_c$ represents the functor taking $(P, \le)$ to the power set of $P$. Now since the set $\{ 0,1 \}$ is a cogenerator in $\Set$, it follows that $\{0,1\}_c$ is a cogenerator of $\PreOrd$. + + We now claim that $\{0,1\}_c$ together with $\{ 0 < 1 \}$ form an extremal cogenerating set. Thus, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f$ induces a bijection for morphisms both to $\{0,1\}_c$ and to $\{ 0 < 1 \}$. Then since $\{0,1\}$ is an extremal cogenerator in $\Set$, it follows that $f$ is 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 we can define an increasing function $\varphi : P \to \{0<1\}$ which sends $p \mapsto 1$ if $p_1 \le p$, and $p \mapsto 0$ otherwise. By the assumption on $f$, there is an increasing function $\psi : Q \to \{0<1\}$ such that $\psi \circ f = \varphi$. Since $1 = \psi(f(p_1)) \le \psi(f(p_2))$, it follows that $\varphi(p_2) = 1$, so $p_1 \le p_2$. We conclude that $f$ is an isomorphism. + + Finally, by this result, we can conclude that the product of $\{0,1\}_c$ and $\{0<1\}$ is an extremal cogenerator. + unsatisfied_properties: - property: regular proof: See Example 3.14 at the nLab. diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 6c3bde0f..32ac39f3 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -32,6 +32,14 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty set is weakly terminal (by using constant maps). + - property: extremal generator + proof: The one-point set is an extremal generator since it represents the identity functor $\id_{\Set}$ which is certainly faithful and conservative. + check_redundancy: false + + - property: extremal cogenerator + proof: The two-point set is an extremal cogenerator since it represents the contravariant power set functor $\Set^{\op} \to \Set$ which is faithful and conservative (see contravariant power set functor). + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index ae626057..68501ef3 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -32,11 +32,11 @@ satisfied_properties: - property: subobject classifier proof: This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide. - - property: generator - proof: The one-point set is clearly a generator. + - property: extremal generator + proof: The one-point set is an extremal generator even in $\Set$. Now apply Lemma 10 here. - - property: cogenerator - proof: The two-point set is a cogenerator in $\Set$, hence also in $\Set_\c$. + - property: extremal cogenerator + proof: The two-point set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. - property: semi-strongly connected proof: This is because the larger category $\Set$ has this property. diff --git a/database/data/categories/Set_f.yaml b/database/data/categories/Set_f.yaml index 0f17ebb2..3e709a78 100644 --- a/database/data/categories/Set_f.yaml +++ b/database/data/categories/Set_f.yaml @@ -17,11 +17,8 @@ satisfied_properties: - property: locally small proof: There is a forgetful functor $\Set_\f \to \Set$ and $\Set$ is locally small. - - property: generator - proof: The singleton set (which is not terminal) is a generator as it represents the forgetful functor $\Set_\f \to \Set$. - - - property: cogenerator - proof: 'The set $\{0,1\}$ is a cogenerator in $\Set_\f$: Assume that $f,g : X \rightrightarrows Y$ are two finite-to-one maps such that $h \circ f = h \circ g$ for all finite-to-one maps $h : Y \to \{0,1\}$. This exactly means $f^*(A)=g^*(A)$ for all finite subsets $A \subseteq Y$. Applying this to $A = \{f(x)\}$ for $x \in X$ we get $x \in f^*(\{f(x)\}) = g^*(\{f(x)\})$, so that $g(x) = f(x)$.' + - property: extremal generator + proof: The singleton set (which is not terminal) is an extremal generator as it represents the forgetful functor $\Set_\f \to \Set$ which is faithful and conservative. - property: semi-strongly connected proof: From set theory it is known that for all sets $X,Y$ there is an injective map $X \to Y$ or an injective map $Y \to X$, and injective maps are finite-to-one. @@ -78,8 +75,8 @@ unsatisfied_properties: - property: sequential limits 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_\f$, 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: coaccessible - proof: 'Assume that $\Set_\f$ is $\lambda$-coaccessible for some regular cardinal. Then there is an infinite cardinal $\kappa$ such that every $X \in \Set_\f$ is a $\lambda$-cofiltered limit of sets of cardinality $\leq \kappa$. In particular, since every $\lambda$-cofiltered category is non-empty, there is some set $Y$ of cardinality $\leq \kappa$ that admits a morphism $f : X \to Y$ in $\Set_f$. Since $f$ has finite fibers, this implies $\card(X) \leq \card(Y) \cdot \aleph_0 \leq \kappa$. Since $X$ was an arbitrary set, this is a contradiction.' + - property: cogenerating set + proof: 'Suppose that $S$ is a set of objects of $\Set_\f$, 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$.' special_objects: initial object: diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 353a88b2..3d88de7a 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -16,12 +16,12 @@ satisfied_properties: - property: locally small proof: There is a forgetful functor $\Setne \to \Set$ and $\Set$ is locally small. - - property: generator - proof: The one-point set is clearly a generator. + - property: extremal generator + proof: The one-point set is an extremal generator even in $\Set$. Now use Lemma 10 here. check_redundancy: false - - property: cogenerator - proof: The two-point set is a cogenerator, this follows as for $\Set$. + - property: extremal cogenerator + proof: The two-point set is an extremal cogenerator even in $\Set$. Now use Lemma 10 here. - property: products proof: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index c4d961e2..a48168fe 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -38,11 +38,8 @@ satisfied_properties: - property: generator proof: The one-point space is a generator since it represents the forgetful functor $\Top \to \Set$. - - property: cogenerator - proof: It is easily checked that the indiscrete two-point space is a cogenerator. - - property: infinitary extensive - proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the subspace topology. If $f$ is continuous, each $Y_i = f^{-1}(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' + proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the subspace topology. If $f$ is continuous, each $Y_i = f^*(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -53,12 +50,19 @@ satisfied_properties: - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. + - property: extremal cogenerator + proof: >- + Using the dual of Lemma 9 here with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of $\Set$, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective. + + Now, by this result, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$. + unsatisfied_properties: - property: skeletal proof: This is trivial. - property: balanced proof: If $X$ is a set, consider the discrete space $X_d$ on $X$ and the indiscrete space $X_i$ on $X$. The identity map $X \to X$ lifts to a continuous map $X_d \to X_i$, which is bijective and therefore both a mono- and an epimorphism, but it is not an isomorphism unless $X$ has at most one element. + check_redundancy: false - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see MSE/1255678.' @@ -66,9 +70,6 @@ unsatisfied_properties: - property: regular proof: See Example 3.14 at the nLab. - - property: accessible - proof: In fact, it does not have any small colimit-dense subcategory by MSE/4097315. For a related result, see MO/288648. - - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' @@ -81,6 +82,12 @@ unsatisfied_properties: - 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.' + - property: extremal generating set + proof: >- + Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating set. + + To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $T := \im(f) \cap \kappa$. Then $T \subseteq \kappa$ and $\card(T) \leq \card(G) < \kappa$. Since $\kappa$ is regular, this implies $\alpha := \sup(T) < \kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$. + special_objects: initial object: description: empty space diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index 5528583d..4c757a43 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -42,9 +42,6 @@ satisfied_properties: - property: generator proof: The discrete space $\{0,1\}$ with base point $0$ is a generator since it represents the forgetful functor $\Top_* \to \Set$. - - property: cogenerator - proof: It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator. - - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ with base point $1$ is a regular subobject classifier since pointed continuous maps $X \to \{0,1\}$ correspond to pointed subsets of $X$ (by taking the fiber of $1$ as usual). @@ -58,7 +55,7 @@ satisfied_properties: proof: >- We continue the proof for $\Set_*$ by showing that the natural bijective map $$\textstyle \alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$$ - is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open. + is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^*(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^*(V_i) \cap \lim_i Y_i)$ is $p_i^*(X \vee V_i)$, hence open. - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. @@ -66,19 +63,19 @@ satisfied_properties: - property: coregular proof: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. + - property: extremal cogenerator + proof: >- + It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator, using the fact that the pointed set $\{0,1\}$ with base point $1$ is a cogenerator of $\Set_*$. If $S$ is the Sierpinski space on $\{0,1\}$, we claim that adding $(S, 0)$ and $(S, 1)$ gives an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. Then $f$ inducing a bijection on maps to $(\{0,1\},1)$ implies that the underlying function of $f$ is bijective. In particular, because $f$ is injective, we see that for $V$ an open subset of $Y$, $f^*(V)$ contains the base point of $X$ if and only if $V$ contains the base point of $Y$. Also, $f$ inducing a bijection on maps to $(S, 1)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets containing the base points, and $f$ inducing a bijection on maps to $(S, 0)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets not containing the base points. From these observations, we can conclude that $f$ is a homeomorphism. + + Now, by this result, we get that the product of these three pointed topological spaces is an extremal cogenerator of $\Top_*$. + unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: balanced - proof: If $X$ is a set with a base point $x_0$, consider the discrete space $X_d$ on $X$ and the indiscrete space $X_i$ on $X$. The identity map $X \to X$ lifts to a continuous map $X_d \to X_i$ preserving $x_0$, which is bijective and therefore both a mono- and an epimorphism, but it is not an isomorphism unless $X = \{x_0\}$. - - property: regular proof: See Example 3.14 at the nLab. The proof also works for pointed spaces (resp. posets) by using the base points $a$ and $0$. - - property: accessible - proof: In fact, it does not have any small colimit-dense subcategory by MSE/4097315. The proof easily adapts to pointed spaces. - - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top_* \to \Top_*$ does not preserve colimits, see MSE/2969372. The counterexample also works for pointed spaces.' @@ -107,6 +104,9 @@ unsatisfied_properties: - 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 \}$.' + - property: extremal generating set + proof: 'The proof is similar to the one for $\Top$: if $S$ is a set of pointed topological spaces and $\kappa$ is an infinite regular cardinal greater than $\card(G)$ for every $G\in S$, we show as before that morphisms from $S$ cannot detect the failure of $(\kappa \sqcup \{ \kappa \}, 0) \to (\kappa + 1, 0)$ to be an isomorphism (where as before, we use the standard order topology on both $\kappa$ and $\kappa + 1$).' + special_objects: initial object: description: singleton space with the unique base point diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 1bc8bd9c..3e90d4fb 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -32,9 +32,6 @@ satisfied_properties: - property: preadditive proof: It is a full subcategory of the preadditive category $\Ab$. - - property: cogenerator - proof: The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. - - property: regular proof: The regular epimorphisms are exactly the surjective homomorphisms (see below), and these are clearly stable under pullbacks. @@ -44,6 +41,18 @@ satisfied_properties: $$P = (B \times C)/\{(i(a),-f(a)): a \in A\}.$$ It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. + - property: extremal cogenerating set + proof: >- + The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. + + We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \text{~prime}\}$ is an extremal cogenerating set, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By equivalent condition (4) in the characterization below of regular monomorphisms, this is equivalent to showing $\alpha$ is injective, and whenever we have $x\in G$ and prime $p$ such that $\alpha(x)$ is $p$-divisible in the product, then $x$ is $p$-divisible in $G$. From the above, including $\IQ$ in $S$ is already sufficient to make $\alpha$ a monomorphism, i.e. an injective homomorphism. + + We will prove the second part of this condition by establishing the contrapositive for each prime $p$; thus, suppose we have $x\in G$ which is not $p$-divisible. Let $\{y_i : i \in I\}$ be a subset of $G$ including $x = y_{i_0}$ whose images in $G / pG$ form a basis for this $\IZ / p \IZ$-vector space. We will now prove by induction that for each $n$, $G / p^n G$ is a free $\IZ / p^n \IZ$-module with basis given by the images of $y_i$. The base case $n=1$ is true by assumption. Now for the inductive step from $n$ to $n+1$, for $g \in G$ we can find $a_i \in \IZ$ (all but finitely many equal to zero) such that $g \in \sum_{i\in I} a_i y_i + p^n G$. Since $G$ is torsion-free, there exists a unique $h$ such that $g = \sum_{i\in I} a_i y_i + p^n h$. Now projecting $h$ into $G / pG$, we can find $b_i \in \IZ$ such that $h \in \sum_{i\in I} b_i y_i + pG$. Hence, $g \in \sum_{i\in I} (a_i + p^n b_i) y_i + p^{n+1} G$. The uniqueness of the coefficients up to congruence modulo $p^{n+1}$ follows from the fact that there are unique choices of $a_i$ with $0 \le a_i < p^n$, and then the $b_i$ are unique up to congruence modulo $p$. + + Now for each $n$, let $\varphi_n : G / p^n G \to \IZ / p^n \IZ$ be the coordinate projection at $i_0$. These are compatible in $n$ (since the basis has been chosen uniformly), hence yield a homomorphism + $$\varphi : G \to \lim_n (G / p^n G) \to \lim_n (\IZ / p^n \IZ) = \IZ_p.$$ + We have $\varphi(x) = 1$; thus, the $(\IZ_p, \varphi)$ component of $\alpha(x)$ is not $p$-divisible, implying that $\alpha(x)$ itself is not $p$-divisible. + unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -75,8 +84,19 @@ special_morphisms: description: 'homomorphisms $f : A \to B$ such that $B/f(A)$ is a torsion group' proof: The homomorphism $f$ is an epimorphism iff its cokernel in $\TorsFreeAb$ is trivial. As with all types of colimits, the cokernel is the torsion-free reflection of the cokernel in $\Ab$, which is $B/f(A)$. This is trivial iff $B/f(A)$ is torsion. regular monomorphisms: - description: 'injective group homomorphisms $i : A \to B$ such that $B/i(A)$ is torsion-free, i.e., $i$ is the inclusion of a saturated subgroup' - proof: 'If $i : A \to B$ is the kernel of $f : B \to C$ in $\TorsFreeAb$, it is also the kernel of $f$ in $\Ab$, so we know that $i$ is injective with $i(A) = \{b \in B : f(b) = 0\}$. If $n \in \IZ \setminus \{0\}$ and $b \in B$ satisfy $f(n b) = 0$, then also $f(b)=0$ since $C$ is torsion-free. This shows that $B/i(A)$ is torsion-free. Conversely, if $i$ is injective and $B/i(A)$ is torsion-free, then $i$ is the kernel of the natural homomorphism $B \to B/i(A)$.' + description: 'For a homomorphism $f : A \to B$ the following are equivalent: (1) $f$ is a regular monomorphism. (2) $f$ is injective and $B/f(A)$ is torsion-free, i.e., $f$ is the inclusion of a saturated subgroup. (3) $f$ is injective and whenever we have $n \in \IZ \setminus \{0\}$ and $a \in A$ such that $f(a)$ is $n$-divisible in $B$, then $a$ is $n$-divisible in $A$. (4) $f$ is injective and whenever we have $p$ prime and $a\in A$ such that $f(a)$ is $p$-divisible in $B$, then $a$ is $p$-divisible in $A$.' + proof: >- + (1) implies (2): If $f : A \to B$ is the kernel of $g : B \to C$ in $\TorsFreeAb$, it is also the kernel of $f$ in $\Ab$, so we know that $f$ is injective with $f(A) = \{b \in B : g(b) = 0\}$. If $n \in \IZ \setminus \{0\}$ and $b\in B$ satisfy $g(n b) = 0$, then also $g(b)=0$ since $C$ is torsion-free. This shows that $B/f(A)$ is torsion-free. + + (2) implies (1): If $f$ is injective and $B/f(A)$ is torsion-free, then $f$ is the kernel of the natural homomorphism $B \to B/f(A)$. + + (2) implies (3): If $f(a)$ is $n$-divisible, say $f(a) = nb$. Then $n[b] = 0$ for $[b] \in B/f(A)$, so $[b] = 0$. This implies $b \in f(A)$; say $f(a') = b$. Then $f(na') = nb = f(a)$, so by injectivity of $f$, we get $a = na'$. + + (3) implies (2): Suppose we have $n \in \IZ \setminus \{0\}$ and $b \in B$ such that letting $[b] \in B/f(A)$ be the image, $n[b] = 0$. That implies $nb \in f(A)$; say $nb = f(a)$ for $a \in A$. Then $f(a)$ is $n$-divisible, so $a$ is $n$-divisible; say $a = n a'$. This gives $n f(a') = f(a) = nb$. Since $B$ is torsion-free, we conclude $f(a') = b$, so $[b] = 0$ in $B/f(A)$. + + (3) implies (4): This is trivial. + + (4) implies (3): It is sufficient to show that the set of $n \in \IZ \setminus \{0\}$ such that $n$-divisibility of $f(a)$ implies $n$-divisibility of $a$ for all $a \in A$ is closed under multiplication: then since this set contains all primes by assumption, and it is easy to see it contains $-1$, it must be all of $\IZ \setminus \{0\}$. Thus, suppose we have $m$ and $n$ in this set, and suppose that $a\in A$ is such that $f(a)$ is $mn$-divisible. Then in particular, $f(a)$ is $n$-divisible, so $a$ is $n$-divisible; say $a = n a'$. Since $B$ is torsion-free, we must have that $f(a')$ is $m$-divisible, so $a'$ is $m$-divisible; say $a' = m a''$. Then $a = mn a''$, showing that $a$ is $mn$-divisible. regular epimorphisms: description: surjective group homomorphisms proof: 'By the construction of the coequalizer in $\TorsFreeAb$ as the torsion-free reflection of the coequalizer in $\Ab$, every regular epimorphism is surjective. Conversely, if $f : A \to B$ is a surjective homomorphism of torsion-free abelian groups, in $\Ab$ it is the coequalizer of the two projections $A \times_B A \rightrightarrows A$, and $A \times_B A$ is also torsion-free. Hence, it is also the coequalizer of these projections in $\TorsFreeAb$.' diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index 2bc65497..d043f0ec 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -28,6 +28,14 @@ satisfied_properties: - property: finitary algebraic proof: Take the algebraic theory of a vector space. + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator since it represents the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. + check_redundancy: false + + - property: extremal cogenerator + proof: 'The one-dimensional vector space $K$ is an extremal cogenerator. To show this, using this result, since $\Vect_K$ is balanced, it suffices to show that $K$ is a cogenerator. For this, suppose we have two unequal vectors $x, y \in V$. Then $x - y \ne 0$, so there exists a functional $\varphi : V \to K$ such that $\varphi(x - y) \ne 0$. It follows that $\varphi(x) \ne \varphi(y)$.' + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Z_div.yaml b/database/data/categories/Z_div.yaml index e51985d6..f3c24246 100644 --- a/database/data/categories/Z_div.yaml +++ b/database/data/categories/Z_div.yaml @@ -42,6 +42,12 @@ unsatisfied_properties: - property: countably codistributive proof: If $p$ runs through all odd primes, we have $2 \sqcup \prod_p p = \lcm(2,\gcd_p p) = \lcm(2,0) = 0$, but $\prod_p (2 \sqcup p) = \gcd_p (\lcm(2,p)) = \gcd_p (2 \cdot p) = 2$. + - property: extremal generator + proof: The category is equivalent to $(\IN,\mid)$, which has infinitely many non-minimal elements. Therefore, by the corollary here, an extremal generator cannot exist. + + - property: extremal cogenerator + proof: The category is equivalent to $(\IN,\mid)$, which has infinitely many non-maximal elements. Therefore, by the corollary here, an extremal generator cannot exist. + special_objects: initial object: description: $1$ diff --git a/database/data/categories/real_interval.yaml b/database/data/categories/real_interval.yaml index d5e4b3d5..be32e71c 100644 --- a/database/data/categories/real_interval.yaml +++ b/database/data/categories/real_interval.yaml @@ -38,6 +38,9 @@ unsatisfied_properties: - property: inverse proof: Consider the strictly increasing sequence $1 - 1/2^n$ for $n \geq 0$. + - property: extremal generator + proof: The poset has infinitely many non-minimal elements $(0, 1]$. Therefore, by the corollary here, an extremal generator cannot exist. + - property: locally finitely presentable proof: It suffices to prove that $0$ (the initial object) is the only finitely presentable object. If $s > 0$, then $s = \sup_{n \in \IN, \, s \geq 1/n } (s - 1/n)$, but there is no $n$ with $s \leq s - 1/n$. diff --git a/database/data/categories/walking_commutative_square.yaml b/database/data/categories/walking_commutative_square.yaml index f2163d5c..9af90108 100644 --- a/database/data/categories/walking_commutative_square.yaml +++ b/database/data/categories/walking_commutative_square.yaml @@ -38,8 +38,8 @@ unsatisfied_properties: - property: semi-strongly connected proof: There is no morphism between $b$ and $c$ (resp., between $(0,1)$ and $(1,0)$). - - property: finitary algebraic - proof: This follows from this lemma. + - property: extremal generator + proof: The corresponding poset has three distinct non-minimal elements $b,c,d$. Therefore, by the corollary here, an extremal generator cannot exist. special_objects: initial object: diff --git a/database/data/categories/walking_composable_pair.yaml b/database/data/categories/walking_composable_pair.yaml index 0889d780..026b7935 100644 --- a/database/data/categories/walking_composable_pair.yaml +++ b/database/data/categories/walking_composable_pair.yaml @@ -35,8 +35,8 @@ satisfied_properties: proof: 'Take the two-sorted (finitary) algebraic theory with exactly one unary operation between them and the equation $x=y$ for each sort. There are exactly three algebras for this theory up to isomorphism: the identities on the empty set and the singleton, the morphism from the empty set to the singleton. Hence we get the equivalence to $\{0 \to 1 \to 2\}$.' unsatisfied_properties: - - property: finitary algebraic - proof: This follows from this lemma. + - property: extremal generator + proof: The corresponding poset contains two distinct non-minimal elements $1,2$. Therefore, by the corollary here, an extremal generator cannot exist. special_objects: initial object: diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index ee084f04..a652f7c0 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -32,11 +32,11 @@ satisfied_properties: - property: terminal object proof: The object $[0]$ is terminal since it is already terminal in $\Delta$. - - property: generator - proof: The object $[0]$ is generator since this is already true in $\Delta$. A direct proof is also possible. + - property: extremal generator + proof: The object $[1]$ is an extremal generator even in $\Delta$; now use Lemma 10 here. A direct proof is also possible. - - property: cogenerator - proof: The object $[1]$ is cogenerator since this is already true in $\Delta$. A direct proof is also possible. + - property: extremal cogenerator + proof: The object $[1]$ is an extremal cogenerator even in $\Delta$; now use Lemma 10 here. A direct proof is also possible. - property: epi-regular proof: 'The only non-identity epimorphism is $p$, which is the coequalizer of $\id, ip : [1] \rightrightarrows [1]$ (since $pi = \id$).' diff --git a/database/data/categories/walking_fork.yaml b/database/data/categories/walking_fork.yaml index 628071e5..f5d44606 100644 --- a/database/data/categories/walking_fork.yaml +++ b/database/data/categories/walking_fork.yaml @@ -32,9 +32,6 @@ satisfied_properties: - property: one-way proof: This is trivial. - - property: generator - proof: It is easy to check that $1$ is a generator. - - property: cogenerator proof: It is easy to check that $2$ is a cogenerator. @@ -44,6 +41,14 @@ satisfied_properties: - property: equalizers proof: The only pair of distinct parallel morphisms is $f,g$, and their equalizer is $i$. + - property: extremal generator + proof: >- + It is easy to check that $\Hom(1, {-})$ sends the category + $$0 \to 1 \rightrightarrows 2$$ + to the diagram in $\Set$ + $$\varnothing \to \{ \id_1 \} \rightrightarrows \{ f, g \}.$$ + From this, it is easy to see that $\Hom(1, {-})$ is faithful and conservative, so $1$ is an extremal generator. + - property: locally cartesian closed proof: We need to check that every slice category is cartesian closed. The slice category over $0$ is the trivial category. The slice category over $1$ is the walking morphism. Finally, the slice category over $2$ ist the walking commutative square. All of these are cartesian closed, see their pages for details. @@ -51,12 +56,13 @@ unsatisfied_properties: - property: strongly connected proof: There is no morphism $1 \to 0$. - - property: balanced - proof: Both $f$ and $g$ are monomorphisms and epimorphisms. - - property: binary powers proof: 'Assume that $X \coloneqq 2 \times 2$ exists. Since there is a diagonal morphism $2 \to X$, we must have $X = 2$, and the two projections $p_1,p_2 : X \rightrightarrows 2$ must be equal to the identity. But $f,g$ induce a morphism $(f,g) : 1 \to X$ with $p_1 (f,g) = f$ and $p_2 (f,g) = g$, so that $f=g$, a contradiction.' + - property: extremal cogenerator + proof: >- + Since any cogenerator must distinguish $f,g : 1 \rightrightarrows 2$ and the only object which has a morphism from $2$ is $2$, the only cogenerator is $2$. The unique morphism $h : 0 \to 2$ is not an isomorphism, but ${-} \circ h : \Hom(2,2) \to \Hom(0,2)$ is a bijection since both sides are singletons. Thus, $2$ is not an extremal cogenerator. + special_objects: initial object: description: $0$ diff --git a/database/data/categories/walking_pair.yaml b/database/data/categories/walking_pair.yaml index bcdfa53f..7df4c306 100644 --- a/database/data/categories/walking_pair.yaml +++ b/database/data/categories/walking_pair.yaml @@ -35,8 +35,8 @@ satisfied_properties: - property: one-way proof: This is trivial. - - property: generator - proof: It is easy to check that $0$ is a generator. + - property: extremal generator + proof: It is easy to check that $0$ is an extremal generator. - property: left cancellative proof: The two morphisms $0 \rightrightarrows 1$ are clearly monomorphisms. diff --git a/database/data/categories/walking_span.yaml b/database/data/categories/walking_span.yaml index 3f75f772..265ec318 100644 --- a/database/data/categories/walking_span.yaml +++ b/database/data/categories/walking_span.yaml @@ -28,19 +28,22 @@ satisfied_properties: - property: skeletal proof: The three objects are not isomorphic. - - property: initial object - proof: $0$ is an initial object. - - property: binary products proof: We have $0 \times x = 0$ for all $x$, $x \times x = x$, and $1 \times 2 = 0$. - property: locally cartesian closed proof: The slice category over $0$ is the trivial category, and the slice category over $1$ is the walking morphism, which is cartesian closed. The same holds for $2$ by symmetry. + - property: extremal cogenerator + proof: It follows from the corollary here that $0$, being the unique non-maximal element of the poset $\{ 0 < 1, 0 < 2 \}$, is an extremal cogenerator. + unsatisfied_properties: - property: sifted proof: There is no cospan between $1$ and $2$. + - property: extremal generator + proof: The corresponding poset has two non-minimal elements $1$ and $2$. Therefore, by the corollary here, it is impossible for $\Span$ to have an extremal generator. + special_objects: initial object: description: $0$ diff --git a/database/data/categories/walking_splitting.yaml b/database/data/categories/walking_splitting.yaml index e4f76405..eaca453e 100644 --- a/database/data/categories/walking_splitting.yaml +++ b/database/data/categories/walking_splitting.yaml @@ -37,8 +37,8 @@ satisfied_properties: - property: normal proof: 'The only non-identity monomorphism is $i : 0 \to 1$, which is the kernel of $\id_1$.' - - property: generator - proof: 'The object $1$ a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$.' + - property: extremal generator + proof: 'The object $1$ is a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$. It is also an extremal generator since $\Hom(1, 0) = \{ p \}$ and $\Hom(1, 1) = \{ \id_1, ip \}$ are not bijective. The only other non-isomorphism to check is $ip : 1 \to 1$, where left multiplication by the non-unit $ip$ cannot induce a bijection on $\End(1)$.' - property: preadditive proof: 'We can define $\id_1 + \id_1 \coloneqq ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\Vect_{\IF_2}$ that consists only of the trivial vector space $\{0\}$ and $\IF_2$. Since $\Vect_{\IF_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \IF_2$, $p : \IF_2 \to \{0\}$, and the zero morphism $ip : \IF_2 \to \IF_2$. Clearly, $pi$ is the identity.' diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 9e8b7719..b5870acc 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -64,8 +64,9 @@ assumptions: - accessible conclusions: - - generating set - proof: For a $\kappa$-accessible category, the set $G$ appearing in the definition gives a small dense full subcategory, which is in particular a generating set. + - extremal generating set + # TODO: refactor this once we add the property "has small dense subcategory" + proof: The set appearing in the definition of a $\kappa$-accessible category gives a small dense full subcategory, which is in particular an extremal generating set. is_equivalence: false - id: accessible_well-powered diff --git a/database/data/category-implications/connected.yaml b/database/data/category-implications/connected.yaml index d1748b38..1c280ba1 100644 --- a/database/data/category-implications/connected.yaml +++ b/database/data/category-implications/connected.yaml @@ -64,8 +64,15 @@ assumptions: - core-connected conclusions: - - generator - proof: This is trivial. + - extremal generator + proof: >- + Let $G$ be any object of a core-connected category. Then certainly $G$ is a generator: Let $f, g : X \rightrightarrows Y$ be morphisms such that $f \circ h = g \circ h$ for all $h : G \to X$. Choose an isomorphism $h : G \to X$. Then $h$ is an epimorphism, so that $f = g$. + + To see $G$ is in fact an extremal generator: Let $f : X \to Y$ be a morphism such that + $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$ + is a bijection. Then for any object $T$, + $$f \circ {-} : \Hom(T, X) \to \Hom(T, Y)$$ + is a bijection since $T \cong G$, and the Yoneda embedding of $f$ is a natural transformation $\Hom({-}, X) \to \Hom({-}, Y)$. By the Yoneda Lemma, $f$ is therefore an isomorphism. is_equivalence: false - id: trivial_is_core-connected diff --git a/database/data/category-implications/filtered + sifted.yaml b/database/data/category-implications/filtered + sifted.yaml index a8b2e992..6cc12900 100644 --- a/database/data/category-implications/filtered + sifted.yaml +++ b/database/data/category-implications/filtered + sifted.yaml @@ -8,6 +8,16 @@ proof: 'Every filtered category $\C$ is inhabited and has final diagonal functors $\Delta : \C \to \C^J$ for all finite index categories $J$; in particular, it is inhabited and its diagonal $\Delta: \C \to \C \times \C$ is final.' is_equivalence: false +# TODO: with appropriate additional category properties, the hypothesis that the category is sifted could be weakened to a hypothesis that the category is inhabited and has cospans of all pairs, or equivalently that all finite sets of objects have a cospan +- id: thin_sifted_is_filtered + assumptions: + - thin + - sifted + conclusions: + - filtered + proof: The assumption that the category is sifted implies that any finite set of objects (including an empty set) has a cospan. In order to conclude the category is filtered, the only thing left to show is that any parallel pair is coequalized by some morphism; but this is trivial in a thin category. + is_equivalence: false + - id: sifted_is_connected assumptions: - sifted diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index 75de76d0..4276c6be 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -9,20 +9,83 @@ proof: This is trivial. is_equivalence: false +- id: extremal_generator_consequence + assumptions: + - extremal generator + conclusions: + - extremal generating set + - generator + proof: This is trivial. + is_equivalence: false + +- id: extremal_generating_set_consequence + assumptions: + - extremal generating set + conclusions: + - generating set + proof: This is trivial. + is_equivalence: false + +- id: generator_balanced_consequence + assumptions: + - generator + - balanced + conclusions: + - extremal generator + proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). + is_equivalence: false + +- id: generating_set_balanced_consequences + assumptions: + - generating set + - balanced + conclusions: + - extremal generating set + proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). + is_equivalence: false + - id: generator_via_coproduct assumptions: - coproducts - generating set - - zero morphisms + - strongly connected conclusions: - generator - proof: 'If $S$ is a generating set, we claim that $U \coloneqq \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' + proof: We get this as a corollary of this result. + is_equivalence: false + +- id: extremal_generator_via_coproduct + assumptions: + - coproducts + - extremal generating set + - strongly connected + conclusions: + - extremal generator + proof: We get this as a corollary of this result. is_equivalence: false - id: free-algebra-generates assumptions: - finitary algebraic conclusions: - - generator - proof: Pick an algebraic theory that represents the category. The free algebra $F(1)$ on one generator is a generator since morphisms $F(1) \to X$ correspond to the elements of (the underlying set of) the algebra $X$. + - 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. + is_equivalence: false + +- id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set + assumptions: + - locally finite + - left cancellative + - semi-strongly connected + - extremal generating set + conclusions: + - essentially small + proof: >- + Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating set $S$. We then claim that + $$\Ob(\C) \to \IN^S, \, X \mapsto \bigl(G \mapsto \card(\Hom(G, X))\bigr)$$ + is injective on isomorphism classes of $\Ob(\C)$. To see this, suppose two objects $X$ and $Y$ map to the same cardinality tuple. Since $\C$ is semi-strongly connected, we may assume without loss of generality that there is a morphism $f : X \to Y$. Then since $f$ is a monomorphism, for each $G \in S$ we have + $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$ + is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism. + + This shows that the collection of isomorphism classes of objects of $X$ is in bijection with a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. is_equivalence: false diff --git a/database/data/category-implications/groupoids.yaml b/database/data/category-implications/groupoids.yaml index d0660811..a995b124 100644 --- a/database/data/category-implications/groupoids.yaml +++ b/database/data/category-implications/groupoids.yaml @@ -40,6 +40,24 @@ proof: Every slice category is a trivial category. is_equivalence: false +- id: groupoid_generator + assumptions: + - groupoid + - generator + conclusions: + - extremal generator + proof: This is trivial. + is_equivalence: false + +- id: groupoid_generating_set + assumptions: + - groupoid + - generating set + conclusions: + - extremal generating set + proof: This is trivial. + is_equivalence: false + - id: groupoid_with_multi-terminal assumptions: - groupoid diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index beb8c24a..3a036dfd 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -13,11 +13,11 @@ assumptions: - essentially small conclusions: - - generating set + - extremal generating set - locally essentially small - well-copowered - well-powered - proof: This is trivial. + proof: All conclusions are trivial except perhaps that the category has an extremal generating set. For that, let $S$ be a set with one representative of each isomorphism class of objects of the category. Then it is easy to show using the Yoneda Lemma that $S$ is an extremal generating set. is_equivalence: false - id: finite_consequence diff --git a/database/data/category-properties/cogenerating set.yaml b/database/data/category-properties/cogenerating set.yaml index cef03911..b202f105 100644 --- a/database/data/category-properties/cogenerating set.yaml +++ b/database/data/category-properties/cogenerating set.yaml @@ -1,12 +1,18 @@ id: cogenerating set relation: has a -description: 'A set of objects $S$ is called a cogenerating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : B \to G$ with $G \in S$ we have $h \circ f = h \circ g$. Equivalently, the functor $(\Hom(-,G))_{G \in S} : \C^{\op} \to (\Set^+)^S$ is faithful. This property refers to the existence of a cogenerating set.' +description: >- + A set of objects $S$ is called a cogenerating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : B \to Q$ with $Q \in S$ we have $h \circ f = h \circ g$. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful. This property refers to the existence of a cogenerating set. + + In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + $$A \to \textstyle\prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ + is a monomorphism for every object $A$. nlab_link: https://ncatlab.org/nlab/show/cogenerator dual: generating set invariant_under_equivalences: true related: - cogenerator + - extremal cogenerating set tags: - size diff --git a/database/data/category-properties/cogenerator.yaml b/database/data/category-properties/cogenerator.yaml index a7164f97..02645b87 100644 --- a/database/data/category-properties/cogenerator.yaml +++ b/database/data/category-properties/cogenerator.yaml @@ -7,7 +7,8 @@ invariant_under_equivalences: true related: - cogenerating set + - extremal cogenerator tags: - - morphism behavior + - object behavior - size diff --git a/database/data/category-properties/extremal cogenerating set.yaml b/database/data/category-properties/extremal cogenerating set.yaml new file mode 100644 index 00000000..f1acbce8 --- /dev/null +++ b/database/data/category-properties/extremal cogenerating set.yaml @@ -0,0 +1,18 @@ +id: extremal cogenerating set +relation: has an +description: >- + A set of objects $S$ is called an extremal cogenerating set if it is a cogenerating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $Q \in S$ we have ${-}\circ f : \Hom(B, Q) \to \Hom(A, Q)$ is a bijection. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal cogenerating set. + + In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + $$\textstyle A \to \prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ + is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal generating set +invariant_under_equivalences: true + +related: + - extremal cogenerator + - cogenerating set + +tags: + - size diff --git a/database/data/category-properties/extremal cogenerator.yaml b/database/data/category-properties/extremal cogenerator.yaml new file mode 100644 index 00000000..ef53ecd9 --- /dev/null +++ b/database/data/category-properties/extremal cogenerator.yaml @@ -0,0 +1,21 @@ +id: extremal cogenerator +relation: has an +description: >- + An object $Q$ of a category is called an extremal cogenerator if it is a cogenerator and for every morphism $f : A \to B$, if ${-}\circ f : \Hom(B,Q)\to\Hom(A,Q)$ is a bijection, then $f$ is an isomorphism. Equivalently, the functor $\Hom(-,Q) : \C^{\op} \to \Set^+$ is faithful and conservative. This property refers to the existence of an extremal cogenerator. + + In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + $$\textstyle A \to \prod_{f\in\Hom(A,Q)} Q$$ + is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). + + By definition, $Q$ is an extremal cogenerator if and only if $\{Q\}$ is an extremal cogenerating set. +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal generator +invariant_under_equivalences: true + +related: + - extremal cogenerating set + - cogenerator + +tags: + - object behavior + - size diff --git a/database/data/category-properties/extremal generating set.yaml b/database/data/category-properties/extremal generating set.yaml new file mode 100644 index 00000000..beb4151d --- /dev/null +++ b/database/data/category-properties/extremal generating set.yaml @@ -0,0 +1,18 @@ +id: extremal generating set +relation: has an +description: >- + A set of objects $S$ is called an extremal generating set if it is a generating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $G \in S$ we have $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is a bijection. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal generating set. + + In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ + is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal cogenerating set +invariant_under_equivalences: true + +related: + - extremal generator + - generating set + +tags: + - size diff --git a/database/data/category-properties/extremal generator.yaml b/database/data/category-properties/extremal generator.yaml new file mode 100644 index 00000000..086b3fe2 --- /dev/null +++ b/database/data/category-properties/extremal generator.yaml @@ -0,0 +1,21 @@ +id: extremal generator +relation: has an +description: >- + An object $G$ of a category is called an extremal generator if it is a generator and for every morphism $f : A \to B$, if $f\circ{-} : \Hom(G,A)\to\Hom(G,B)$ is a bijection, then $f$ is an isomorphism. Equivalently, the functor $\Hom(G,-) : \C \to \Set^+$ is faithful and conservative. This property refers to the existence of an extremal generator. + + In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + $$\textstyle\bigsqcup_{f\in\Hom(G,A)} G \to A$$ + is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). + + By definition, $G$ is an extremal generator if and only if $\{G\}$ is an extremal generating set. +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal cogenerator +invariant_under_equivalences: true + +related: + - extremal generating set + - generator + +tags: + - object behavior + - size diff --git a/database/data/category-properties/generating set.yaml b/database/data/category-properties/generating set.yaml index ae566ba4..2658ce9c 100644 --- a/database/data/category-properties/generating set.yaml +++ b/database/data/category-properties/generating set.yaml @@ -1,12 +1,18 @@ id: generating set relation: has a -description: 'A set of objects $S$ is called a generating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : G \to A$ with $G \in S$ we have $f \circ h = g \circ h$. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful. This property refers to the existence of a generating set.' +description: >- + A set of objects $S$ is called a generating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : G \to A$ with $G \in S$ we have $f \circ h = g \circ h$. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful. This property refers to the existence of a generating set. + + In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ + is an epimorphism for every object $A$. nlab_link: https://ncatlab.org/nlab/show/separator dual: cogenerating set invariant_under_equivalences: true related: - generator + - extremal generating set tags: - size diff --git a/database/data/category-properties/generator.yaml b/database/data/category-properties/generator.yaml index 15be9911..71196236 100644 --- a/database/data/category-properties/generator.yaml +++ b/database/data/category-properties/generator.yaml @@ -7,7 +7,8 @@ invariant_under_equivalences: true related: - generating set + - extremal generator tags: - - morphism behavior + - object behavior - size diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 9e915b32..9804cd0f 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -27,6 +27,18 @@ proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. is_equivalence: false +- id: faithful_with_balanced_domain + assumptions: + - faithful + mapped_assumptions: + domain: + - balanced + conclusions: + - conservative + # TODO: refactor this if adding "reflects monomorphisms" / "reflects epimorphisms" properties + proof: 'It is easy to see that a faithful functor $F$ reflects monomorphisms: If we have two morphisms $x_1, x_2 : U \rightrightarrows X$ and $f : X \to Y$ such that $f(x_1) = f(x_2)$, and $F(f)$ is a monomorphism, then $F(x_1) = F(x_2)$; therefore, $x_1 = x_2$, so $f$ is also a monomorphism. The dual argument shows that $F$ also reflects epimorphisms. Therefore, if $F(f)$ is an isomorphism, then $f$ is both a monomorphism and an epimorphism; by the assumption on the domain category, this implies that $f$ is an isomorphism.' + is_equivalence: false + - id: left-invertible_consequences assumptions: - left-invertible diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml index f2183422..1533afd2 100644 --- a/database/data/functors/power_set_covariant.yaml +++ b/database/data/functors/power_set_covariant.yaml @@ -24,9 +24,6 @@ satisfied_properties: proof: 'If $f : X \to Y$ is injective, then $f^* \circ f_* = \id_{P(X)}$, so that $f_*$ is injective.' check_redundancy: false - - property: conservative - proof: 'Assume that $f : X \to Y$ is a map such that $f_* : P(X) \to P(Y)$ is an isomorphism. There is some $A \subseteq X$ with $Y = f_*(A)$, this proves that $f$ is surjective. It is also injective: If $x,y \in X$ satisfy $f(x) = f(y)$, then $f_*(\{x\}) = f_*(\{y\})$, and hence $\{x\} = \{y\}$, i.e. $x = y$.' - - property: preserves coreflexive equalizers proof: >- Let $f,g : X \rightrightarrows Y$ be a coreflexive pair in $\Set$. Choose a common retraction $r : Y \to X$, so that $rf = rg = \id_X$. Let $E = \{x \in X : f(x)=g(x)\}$ be the usual equalizer in $\Set$. We must show that for every subset $A \subseteq X$, the equality $f_*(A) = g_*(A)$ implies $A \subseteq E$. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 07245296..f88bfaf0 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -20,6 +20,7 @@ \F: \mathcal{F} \I: \mathcal{I} \J: \mathcal{J} +\M: \mathcal{M} \O: \mathcal{O} \S: \mathcal{S} \T: \mathcal{T} @@ -63,6 +64,7 @@ \rank: \operatorname{rank} \Gal: \operatorname{Gal} \Alt: \operatorname{Alt} +\Open: \operatorname{Open} # categories \Set: \mathbf{Set} diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index a3742dc7..4d8ef7c2 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -116,6 +116,10 @@ "ℵ₂-small coproducts": true, "ℵ₂-small powers": true, "ℵ₂-small copowers": true, + "extremal generator": true, + "extremal generating set": true, + "extremal cogenerator": true, + "extremal cogenerating set": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 437474cb..5ceebb92 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -113,6 +113,10 @@ "ℵ₂-small copowers": true, "pretopos": true, "quasitopos": true, + "extremal generator": true, + "extremal generating set": true, + "extremal cogenerator": true, + "extremal cogenerating set": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 0f62fd84..f66e00c9 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -80,6 +80,8 @@ "ℵ₂-small coproducts": true, "ℵ₂-small powers": true, "ℵ₂-small copowers": true, + "extremal cogenerator": true, + "extremal cogenerating set": true, "abelian": false, "additive": false, @@ -173,5 +175,7 @@ "quasitopos": false, "regular-subobject-trivial": false, "regular-quotient-trivial": false, - "core-connected": false + "core-connected": false, + "extremal generator": false, + "extremal generating set": false } diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index 1b1bfa01..b3717bb9 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -262,9 +262,9 @@ test('user can open and close a proof for a property of a category', async ({ pa test('user can open a proof for a deduced satisfied property of category', async ({ page }) => { - await page.goto('/category/Set', { waitUntil: 'networkidle' }) + await page.goto('/category/Ring', { waitUntil: 'networkidle' }) - const claim = page.locator('li', { has: page.getByText('has a generator') }) + const claim = page.locator('li', { has: page.getByText('has an extremal generator') }) await expect(claim).toBeVisible() @@ -273,7 +273,7 @@ test('user can open a proof for a deduced satisfied property of category', async const popup = page.locator('.popup').filter({ hasText: 'Proof' }) await expect( - popup.getByText('Since it is finitary algebraic, it has a generator') + popup.getByText('Since it is finitary algebraic, it has an extremal generator') ).toBeVisible() })