From d7c406150fefca0de40c6c8b41a64ab2f99ae787 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 11 Jul 2026 19:49:56 -0400 Subject: [PATCH 1/2] Add extremal (co)generating sets and single extremal (co)generators Co-authored-by: Script Raccoon --- content/generator_construction.md | 12 +++- content/thin_extremal_generator.md | 21 ++++++ database/data/categories/Ab_fg.yaml | 4 +- database/data/categories/Ban.yaml | 5 +- database/data/categories/Cat.yaml | 7 +- database/data/categories/Delta.yaml | 8 +-- database/data/categories/FI.yaml | 4 +- database/data/categories/FS.yaml | 7 +- database/data/categories/FiltVect.yaml | 4 ++ database/data/categories/FinOrd.yaml | 8 +-- database/data/categories/FinSet.yaml | 8 +-- database/data/categories/FinVect_c.yaml | 4 +- database/data/categories/FinVect_f.yaml | 4 +- database/data/categories/FinVect_u.yaml | 4 +- database/data/categories/FreeAb.yaml | 4 +- database/data/categories/Grp_c.yaml | 4 +- database/data/categories/Haus.yaml | 9 +-- database/data/categories/Man.yaml | 16 +++-- database/data/categories/Meas.yaml | 20 ++++-- database/data/categories/Met.yaml | 4 ++ database/data/categories/Met_c.yaml | 13 ++-- database/data/categories/Met_oo.yaml | 4 +- database/data/categories/Mono.yaml | 15 +++-- database/data/categories/N.yaml | 6 ++ database/data/categories/N_oo.yaml | 7 +- database/data/categories/PMet.yaml | 6 +- database/data/categories/Pos.yaml | 11 +-- database/data/categories/PreOrd.yaml | 13 ++-- database/data/categories/Set_c.yaml | 8 +-- database/data/categories/Set_f.yaml | 11 ++- database/data/categories/Setne.yaml | 8 +-- database/data/categories/Top.yaml | 21 +++--- database/data/categories/Top_pointed.yaml | 18 ++--- database/data/categories/TorsFreeAb.yaml | 11 ++- database/data/categories/Z_div.yaml | 6 ++ database/data/categories/real_interval.yaml | 3 + .../walking_commutative_square.yaml | 4 +- .../categories/walking_composable_pair.yaml | 4 +- .../categories/walking_coreflexive_pair.yaml | 8 +-- database/data/categories/walking_fork.yaml | 20 ++++-- database/data/categories/walking_pair.yaml | 4 +- database/data/categories/walking_span.yaml | 14 +++- .../data/categories/walking_splitting.yaml | 4 +- .../category-implications/accessible.yaml | 5 +- .../data/category-implications/connected.yaml | 4 +- .../category-implications/generators.yaml | 67 +++++++++++++++++-- .../data/category-implications/groupoids.yaml | 18 +++++ database/data/category-implications/size.yaml | 4 +- .../category-properties/cogenerating set.yaml | 1 + .../data/category-properties/cogenerator.yaml | 1 + .../extremal cogenerating set.yaml | 18 +++++ .../extremal cogenerator.yaml | 21 ++++++ .../extremal generating set.yaml | 18 +++++ .../extremal generator.yaml | 21 ++++++ .../category-properties/generating set.yaml | 1 + .../data/category-properties/generator.yaml | 1 + database/data/functor-implications/misc.yaml | 12 ++++ .../data/functors/power_set_covariant.yaml | 3 - database/data/macros.yaml | 2 + database/scripts/expected-data/Ab.json | 4 ++ database/scripts/expected-data/Set.json | 4 ++ database/scripts/expected-data/Top.json | 6 +- tests/categories.spec.ts | 4 +- 63 files changed, 447 insertions(+), 144 deletions(-) create mode 100644 content/thin_extremal_generator.md create mode 100644 database/data/category-properties/extremal cogenerating set.yaml create mode 100644 database/data/category-properties/extremal cogenerator.yaml create mode 100644 database/data/category-properties/extremal generating set.yaml create mode 100644 database/data/category-properties/extremal generator.yaml diff --git a/content/generator_construction.md b/content/generator_construction.md index a7cef4c68..31a540424 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) (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. 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/thin_extremal_generator.md b/content/thin_extremal_generator.md new file mode 100644 index 000000000..31f43484d --- /dev/null +++ b/content/thin_extremal_generator.md @@ -0,0 +1,21 @@ +--- +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 extremal generator of a thin category. Then for any object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism. +::: + +_Proof._ 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. $\square$ + +::: Corollary +A poset whose corresponding thin category has an extremal generator can contain at most one non-minimal element. +::: + +_Proof._ In a thin category coming from a poset, the second condition in the previous lemma 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 7ab864bd5..41588e5b8 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 f42a88994..4cdfe1bc9 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -20,8 +20,9 @@ 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: 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 $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|$. 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: CIP proof: This is immediate from the concrete description of coproducts and products. diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 58c86d4f6..bb9cb21d1 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -27,8 +27,11 @@ 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: 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. - 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$.' diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index 2c8930b4d..96ae22728 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$. - - 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$. - 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 0db4df274..21c676b81 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 c5415c430..02b176769 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -28,8 +28,11 @@ 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: 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 morphism $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 subsets, and it certainly also maps $\varnothing \mapsto \varnothing$. Therefore, since the contravariant powerset functor is conservative, that implies $f$ is an isomorphism. - 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. diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 29d7ae932..d12b6daa3 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -47,6 +47,10 @@ 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$. Then $K_n \hookrightarrow (K, n \mapsto K)$ represents the functor $(V, F) \mapsto F_n(V)^{\perp} \subseteq V^*$. It is straightforward to check that the dual vector space functor along with these functors is a jointly conservative collection. Therefore, $\{ K_n : n \in \IZ \} \cup \{ (K, n \mapsto K) \}$ is an extremal cogenerating set.' - property: finitely accessible proof: >- diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index ff1714684..c0fed193a 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 same proof as for $\PreOrd$ shows that $\{ 0<1 \}$ is an extremal generator of $\FinOrd$. - - 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$. - 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 be7aa454d..7fd4681d3 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 since it represents the forgetful functor $\FinSet \to \Set$ which is faithful and conservative (in fact, fully faithful). - - property: cogenerator - proof: The two-element set is a cogenerator. + - property: extremal cogenerator + proof: The two-element set is an extremal cogenerator since it represents the contravariant power set functor $\FinSet^{\op} \to \Set$ which is faithful and conservative (see contravariant power set functor). - 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 02db896fd..0fb686096 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 forgetful functor $\FinVect_K \to \Set$ is faithful and conservative, and it is represented by $K$. Hence, $K$ is a generator. - 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 78006a99d..9e20f9273 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 forgetful functor $\FinVect_K \to \Set$ is faithful and conservative, and it is represented by $K$. Hence, $K$ is an extremal generator. - 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 c7734fc31..cbc95c6e9 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 forgetful functor $\FinVect_K \to \Set$ is faithful and conservative, and it is represented by $K$. Hence, $K$ is a generator. - 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 ab65e1fdf..e36b2ca94 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: As for $\Ab$, the group $\IZ$ is an extremal generator. - property: cogenerator proof: It is easy to check that $\IZ$ is a cogenerator for free abelian groups. diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 7b2f8593e..7bcf64561 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 because it represents the forgetful functor $\Grp_\c \to \Set$ which is faithful and conservative. - 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 130249be0..02687dc5a 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 e3e6a6646..6101cc426 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -22,11 +22,19 @@ 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: extremal generator + proof: >- + The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Top \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 recall that the tangent space of $M$ at a point $p$ is equivalent to a set of equivalence classes of smooth curves $\gamma : \IR \to M$ with $\gamma(0) = p$; and similarly for the tangent space of $N$ at $f(p)$. Also, the push-forward of tangent spaces is characterized by $f_*([\gamma]) = [\gamma \circ f]$. We conclude that $f_* : \T_{M,p} \to \T_{N,f(p)}$ is an isomorphism for each $p \in M$. Thus, $f$ is 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 bump map $\varphi : N \to \IR$ such that the image of $\varphi$ is contained in $[0,1]$, and $\varphi$ achieves value 1 only at $q$ (for example, $e^{-|x|^2}$ achieves this on $\IR^n$; then we can multiply by a bump function which is 1 on a neighborhood of the origin and which has compact support, and then transport this to a chart around $q$). But then we can construct a smooth function $\psi : M \to \IR$ by $\psi(p) \coloneqq \frac{1}{1 - \phi(f(p))}$. The corresponding function $N \to \IR$ must agree with $\frac{1}{1 - \phi}$ on the image of $f$. We can now get a contradiction from the fact that the image of $f$ is dense, and therefore contains a sequence of points converging to $q$, whereas the values of $\frac{1}{1 - \phi}$ on this sequence diverge to $\infty$. - - 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).' + Now, recall that the tangent space of $M$ at a point $p$ is defined as the space of $\IR$-linear functions $\partial : C^\infty(M) \to \IR$ such that $\partial(\varphi \psi) = \varphi(p) \partial(\psi) + \psi(p) \partial(\varphi)$; and similarly for the tangent space of $N$ at $f(p)$. (Alternately, some authors might use germs of functions near $p$; however, such germs are easy to extend to global smooth functions with the same germ, via the technique of multiplying by a bump map.) Also, the push-forward $f_* : \T_{M,p} \to \T_{N,f(p)}$ is defined as composition with $f$. But by assumption, $f$ induces a bijection between $C^\infty(M)$ and $C^\infty(N)$, and it is easy to check that this restricts to an isomorphism $f_* : \T_{M,p} \to \T_{N,f(p)}$. Thus, $f$ is a diffeomorphism. - property: semi-strongly connected proof: Every non-empty manifold is weakly terminal (by using constant maps). diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index d7221d06e..e2c9c407d 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. @@ -43,6 +40,14 @@ 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 the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' + - 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$. + - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. @@ -53,9 +58,6 @@ 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,12 @@ 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$. Then for any measurable function $f : G \to (\kappa + 1, \M_\kappa)$ with $G \in S$, 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 the $f$ factors through $(\kappa + 1, \M_\kappa')$. This shows that $\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$ is a bijection for each $G \in S$, implying that $S$ cannot be an extremal generating set. + 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 942abdf78..eba9dd704 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -24,6 +24,10 @@ satisfied_properties: - property: generator proof: The one-point metric space is a generator since it represents the forgetful functor $\Met \to \Set$. + check_redundancy: false + + - 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. To see this, first note that we have an epimorphism $! : Q \twoheadrightarrow 1$ and $1$ is a generator, so $Q$ 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(x_1, x_2) = \delta > 0$. Then by definition, $d(f(x_1), f(x_2)) \le \delta$. On the other hand, there is a morphism $G \to Y$ which maps $\delta$ to $x_2$ and every other element of $\IR_{\ge 0}$ to $x_1$. Since $f$ is injective on underlying sets, the fact that this morphism is in the image of $f \circ {-}$ implies that $\delta \le d(f(x_1), f(x_2))$ also. Therefore, $f$ is a bijective isometry.' - 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$.' diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 74e9dd022..5b81eac0c 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -32,11 +32,16 @@ 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: 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: cogenerator - proof: The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator. + - property: extremal cogenerator + proof: >- + The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator. We claim that, in fact, it 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 $\varphi(f(x_n)) = \frac{1}{d(f(x_n), y)} \to \infty$ as $n \to \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. - property: well-powered proof: This follows easily from the fact that monomorphisms are injective in this category. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index f77f1e5b2..fb75dff02 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -17,8 +17,8 @@ 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: 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: 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$.' diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index b4099c138..9e02eba98 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -29,9 +29,13 @@ 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 + - 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$. + 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\}, \{1\})$. Then since the first object represents the functor taking $(X, X')$ to the power set of $X$, the bijection of morphisms for that object implies that $f$ is a bijection $X \to Y$. On the other hand, the second object represents the subfunctor taking $(X, X')$ to the collection of subsets of $X$ which contain $X'$. In particular, there is exactly one superset of $Y'$ which pulls back to $X'$, which implies $f(X') = Y'$ and thus $f$ is an isomorphism. + + 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: complete proof: >- @@ -88,13 +92,14 @@ 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: >- + Suppose $(G, G')$ were an extremal generator. Then if $G'$ is empty, we have $\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (1, 1))$ is a function between singleton sets and therefore a bijection, while $(1, 0) \to (1, 1)$ is not an isomorphism. On the other hand, if $G'$ is non-empty, then for either choice of morphism $(1, 0) \to (2, 0)$, we have $\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (2, 0))$ is a function between empty sets and therefore a bijection, while $(1, 0) \to (2, 0)$ is not an isomorphism. Thus, either case gives a contradiction. + special_objects: initial object: description: $(0, 0)$ diff --git a/database/data/categories/N.yaml b/database/data/categories/N.yaml index bf1af6874..45add20bf 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 7303fcb03..ecd3999c0 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 9ceac19e3..e58dbfcaf 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -18,9 +18,13 @@ satisfied_properties: - property: generator proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. + check_redundancy: false + + - property: extremal generator + proof: A proof similar to the one for $\Met$ shows that $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\PMet$. (For the case where $x_1 \ne x_2$ and $d(x_1, x_2) = 0$, use the map which sends all elements of $\IR_{\ge 0}$ to $x_1$ and $0'$ to $x_2$.) - 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$. + proof: The set $\{0,1\}$ equipped with the pseudo-metric $d(0,1)=0$ is a cogenerator since every map into it 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. diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index a8cfd5530..5208c10b3 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -27,11 +27,14 @@ 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: extremal generator + proof: We can use the same proof as for $\PreOrd$ to show that $\{0<1\}$ is an extremal generator of $\Pos$. - - 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: 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 ${-} \circ 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. - 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.' diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 2bd97f7b6..bd27e1538 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -23,11 +23,16 @@ 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: 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: 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: 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. - property: semi-strongly connected proof: Every non-empty preordered set is weakly terminal (by using constant maps). diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index ae6260574..cc77b4632 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 clearly an extremal generator. - - 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 in $\Set$, hence also in $\Set_\c$. - 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 0f17ebb22..3e709a78f 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 136deb47b..c13c5639a 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 clearly an extremal generator. 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, this follows as for $\Set$. - 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 c4d961e26..9ae3a9d52 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -38,11 +38,14 @@ 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: extremal cogenerator + proof: >- + It is easily checked that the indiscrete two-point space is a cogenerator. We claim that adding the Sierpinski space $(\{ 0, 1 \}, \{ \varnothing, \{ 1 \}, \{ 0, 1 \} \})$ 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. + + 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$. - 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$. @@ -57,18 +60,12 @@ 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. - - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see MSE/1255678.' - 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 +78,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$. We then claim that $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ is a bijection for every $G \in S$, showing that $S$ cannot be an extremal generating set. Here we use the standard order topology on both $\kappa$ and $\kappa + 1$. + + To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $\im(f) \cap \kappa$. This is a subset of $\kappa$ whose cardinality is strictly less than $\kappa$, so its supremum $\alpha$ is also less than $\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 5528583db..e4d2f1b61 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -42,8 +42,11 @@ 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: extremal cogenerator + proof: >- + It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator. 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_*$. - 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 +61,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$. @@ -70,15 +73,9 @@ 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 1bc8bd9c9..7e71a9fb0 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -32,8 +32,15 @@ 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: 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 \mathrm{~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 $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 the characterization below, this is equivalent to showing it is injective, and its image is a saturated subgroup. From the above, including $\IQ$ in $S$ is already sufficient to make it a monomorphism, i.e. an injective homomorphism. For the second part, it suffices to show for each prime $p$ that if $x\in G$ is not $p$-divisible, then its image in the product is not $p$-divisible. + + To see this, let $\{y_i : i \in I\}$ be a set 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 x_i + p^n G$. Since $G$ is torsion-free, there exists a unique $h$ such that $g = \sum_{i\in I} a_i x_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 x_i + pG$. Hence, $g \in \sum_{i\in I} (a_i + p^n b_i) x_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$. + + This then allows us to define a morphism $\varphi : G \to \IZ_p$ sending $g\in G$ to the limit of the $i_0$-indexed coefficients in $G / p^n G$. We have $\varphi(x) = 1$; thus, the $(\IZ_p, \varphi)$ component of the image of $x$ in the product is not $p$-divisible, implying that the image of $x$ itself is not $p$-divisible. - property: regular proof: The regular epimorphisms are exactly the surjective homomorphisms (see below), and these are clearly stable under pullbacks. diff --git a/database/data/categories/Z_div.yaml b/database/data/categories/Z_div.yaml index e51985d65..f3c24246c 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 d5e4b3d58..be32e71c5 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 f2163d5c9..9af901084 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 0889d780a..026b79355 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 ee084f042..db1872589 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 $[0]$ is an extremal generator since this is already true in $\Delta$. 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 since this is already true in $\Delta$. 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 628071e5a..ac2b73af4 100644 --- a/database/data/categories/walking_fork.yaml +++ b/database/data/categories/walking_fork.yaml @@ -32,8 +32,13 @@ satisfied_properties: - property: one-way proof: This is trivial. - - property: generator - proof: It is easy to check that $1$ is a generator. + - 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: cogenerator proof: It is easy to check that $2$ is a cogenerator. @@ -51,12 +56,17 @@ 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: >- + We see that $2$ is the only cogenerator of $\Fork$, since it must distinguish $f, g : 1 \rightrightarrows 2$ and any morphism with domain $2$ also has codomain $2$. However, $\Hom({-}, 2)$ sends the category + $$0 \to 1 \rightrightarrows 2$$ + to the diagram in $\Set$ + $$\{ f \circ i = g \circ i \} \leftarrow \{ f, g \} \leftleftarrows \{ \id_2 \}.$$ + Here we see that the diagram sends the non-isomorphism $f\circ i = g\circ i : 0 \to 2$ to a bijection of singleton sets, so $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 bcdfa53f8..7df4c3065 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 3f75f7727..c5838ff3c 100644 --- a/database/data/categories/walking_span.yaml +++ b/database/data/categories/walking_span.yaml @@ -28,19 +28,27 @@ 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: >- + The functor $\Hom({-}, 0)$ sends the category + $$1 \leftarrow 0 \rightarrow 2$$ + to the diagram in $\Set$ + $$\varnothing \rightarrow \{ \id_0 \} \leftarrow \varnothing.$$ + From this, it is easy to see that $\Hom({-}, 0)$ is faithful (which is trivial since the category is thin) and conservative. Therefore, $0$ 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 e4f764054..15f83c511 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 \rightrightarrows 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 94033586c..edc3f93e0 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -56,8 +56,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: For a $\kappa$-accessible category, the set $G$ appearing in the definition 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 d1748b38f..b80169566 100644 --- a/database/data/category-implications/connected.yaml +++ b/database/data/category-implications/connected.yaml @@ -64,8 +64,8 @@ assumptions: - core-connected conclusions: - - generator - proof: This is trivial. + - extremal generator + proof: The fact that any object is a generator is trivial. To see any object is an extremal generator, use the fact that the category is equivalent to $BM$ for some monoid $M$, along with the fact that for an element $m$ of a monoid $M$, $m$ is a unit if and only if left multiplication by $m$ is a bijection $M \to M$. is_equivalence: false - id: trivial_is_core-connected diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index 75de76d09..db0c088a2 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -9,20 +9,79 @@ 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_right-cancellative_semi-strongly-connected_extremal-generating-set + assumptions: + - locally finite + - right cancellative + - semi-strongly connected + - extremal generating set + conclusions: + - essentially small + proof: >- + Suppose a category $\C$ is locally finite, semi-strongly connected, and has an extremal generating set $S$. We then claim that $\Ob(\C) \to \IN^S, X \mapsto (G \mapsto \card(\Hom(G, X)))$, is injective on isomorphism classes of $\Ob(\C)$. To see this, suppose two objects $X$ and $Y$ map into the same cardinality tuple. Then there is either a morphism $f : X \to Y$ or a morphism $f : Y \to X$; without loss of generality, say $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 d0660811c..a995b1240 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 beb8c24ab..1efae19d3 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 Yoneda's 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 cef039115..d9eb5a6fd 100644 --- a/database/data/category-properties/cogenerating set.yaml +++ b/database/data/category-properties/cogenerating set.yaml @@ -7,6 +7,7 @@ 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 a7164f971..bef87986a 100644 --- a/database/data/category-properties/cogenerator.yaml +++ b/database/data/category-properties/cogenerator.yaml @@ -7,6 +7,7 @@ invariant_under_equivalences: true related: - cogenerating set + - extremal cogenerator tags: - morphism behavior 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 000000000..f1acbce8c --- /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 000000000..a3c202435 --- /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: + - morphism 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 000000000..beb4151d9 --- /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 000000000..9c333c5af --- /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: + - morphism behavior + - size diff --git a/database/data/category-properties/generating set.yaml b/database/data/category-properties/generating set.yaml index ae566ba4e..9a9704e05 100644 --- a/database/data/category-properties/generating set.yaml +++ b/database/data/category-properties/generating set.yaml @@ -7,6 +7,7 @@ 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 15be99116..ccc2b4fba 100644 --- a/database/data/category-properties/generator.yaml +++ b/database/data/category-properties/generator.yaml @@ -7,6 +7,7 @@ invariant_under_equivalences: true related: - generating set + - extremal generator tags: - morphism behavior diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 2cace7e9c..e9b6c275f 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 \to 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 f21834224..1533afd21 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 c91031fe2..3549e71fc 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} @@ -61,6 +62,7 @@ \cod: \operatorname{cod} \rank: \operatorname{rank} \Gal: \operatorname{Gal} +\Open: \operatorname{Open} # categories \Set: \mathbf{Set} diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index a3742dc7c..4d8ef7c29 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 437474cbf..5ceebb920 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 0f62fd843..f66e00c9c 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 1b1bfa01a..5d06b932a 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -264,7 +264,7 @@ test('user can open a proof for a deduced satisfied property of category', async }) => { await page.goto('/category/Set', { 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() }) From 484beecd2d706e4bc6a8d536d9700f5a35dfd471 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Jul 2026 14:48:16 -0400 Subject: [PATCH 2/2] Add extremal cogenerators for Met, Met_oo, PMet --- database/data/categories/Met.yaml | 11 +++++++++-- database/data/categories/Met_oo.yaml | 4 ++-- database/data/categories/PMet.yaml | 11 ++++++++--- 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index eba9dd704..034ee9670 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -29,8 +29,15 @@ satisfied_properties: - 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. To see this, first note that we have an epimorphism $! : Q \twoheadrightarrow 1$ and $1$ is a generator, so $Q$ 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(x_1, x_2) = \delta > 0$. Then by definition, $d(f(x_1), f(x_2)) \le \delta$. On the other hand, there is a morphism $G \to Y$ which maps $\delta$ to $x_2$ and every other element of $\IR_{\ge 0}$ to $x_1$. Since $f$ is injective on underlying sets, the fact that this morphism is in the image of $f \circ {-}$ implies that $\delta \le d(f(x_1), f(x_2))$ also. Therefore, $f$ is a bijective isometry.' - - 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: 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 $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. That means that $d(x, x') = |d(x, x') - d(x, x)| = |\phi(x') - \phi(x)| = |\psi(f(x')) - \psi(f(x))| \le d(f(x), f(x'))$. On the other hand, since $f$ is non-expansive, $d(f(x), f(x')) = d(x, x')$. 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 $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. However, since $\psi$ 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. + + We have now shown that $f$ is an isometry which is bijective on underlying sets, so $f$ is an isomorphism. - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index fb75dff02..b6f71d6bf 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -20,8 +20,8 @@ satisfied_properties: - 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: 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: extremal cogenerator + proof: 'The proof is similar to $\Met$: an extremal 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 $1 + 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). diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index e58dbfcaf..bd84aa64c 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -21,10 +21,15 @@ satisfied_properties: check_redundancy: false - property: extremal generator - proof: A proof similar to the one for $\Met$ shows that $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\PMet$. (For the case where $x_1 \ne x_2$ and $d(x_1, x_2) = 0$, use the map which sends all elements of $\IR_{\ge 0}$ to $x_1$ and $0'$ to $x_2$.) + proof: A proof similar to the one for $\Met$ shows that $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\PMet$. (For the case of the injectivity proof where $x_1 \ne x_2$ and $d(x_1, x_2) = 0$, use the map which sends all elements of $\IR_{\ge 0}$ to $x_1$ and $0'$ to $x_2$.) - - property: cogenerator - proof: The set $\{0,1\}$ equipped with the pseudo-metric $d(0,1)=0$ is a cogenerator since every map into it is automatically non-expansive and since $\{0,1\}$ is a cogenerator in $\Set$. + - 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$. Then $Q$ is an extremal cogenerator. + + To see this, 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}$ induces a non-expansive map $Y \to \IR_{\ge 0}$. - property: strict initial object proof: The empty (pseudo-)metric space is initial and clearly strict.