From d7c406150fefca0de40c6c8b41a64ab2f99ae787 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 11 Jul 2026 19:49:56 -0400 Subject: [PATCH 01/11] 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 02/11] 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. From 143855171ab13351c2083a30af65ae7f7c8a984e Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Mon, 20 Jul 2026 20:50:57 -0400 Subject: [PATCH 03/11] Add an easy implication to simplify deduced proof that the walking span has an initial object --- .../data/category-implications/filtered + sifted.yaml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/database/data/category-implications/filtered + sifted.yaml b/database/data/category-implications/filtered + sifted.yaml index a8b2e9929..6cc129005 100644 --- a/database/data/category-implications/filtered + sifted.yaml +++ b/database/data/category-implications/filtered + sifted.yaml @@ -8,6 +8,16 @@ proof: 'Every filtered category $\C$ is inhabited and has final diagonal functors $\Delta : \C \to \C^J$ for all finite index categories $J$; in particular, it is inhabited and its diagonal $\Delta: \C \to \C \times \C$ is final.' is_equivalence: false +# TODO: with appropriate additional category properties, the hypothesis that the category is sifted could be weakened to a hypothesis that the category is inhabited and has cospans of all pairs, or equivalently that all finite sets of objects have a cospan +- id: thin_sifted_is_filtered + assumptions: + - thin + - sifted + conclusions: + - filtered + proof: The assumption that the category is sifted implies that any finite set of objects (including an empty set) has a cospan. In order to conclude the category is filtered, the only thing left to show is that any parallel pair is coequalized by some morphism; but this is trivial in a thin category. + is_equivalence: false + - id: sifted_is_connected assumptions: - sifted From ff6cfcbf90b31f1304f754e98e8c1d241177d287 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 21 Jul 2026 00:05:27 -0400 Subject: [PATCH 04/11] Address some of the review comments --- content/subcategories.md | 6 +++++ database/data/categories/Ban.yaml | 2 +- database/data/categories/Delta.yaml | 4 ++-- database/data/categories/FS.yaml | 2 +- database/data/categories/FiltVect.yaml | 7 +++++- database/data/categories/FinOrd.yaml | 4 ++-- database/data/categories/FinSet.yaml | 4 ++-- database/data/categories/FinVect_c.yaml | 2 +- database/data/categories/FinVect_f.yaml | 2 +- database/data/categories/FinVect_u.yaml | 2 +- database/data/categories/FreeAb.yaml | 2 +- database/data/categories/Grp.yaml | 3 +++ database/data/categories/Grp_c.yaml | 2 +- database/data/categories/Man.yaml | 12 ++++++---- database/data/categories/Meas.yaml | 6 ++++- database/data/categories/Met.yaml | 32 ++++++++++++++++++++----- database/data/categories/Set.yaml | 8 +++++++ database/data/categories/Vect.yaml | 8 +++++++ 18 files changed, 83 insertions(+), 25 deletions(-) diff --git a/content/subcategories.md b/content/subcategories.md index 977fb09ba..34040feb0 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -116,3 +116,9 @@ $$ $$ is a composition of faithful functors, hence faithful. $\square$ + +::: Lemma 10 +Any fully faithful functor reflects extremal generating sets (and therefore, by duality, it also reflects extremal cogenerating sets). In other words, if $U : \C \to \D$ is a fully faithful functor, and $S$ is a set of objects such that $U(S)$ is an extremal generating set of $\D$, then $S$ is an extremal generating set of $\C$. +::: + +_Proof:_ Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative. $\square$ diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml index 4cdfe1bc9..8c60955f3 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -22,7 +22,7 @@ satisfied_properties: - 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. + The Hahn-Banach theorem implies that $\IC$ is a cogenerator. We claim that it is in fact an extremal cogenerator. Thus, suppose $f : X \to Y$ is a morphism such that ${-} \circ f : \Hom(Y, \IC) \to \Hom(X, \IC)$ is bijective on the underlying sets. Then for any non-zero $x \in X$, by the Hahn-Banach theorem, there exists $\varphi \in X^*$ such that $|\varphi| = 1$ and $\varphi(x) = |x|$. Since $|\varphi| = 1$, we see that $\varphi$ is a morphism $X \to \IC$ in $\Ban$; so by the assumption, there exists a morphism $\psi : Y \to \IC$ such that $\varphi = \psi \circ f$. Therefore, $|x| = |\psi(f(x))| \le |f(x)|$; and conversely, since $f$ is a morphism, $|f(x)| \le |x|$. On the other hand, if $x = 0$, then certainly $|f(x)| = |x| = 0$. This shows that $f$ is isometric and therefore a regular monomorphism (see below). On the other hand, since $\IC$ is a cogenerator and ${-} \circ f$ is injective, we have $f$ is also an epimorphism. Hence, $f$ is an isomorphism. - property: CIP proof: This is immediate from the concrete description of coproducts and products. diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index 96ae22728..fb79a8b1e 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -34,10 +34,10 @@ satisfied_properties: proof: For all $n,m$ there are morphisms $[n] \to [0] \to [m]$. - property: extremal generator - proof: The ordered set $[1] = \{0 < 1\}$ is an extremal generator, even for $\PreOrd$. + proof: The ordered set $[1] = \{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. - property: extremal cogenerator - proof: The ordered set $[1] = \{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. + proof: The ordered set $[1] = \{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. - property: skeletal proof: 'If $f : [n] \to [m]$ is an isomorphism, then $n + 1 = m + 1$ by comparing the cardinalities, hence $n = m$.' diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index 02b176769..a93fe84fb 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -32,7 +32,7 @@ satisfied_properties: 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. + Now, suppose we have a surjective map $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty proper subsets, and it certainly also maps $\varnothing \mapsto \varnothing$ and $Y \mapsto X$. Therefore, since the contravariant powerset functor is conservative, that implies $f$ is an isomorphism. - property: 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 d12b6daa3..7b4ad2a10 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -50,7 +50,12 @@ satisfied_properties: 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.' + proof: >- + Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space denoted with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. + + First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, F')$ such that ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$ is a bijection. This implies that $f^* : W^* \to V^*$ is an isomorphism of the dual vector spaces. But since $K$ is a cogenerator of $\Vect_K$ and $\Vect_K$ is balanced, in fact $K$ is an extremal cogenerator of $\Vect_K$; so from $f^*$ being an isomorphism, we conclude $f : V \to W$ is an isomorphism of vector spaces. + + It remains to show that if $f$ also induces a bijection ${-} \circ f : \Hom((W, F'), K_n) \to \Hom(V, F), K_n)$ for each $n$, then $f$ induces an isomorphism of the filtrations. For this step, we may assume without loss of generality that $f = \id_V : V \to V$. By the observations above, this then reduces to showing that if $S_1^\perp = S_2^\perp$ where $S_1 \coloneqq F_n(V), S_2 \coloneqq F_n'(V)$ are subspaces of $V$ such that $S_1^\perp = S_2^\perp$, then $S_1 = S_2$. However, if we had $x \in S_1 \setminus S_2$, then starting with a basis of $S_2$, adjoining $x$, and then extending to a basis of $V$, we see that there is a functional $\varphi \in V^*$ such that $\varphi |_{S_2} = 0$ and $\varphi(x) = 1$. But then $\varphi \in S_2^* \setminus S_1^*$, giving a contradiction. This shows $S_1 \subseteq S_2$; and similarly $S_2 \subseteq S_1$. - property: finitely accessible proof: >- diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index c0fed193a..20626dd9d 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -35,10 +35,10 @@ satisfied_properties: proof: Every non-empty totally ordered set is weakly terminal (by using constant maps). - property: extremal generator - proof: The same proof as for $\PreOrd$ shows that $\{ 0<1 \}$ is an extremal generator of $\FinOrd$. + proof: The ordered set $\{0 < 1\}$ is an extremal generator, even for $\PreOrd$. Now apply Lemma 10 here. - property: extremal cogenerator - proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. + proof: The ordered set $\{0 < 1\}$ is an extremal cogenerator, even for $\Pos$. Now apply Lemma 10 here. - property: equalizers proof: Take the equalizer in $\FinSet$ and restrict the order. diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 7fd4681d3..193a2eb6b 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -27,10 +27,10 @@ satisfied_properties: proof: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$. - 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). + proof: The one-point set is an extremal generator even in $\Set$. Now apply Lemma 10 here. - 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). + proof: The two-element set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. - property: semi-strongly connected proof: Every non-empty finite set is weakly terminal (by using constant maps). diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 0fb686096..98cb1cb42 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -24,7 +24,7 @@ satisfied_properties: 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: 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. + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_f.yaml b/database/data/categories/FinVect_f.yaml index 9e20f9273..7fa859c9e 100644 --- a/database/data/categories/FinVect_f.yaml +++ b/database/data/categories/FinVect_f.yaml @@ -27,7 +27,7 @@ satisfied_properties: proof: Each hom-set $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is finite by assumption. - 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. + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index cbc95c6e9..49fb75b96 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -24,7 +24,7 @@ satisfied_properties: 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: 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. + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index e36b2ca94..e27292b7b 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -24,7 +24,7 @@ satisfied_properties: proof: This is is because free abelian groups are closed under direct sums of abelian groups. - property: extremal generator - proof: As for $\Ab$, the group $\IZ$ is an extremal generator. + proof: The group $\IZ$ is an extremal generator even in $\Grp$. Now apply Lemma 10 here. - property: cogenerator proof: It is easy to check that $\IZ$ is a cogenerator for free abelian groups. diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 68fe0c40e..2ac9644a3 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -39,6 +39,9 @@ satisfied_properties: - property: effective cocongruences proof: A proof can be found here. + - property: extremal generator + proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor $\Grp \to \Set$, which is faithful and conservative. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 7bcf64561..da6d60f21 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -26,7 +26,7 @@ satisfied_properties: check_redundancy: false - 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. + proof: The countable group $\IZ$ is an extremal generator even in $\Grp$. Now use Lemma 10 here. - property: finite products proof: This is because $\Grp$ has finite (in fact, all) products, and $\Grp_\c \hookrightarrow \Grp$ is closed under finite products. This is because a finite product of countable sets is again countable. diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index 6101cc426..8e076e054 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -24,17 +24,21 @@ satisfied_properties: - 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. + The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Man \to \Set$. Since we have an epimorphism $\IR \to 1$, we see that $\IR$ is also a generator. - We claim that in fact, $\IR$ is an extremal generator. To see this, suppose we have a smooth map $f : M \to N$ which induces a bijection of smooth curves on $M$ to smooth curves on $N$. By considering constant curves, we must have that $f$ is a bijection on the underlying sets. Now 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. + We claim that in fact, $\IR$ is an extremal generator. To see this, suppose we have a smooth map $f : M \to N$ which induces a bijection of smooth curves on $M$ to smooth curves on $N$. By considering constant curves, we must have that $f$ is a bijection on the underlying sets. Now for any point $p \in M$ and any tangent vector $v \in \T_{f(p)}(N)$, there exists a smooth curve $\gamma : \IR \to N$ such that $\gamma(0) = f(p)$ and $\gamma'(0) = v$. By the assumption on $f$, there exists a smooth curve $\beta : \IR \to M$ such that $\gamma = f \circ \beta$. By the injectivity of $f$, we must have $\beta(0) = p$, so $\beta'(0) \in \T_p(M)$ and $f_*(\beta'(0)) = \gamma'(0) = v$. This shows that $f_* : \T_p(M) \to \T_{f(p)}(N)$ is surjective, hence $f$ is a submersion whose fibers are singletons. Therefore, by the submersion theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism. - property: extremal cogenerator proof: >- The manifold $\IR$ is a cogenerator, since for every smooth manifold $M$ and points $p \neq q$ in $M$ there is a smooth function $f : M \to \IR$ with $f(p) = 1$ and $f(q) = 0$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25). - In fact, $\IR$ is an extremal cogenerator. To see this, suppose we have a smooth map $f : M \to N$ such that ${-} \circ f : \Hom(N, \IR) \to \Hom(M, \IR)$ is a bijection. Then using bump maps as before to separate points of $M$, we can see that $f$ must be injective on underlying sets. Also, since $\IR$ is a cogenerator and ${-} \circ f$ is injective, we get that $f$ is an epimorphism, so it has dense image (see below). We claim that in fact, $f$ is surjective. To see this, suppose we had $q \in N \setminus \im(f)$. Then there is a 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$. + 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$. - 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. + Now, recall that the tangent space $\T_p(M)$ of $M$ at a point $p$ is defined as the space of $\IR$-linear functions $\partial : C^\infty(M) \to \IR$ such that $\partial(gh) = g(p) \partial(h) + h(p) \partial(g)$; and similarly for the tangent space of $N$ at $f(p)$. Also, the push-forward $f_* : \T_p(M) \to \T_{f(p)}(N)$ is defined by precomposition with $f^* : C^\infty(N) \to C^\infty(M)$. But by assumption, $f^* : C^\infty(N) \to C^\infty(M)$ is a bijection. Also, $f^* : C^\infty(N) \to C^\infty(M)$ is a homomorphism of $\IR$-algebras, so its inverse function $(f^*)^{-1} : C^\infty(M) \to C^\infty(N)$ is also a homomorphism of $\IR$-algebras. Furthermore, + $$(f^*)^{-1}(g)(f(p)) = f^*((f^*)^{-1}(g))(p) = g(p)$$ + for each $g \in C^\infty(M)$. Therefore, we see that for each $\partial \in \T_{f(p)}(N)$, $\partial \circ (f^*)^{-1} \in \T_p(M)$, and this defines an inverse to $f_* : \T_p(M) \to \T_{f(p)}(N)$. Thus, by the inverse function theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism. - 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 e2c9c407d..f6275e996 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -74,7 +74,11 @@ unsatisfied_properties: 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. + Now, suppose $S$ is a set of measurable spaces, and let $\kappa$ be an uncountable regular cardinal greater than $\card(G)$ for each $G \in S$. We claim that the bijective measurable map + $$(\kappa+1, M_\kappa') \to (\kappa+1, \M_\kappa), \, \alpha \mapsto \alpha,$$ + which is not an isomorphism, induces a bijection + $$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$ + for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. special_objects: initial object: diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 034ee9670..be85e7f1d 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -27,17 +27,37 @@ satisfied_properties: 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.' + 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(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, + $$\begin{align*} + d(x_1, x_2) &= d(\psi(0), \psi(\varepsilon)) \\ + & \le d(0, \varepsilon) \\ + & = \varepsilon \\ + & = d(f(x_1), f(x_2)) \\ + & \le d(x_1, x_2). + \end{align*}$$ + This shows that $f$ is isometric. - property: extremal cogenerator + # Note: $\IR$ is not an extremal cogenerator. This is because for example the non-isomorphism $(0, 1) \hookrightarrow [0, 1]$ induces a bijection $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$. To see this, suppose we have a non-expansive map $f : (0, 1) \to \IR$. Then since $f$ is uniformly continuous in particular, it is well known that $\lim_{x\to 0^+} f(x)$ and $\lim_{x\to 1^-} f(x)$ both exist and are finite. If we extend $f$ with these values at 0 and 1 respectively, then it is straightforward to check that the resulting function is still non-expansive. This shows that $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is surjective; and since $(0, 1) \hookrightarrow [0, 1]$ is an epimorphism, $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is also injective. (The same proof also shows that $\IR_{\ge 0}$ is not an extremal cogenerator. proof: >- We claim that $\IR_+$ (where $0 \notin \IR+$) with metric inherited from the usual metric on $\IR$ is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR_+$. This applies in particular to $f(x) \coloneqq d(a,x)+1$ and shows that $1=d(a,a)+1=d(a,b)+1$, so that $a=b$. - In fact, $\IR_+$ is an extremal cogenerator. To see this, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that ${-} \circ f : \Hom(Y, \IR_+) \to \Hom(X, \IR_+)$ is a bijection. First of all, since ${-} \circ f$ is injective and $\IR_+$ is a cogenerator, $f$ is an epimorphism, so it has dense image (see below). Now for each $x \in X$, we have a non-expansive map $\varphi : X \to \IR_+$, $x' \mapsto d(x, x') + 1$. By the assumption, there exists $\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. + In fact, $\IR_+$ is an extremal cogenerator. To see this, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that ${-} \circ f : \Hom(Y, \IR_+) \to \Hom(X, \IR_+)$ is a bijection. First of all, since ${-} \circ f$ is injective and $\IR_+$ is a cogenerator, $f$ is an epimorphism, so it has dense image (see below). Now for each $x \in X$, we have a non-expansive map + $$\varphi : X \to \IR_+, \,x' \mapsto d(x, x') + 1.$$ + By the assumption, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. Therefore, + $$\begin{align*} + d(x, x') &= |d(x, x') - d(x, x)| \\ + & = |\varphi(x') - \varphi(x)| \\ + & = |\psi(f(x')) - \psi(f(x))| \\ + & \le d(f(x), f(x')) \\ + & \le d(x,x'). + \end{align*}$$ + This shows that $f$ is isometric, which in particular implies $f$ is injective on underlying sets. + + It remains to show $f$ is surjective on underlying sets. To see this, suppose to the contrary that we have $y \in Y \setminus f(X)$. Then we have a non-expansive map + $$\varphi : X \to \IR_+,\, x \mapsto d(y, f(x)).$$ + By the assumption on $f$, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. However, since $\psi$ (seen as a function with codomain $\IR$) and $d(y, {-})$ are two continuous functions $Y \to \IR$ which agree on the dense subset $f(X)$, they must be the same function. Thus, $\psi(y) = d(y, y) = 0$, giving a contradiction. - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 6c3bde0f7..32ac39f38 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -32,6 +32,14 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty set is weakly terminal (by using constant maps). + - property: extremal generator + proof: The one-point set is an extremal generator since it represents the identity functor $\id_{\Set}$ which is certainly faithful and conservative. + check_redundancy: false + + - property: extremal cogenerator + proof: The two-point set is an extremal cogenerator since it represents the contravariant power set functor $\Set^{\op} \to \Set$ which is faithful and conservative (see contravariant power set functor). + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index 2bc654970..c13d3947c 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -28,6 +28,14 @@ satisfied_properties: - property: finitary algebraic proof: Take the algebraic theory of a vector space. + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator since it generates the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. + check_redundancy: false + + - property: extremal cogenerator + proof: 'The one-dimensional vector space $K$ is an extremal cogenerator. To show this, since $\Vect_K$ is balanced, it suffices to show that $K$ is a cogenerator. For this, suppose we have two unequal vectors $x, y \in V$. Then $x - y \ne 0$, so there exists a functional $\varphi : V \to K$ such that $\varphi(x - y) \ne 0$. It follows that $\varphi(x) \ne \varphi(y)$.' + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. From d16bf27a6438f351904e73f8fd66ee68d6735bce Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 21 Jul 2026 08:52:57 -0400 Subject: [PATCH 05/11] More updates to address review comments --- database/data/categories/Grp.yaml | 1 + database/data/categories/Met.yaml | 6 +----- database/data/categories/Met_c.yaml | 22 +++++++++++++++++----- database/data/categories/Met_oo.yaml | 2 +- database/data/categories/Mono.yaml | 10 ++++++++-- tests/categories.spec.ts | 2 +- 6 files changed, 29 insertions(+), 14 deletions(-) diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 2ac9644a3..0ffee1527 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -41,6 +41,7 @@ satisfied_properties: - property: extremal generator proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor $\Grp \to \Set$, which is faithful and conservative. + check_redundancy: false unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index be85e7f1d..11a72d323 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -22,13 +22,9 @@ satisfied_properties: - property: strict initial object proof: The empty metric space is initial and clearly strict. - - property: generator - proof: The one-point metric space is a generator since it represents the forgetful functor $\Met \to \Set$. - 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(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, + 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 the one-point metric space $1$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : Q \twoheadrightarrow 1$, then $G$ is also a generator. Now, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, $$\begin{align*} d(x_1, x_2) &= d(\psi(0), \psi(\varepsilon)) \\ & \le d(0, \varepsilon) \\ diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 5b81eac0c..e96a79882 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -37,11 +37,23 @@ satisfied_properties: - 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. + The space $\IR$ with the usual metric is a cogenerator. To see this, suppose we have $x, y \in X$ with $f(x) = f(y)$ for each continuous $f : X \to \IR$. In particular, this folds for $f(z) \coloneqq d(x, z)$, implying that + $$d(x, y) = f(y) = f(x) = d(x, x) = 0,$$ + so $x = y$. + + In fact, $\IR$ is an extremal cogenerator. To see this, suppose $f : X \to Y$ is a continuous function of metric spaces such that ${-} \circ f : \Hom(Y, \IR) \to \Hom(X, \IR)$ is a bijection. We first show that $f$ is injective on the underlying sets. Thus, suppose we have $x_1, x_2 \in X$ with $f(x_1) = f(x_2)$. Then the function $d(x_1, {-}) : X \to \IR$ is continuous, so there exists a continuous function $\varphi : Y \to \IR$ such that $d(x_1, x) = \varphi(f(x))$ for each $x \in X$. In particular, + $$d(x_1, x_2) = \varphi(f(x_2)) = \varphi(f(x_1)) = d(x_1, x_1) = 0,$$ + so $x_1 = x_2$. + + Now, the fact that ${-} \circ f$ is a bijection, and $\IR$ is a cogenerator, implies that $f$ is an epimorphism, i.e. its image is dense in $Y$. We claim that in fact $f$ is surjective on underlying sets. Suppose, for the sake of contradiction, that we had $y \in Y \setminus \im(f)$. Then we can define a continuous function + $$X \to \IR, \, x \mapsto \frac{1}{d(f(x), y)}.$$ + By the assumption on $f$, there exists continuous $\varphi : Y \to \IR$ such that + $$\varphi(f(x)) = \frac{1}{d(f(x), y)}$$ + for each $x \in X$. However, since $f$ has dense image, there is a sequence $(x_n)_{n=1}^\infty$ of points of $X$ such that $f(x_n) \to y$, while + $$\lim_{n\to \infty} \varphi(f(x_n)) = \lim_{n\to \infty} \frac{1}{d(f(x_n), y)} = \infty.$$ + This makes it impossible for $\varphi$ to be continuous at $y$, giving a contradiction. + + Finally, since we have shown $f$ is bijective on underlying sets, to show $f$ is a homeomorphism, it suffices to show that $f$ is closed. Thus, let $F \subseteq X$ be closed. Then $d({-}, F) : X \to \IR$ is a continuous function, so there exists $\varphi : Y \to \IR$ such that $\varphi(f(x)) = d(x, F)$ for each $x\in X$. That implies that $f_*(F) = \{ y\in Y : \varphi(y) = 0 \}$ is closed. - 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 b6f71d6bf..b7c9b3885 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -21,7 +21,7 @@ satisfied_properties: proof: A similar proof to the one for $\Met$ shows that $[0, \infty]$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\Met_{\infty}$. - property: extremal cogenerator - proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric 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$.' + proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric extending the usual metric on $\IR_+$ by defining $d(a,\infty) \coloneqq \infty$ for $a \in \IR_+$. Then one checks that the maps $1 + d(a,{-}) : X \to \IR_+ \cup \{\infty\}$ (assigning the value $\infty$ if $d(a,x) = \infty$) are non-expansive and finishes as for $\Met$.' - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index 9e02eba98..35074f261 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -33,7 +33,9 @@ satisfied_properties: proof: >- Consider the forgetful functor $U : \Mono \to \Set$, $(X, X') \mapsto X$. This has right adjoint $R : \Set \to \Mono$, $X \mapsto (X, X)$. Therefore, by the dual of Lemma 9 here, $R$ preserves cogenerators; and in particular, since $\Set$ has a cogenerator, so does $\Mono$. In other words, $(\{0,1\}, \{0,1\})$ is a cogenerator of $\Mono$. - We now claim that adding $(\{0,1\}, \{1\})$ gives an extremal cogenerating set. To see this, suppose we have $f : (X, X') \to (Y, Y')$ such that ${-} \circ f$ induces bijections of morphisms both to $(\{0,1\}, \{0,1\})$ and to $(\{0,1\}, \{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. + We now claim that adding $(\{0,1\}, \{1\})$ gives an extremal cogenerating set. To see this, suppose we have $f : (X, X') \to (Y, Y')$ such that ${-} \circ f$ induces bijections of morphisms both to $(\{0,1\}, \{0,1\})$ and to $(\{0,1\}, \{0\})$. Then since the first object represents the functor taking $(X, X')$ to $\Hom_{\Set}(X, \{ 0, 1 \})$, and $\{ 0, 1 \}$ is an extremal cogenerator of $\Set$, the bijection of morphisms for the first object implies that $f$ is a bijection $X \to Y$. On the other hand, the second object represents the functor taking $(X, X')$ to the collection of subsets of $X$ which contain $X'$; and under the Yoneda embedding, the monomorphism $(\{0,1\}, \{1\}) \hookrightarrow (\{0,1\}, \{0,1\})$ corresponds to the natural inclusion $\{ S\in P(X) : X' \subseteq S \} \hookrightarrow P(X)$. Therefore, if $f$ also induces a bijection of morphisms to the second object, then in particular there is a set $S$ with $Y' \subseteq S \subseteq Y$ with $f^*(S) = X'$. However, since $f$ is bijective, we also have $f^*(f(X')) = X'$ and $f^* : P(Y) \to P(X)$ is bijective, so $S = f(X')$. In other words, + $$Y' \subseteq S = f(X') \subseteq Y',$$ + so $f(X') = Y'$. Finally, since the collection of two objects is strongly connected (e.g. using the constant maps with image 1 in both directions), this result implies that their product is an extremal cogenerator. @@ -98,7 +100,11 @@ unsatisfied_properties: - 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. + Let $(G, G')$ be any object. Then if $G'$ is empty, the unique morphism $(1, 0) \to (1, 1)$ induces a bijection + $$\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (1, 1))$$ + because both sides are singletons. On the other hand, if $G'$ is non-empty, then for either choice of morphism $(1, 0) \to (2, 0)$, the induced map + $$\Hom((G, G'), (1, 0)) \to \Hom((G, G'), (2, 0))$$ + is bijective because both sides are empty. Thus, in either case, $(G,G')$ is not an extremal generator. special_objects: initial object: diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index 5d06b932a..dace44c91 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -262,7 +262,7 @@ test('user can open and close a proof for a property of a category', async ({ pa test('user can open a proof for a deduced satisfied property of category', async ({ page }) => { - await page.goto('/category/Set', { waitUntil: 'networkidle' }) + await page.goto('/category/Ring', { waitUntil: 'networkidle' }) const claim = page.locator('li', { has: page.getByText('has an extremal generator') }) From 30374a8e0631ce3b79cabbb58e138a0ec5b83ffa Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 21 Jul 2026 22:33:49 -0400 Subject: [PATCH 06/11] Yet more improvements to address review comments --- database/data/categories/Met.yaml | 8 ++++-- database/data/categories/PMet.yaml | 27 +++++++++++++------ database/data/categories/Pos.yaml | 4 +-- database/data/categories/Set_c.yaml | 4 +-- database/data/categories/Setne.yaml | 4 +-- database/data/categories/Top.yaml | 10 ++++--- database/data/categories/Top_pointed.yaml | 2 +- database/data/categories/TorsFreeAb.yaml | 10 ++++--- .../categories/walking_coreflexive_pair.yaml | 4 +-- database/data/categories/walking_fork.yaml | 6 +---- .../data/categories/walking_splitting.yaml | 2 +- .../category-implications/generators.yaml | 10 ++++--- database/data/functor-implications/misc.yaml | 2 +- tests/categories.spec.ts | 2 +- 14 files changed, 59 insertions(+), 36 deletions(-) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 11a72d323..2700169da 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -24,7 +24,11 @@ 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 the one-point metric space $1$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : Q \twoheadrightarrow 1$, then $G$ is also a generator. Now, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, + Let $G$ be the metric space with underlying set $\IR_{\ge 0}$ equipped with the metric where $d(x,y) = 0$ if $x=y$, and otherwise $d(x,y) = x+y$. We claim that $G$ is an extremal generator. + + First, to see that $G$ is a generator, note that the one-point metric space $1$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, then $G$ is also a generator. + + Now, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence, $$\begin{align*} d(x_1, x_2) &= d(\psi(0), \psi(\varepsilon)) \\ & \le d(0, \varepsilon) \\ @@ -35,7 +39,7 @@ satisfied_properties: This shows that $f$ is isometric. - property: extremal cogenerator - # Note: $\IR$ is not an extremal cogenerator. This is because for example the non-isomorphism $(0, 1) \hookrightarrow [0, 1]$ induces a bijection $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$. To see this, suppose we have a non-expansive map $f : (0, 1) \to \IR$. Then since $f$ is uniformly continuous in particular, it is well known that $\lim_{x\to 0^+} f(x)$ and $\lim_{x\to 1^-} f(x)$ both exist and are finite. If we extend $f$ with these values at 0 and 1 respectively, then it is straightforward to check that the resulting function is still non-expansive. This shows that $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is surjective; and since $(0, 1) \hookrightarrow [0, 1]$ is an epimorphism, $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is also injective. (The same proof also shows that $\IR_{\ge 0}$ is not an extremal cogenerator. + # Note: $\IR$ is not an extremal cogenerator. This is because for example the non-isomorphism $(0, 1) \hookrightarrow [0, 1]$ induces a bijection $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$. To see this, suppose we have a non-expansive map $f : (0, 1) \to \IR$. Then since $f$ is uniformly continuous in particular, it is well known that $\lim_{x\to 0^+} f(x)$ and $\lim_{x\to 1^-} f(x)$ both exist and are finite. If we extend $f$ with these values at 0 and 1 respectively, then it is straightforward to check that the resulting function is still non-expansive. This shows that $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is surjective; and since $(0, 1) \hookrightarrow [0, 1]$ is an epimorphism, $\Hom([0, 1], \IR) \to \Hom((0, 1), \IR)$ is also injective. (The same proof also shows that $\IR_{\ge 0}$ is not an extremal cogenerator.) proof: >- We claim that $\IR_+$ (where $0 \notin \IR+$) with metric inherited from the usual metric on $\IR$ is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR_+$. This applies in particular to $f(x) \coloneqq d(a,x)+1$ and shows that $1=d(a,a)+1=d(a,b)+1$, so that $a=b$. diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index bd84aa64c..eb651043b 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -16,20 +16,31 @@ satisfied_properties: - property: locally small proof: There is a forgetful functor $\PMet \to \Set$ and $\Set$ is locally small. - - property: generator - proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. - 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 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$.) + proof: >- + The proof will be similar to the one for $\Met$. Namely, let $G$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$ for $x, y \in \IR_{ge 0}$, and $d(x, 0') = d(0', x) = x$ for $x \in \IR_{\ge 0}$. We will show $G$ is an extremal generator for $\PMet$. + + First, to see $G$ is a generator, note that the one-point metric space is a generator since it represents the forgetful functor $\PMet\to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, then $G$ is also a generator. + + Now, suppose that $f : X \to Y$ is a non-expansive map of pseudo-metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon \ge 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $G$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0') = x_1$. Hence, + $$\begin{align*} + d(x_1, x_2) &= d(\psi(0'), \psi(\varepsilon)) \\ + & \le d(0', \varepsilon) \\ + & = \varepsilon \\ + & = d(f(x_1), f(x_2)) \\ + & \le d(x_1, x_2). + \end{align*}$$ + This shows that $f$ is isometric. - property: extremal cogenerator proof: >- - Let $Q$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric extending the usual metric on $\IR_{\ge 0}$ with $d(x, 0') = x$. Then $Q$ is an extremal cogenerator. + Let $Q$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric extending the usual metric on $\IR_{\ge 0}$ with $d(x, 0') = x$ for $x \in \IR_{\ge 0}$. Then $Q$ is an extremal cogenerator. + + First, to see $Q$ is a cogenerator, note that the subspace $\{ 0, 0' \}$ is a cogenerator since every map into it is automatically nonexpansive and since $\{0,0'\}$ is a cogenerator in $\Set$. Therefore, since $\{ 0, 0' \} \hookrightarrow Q$ is a monomorphism, we have that $Q$ is also a cogenerator. - To see 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. + To see $Q$ is in fact an extremal cogenerator, suppose we have a non-expansive map $f : X \to Y$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection. First of all, any function $Y \to Q$ which factors through $\{ 0, 0' \}$ is automatically non-expansive; and the injectivity of $f^*$ on such maps implies that $f$ is surjective on underlying sets, since $\{ 0, 0' \}$ is a cogenerator of $\Set$. From this, we can conclude that $f^*$ in fact induces a bijection on the functions $Y\to Q$ and $X\to Q$, respectively, which factor through $\{ 0, 0' \}$. Since $\{ 0, 0' \}$ is in fact an extremal cogenerator of $\Set$, we conclude that in fact, $f$ is a bijection on underlying sets. - From here, the proof that $f$ is isometric is similar to the one for $\Met$, using the fact that $d(x, {-}) : X \to \IR_{\ge 0}$ induces a non-expansive map $Y \to \IR_{\ge 0}$. + From here, the proof that $f$ is isometric is similar to the one for $\Met$, using the fact that $d(x, {-}) : X \to \IR_{\ge 0} \hookrightarrow Q$ induces a non-expansive map $Y \to Q$. - 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 5208c10b3..2ee703901 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -28,13 +28,13 @@ satisfied_properties: proof: Every non-empty poset is weakly terminal (by using constant maps). - property: extremal generator - proof: We can use the same proof as for $\PreOrd$ to show that $\{0<1\}$ is an extremal generator of $\Pos$. + proof: We have that $\{0<1\}$ is an extremal generator even in $\PreOrd$. Now apply Lemma 10 here. - property: extremal cogenerator proof: >- We prove that the poset $\{0 < 1\}$ is an extremal cogenerator. First, to prove it is a cogenerator: Let $P$ be a poset and $a,b \in P$ be two elements such that $f(a) = f(b)$ for all order-preserving maps $f : P \to \{0 < 1 \}$. This means that $a$ and $b$ lie in the same upper sets. In particular, $b$ lies in the upper set generated by $a$, meaning $a \leq b$, and similarly we deduce $b \leq a$. Thus, $a = b$. - Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that ${-} \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. + Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that $f$ induces a bijection of upper sets implies that $f$ is also injective on the underlying sets, and also that $f(a_1) \le f(a_2)$ implies $a_1 \le a_2$. Therefore, $f$ is an isomorphism. - 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/Set_c.yaml b/database/data/categories/Set_c.yaml index cc77b4632..68501ef31 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -33,10 +33,10 @@ satisfied_properties: proof: This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide. - property: extremal generator - proof: The one-point set is clearly an extremal generator. + proof: The one-point set is an extremal generator even in $\Set$. Now apply Lemma 10 here. - property: extremal cogenerator - proof: The two-point set is an extremal cogenerator in $\Set$, hence also in $\Set_\c$. + proof: The two-point set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. - property: semi-strongly connected proof: This is because the larger category $\Set$ has this property. diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index c13c5639a..679f3941c 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -17,11 +17,11 @@ satisfied_properties: proof: There is a forgetful functor $\Setne \to \Set$ and $\Set$ is locally small. - property: extremal generator - proof: The one-point set is clearly an extremal generator. + proof: The one-point set is an extremal generator even in $\Set$. Now use Lemma 10 here. check_redundancy: false - property: extremal cogenerator - proof: The two-point set is an extremal cogenerator, this follows as for $\Set$. + proof: The two-point set is an extremal cogenerator even in $\Set$. Now use Lemma 10 here. - property: products proof: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 9ae3a9d52..ba9ce91f6 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -40,7 +40,7 @@ satisfied_properties: - 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. + Using the dual of Lemma 9 with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of $\Set$, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective. Now, by this result, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$. @@ -60,6 +60,10 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. + - property: balanced + proof: If $X$ is a set, consider the discrete space $X_d$ on $X$ and the indiscrete space $X_i$ on $X$. The identity map $X \to X$ lifts to a continuous map $X_d \to X_i$, which is bijective and therefore both a mono- and an epimorphism, but it is not an isomorphism unless $X$ has at most one element. + check_redundancy: false + - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see MSE/1255678.' @@ -80,9 +84,9 @@ unsatisfied_properties: - 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$. + Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating set. - To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $\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 \}$. + To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $T := \im(f) \cap \kappa$. Then $T \subseteq \kappa$ and $\card(T) \leq \card(G) < \kappa$. Since $\kappa$ is regular, this implies $\alpha := \sup(T) < \kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$. special_objects: initial object: diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index e4d2f1b61..6e60f0016 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -44,7 +44,7 @@ satisfied_properties: - 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. + It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator, using the fact that the pointed set $\{0,1\}$ with base point $1$ is a cogenerator of $Set_*$. If $S$ is the Sierpinski space on $\{0,1\}$, we claim that adding $(S, 0)$ and $(S, 1)$ gives an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. Then $f$ inducing a bijection on maps to $(\{0,1\},1)$ implies that the underlying function of $f$ is bijective. In particular, because $f$ is injective, we see that for $V$ an open subset of $Y$, $f^*(V)$ contains the base point of $X$ if and only if $V$ contains the base point of $Y$. Also, $f$ inducing a bijection on maps to $(S, 1)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets containing the base points, and $f$ inducing a bijection on maps to $(S, 0)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets not containing the base points. From these observations, we can conclude that $f$ is a homeomorphism. Now, by this result, we get that the product of these three pointed topological spaces is an extremal cogenerator of $\Top_*$. diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 7e71a9fb0..0c9326557 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -36,11 +36,15 @@ satisfied_properties: 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. + 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 $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By 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. - 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$. + For the second part, note in general that an injective homomorphism $\alpha : G \to H$ of torsion-free groups is a regular monomorphism if and only if whenever $n > 0$ and $x \in G$ is such that $\alpha(x)$ is $n$-divisible in $H$, then $x$ is $n$-divisible in $G$. In fact, it suffices to restrict to prime values of $n$: then for general $n$ with prime factorization $n = p_1 p_2 \cdots p_k$, suppose $\alpha(x)$ is $n$-divisible in $H$. Then in particular, $\alpha(x)$ is $p_1$-divisible, so $x$ is $p_1$-divisible; thus, there exists $x_1 \in G$ such that $p_1 x_1 = x$. Now $\alpha(x_1)$ is $p_2$-divisible, so similarly we find $x_2 \in G$ such that $p_2 x_2 = x_1$, and therefore $p_1 p_2 x_2 = x$. Continuing in this way, we eventually find $x_k \in G$ such that $p_1 p_2 \cdots p_k x_k = x$, i.e. $n x_k = x$. - 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. + In our case where we have $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$, we will prove the contrapositive of this condition; thus, suppose we have $x\in G$ which is not $p$-divisible. Let $\{y_i : i \in I\}$ be a subset of $G$ including $x = y_{i_0}$ whose images in $G / pG$ form a basis for this $\IZ / p \IZ$-vector space. We will now prove by induction that for each $n$, $G / p^n G$ is a free $\IZ / p^n \IZ$-module with basis given by the images of $y_i$. The base case $n=1$ is true by assumption. Now for the inductive step from $n$ to $n+1$, for $g \in G$ we can find $a_i \in \IZ$ (all but finitely many equal to zero) such that $g \in \sum_{i\in I} a_i y_i + p^n G$. Since $G$ is torsion-free, there exists a unique $h$ such that $g = \sum_{i\in I} a_i y_i + p^n h$. Now projecting $h$ into $G / pG$, we can find $b_i \in \IZ$ such that $h \in \sum_{i\in I} b_i y_i + pG$. Hence, $g \in \sum_{i\in I} (a_i + p^n b_i) y_i + p^{n+1} G$. The uniqueness of the coefficients up to congruence modulo $p^{n+1}$ follows from the fact that there are unique choices of $a_i$ with $0 \le a_i < p^n$, and then the $b_i$ are unique up to congruence modulo $p$. + + Now for each $n$, let $\varphi_n : G / p^n G \to \IZ / p^n \IZ$ be the coordinate projection at $i_0$. These are compatible in $n$ (since the basis has been chosen uniformly), hence yield a homomorphism + $$\varphi : G \to \lim_n (G / p^n G) \to \lim_n (\IZ / p^n \IZ) = \IZ_p.$$ + We have $\varphi(x) = 1$; thus, the $(\IZ_p, \varphi)$ component of $\alpha(x)$ is not $p$-divisible, implying that $\alpha(x)$ itself is not $p$-divisible. - 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/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index db1872589..a652f7c01 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -33,10 +33,10 @@ satisfied_properties: proof: The object $[0]$ is terminal since it is already terminal in $\Delta$. - property: extremal generator - proof: The object $[0]$ is an extremal generator since this is already true in $\Delta$. A direct proof is also possible. + proof: The object $[1]$ is an extremal generator even in $\Delta$; now use Lemma 10 here. 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. + proof: The object $[1]$ is an extremal cogenerator even in $\Delta$; now use Lemma 10 here. A direct proof is also possible. - property: epi-regular proof: 'The only non-identity epimorphism is $p$, which is the coequalizer of $\id, ip : [1] \rightrightarrows [1]$ (since $pi = \id$).' diff --git a/database/data/categories/walking_fork.yaml b/database/data/categories/walking_fork.yaml index ac2b73af4..a75396fd6 100644 --- a/database/data/categories/walking_fork.yaml +++ b/database/data/categories/walking_fork.yaml @@ -61,11 +61,7 @@ unsatisfied_properties: - 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. + Since any cogenerator must distinguish $f,g : 1 \rightrightarrows 2$ and the only object which has a morphism from $2$ is $2$, the only cogenerator is $2$. The unique morphism $h : 0 \to 2$ is not an isomorphism, but ${-} \circ h : \Hom(2,2) \to \Hom(0,2)$ is a bijection since both sides are singletons. Thus, $2$ is not an extremal cogenerator. special_objects: initial object: diff --git a/database/data/categories/walking_splitting.yaml b/database/data/categories/walking_splitting.yaml index 15f83c511..eaca453e3 100644 --- a/database/data/categories/walking_splitting.yaml +++ b/database/data/categories/walking_splitting.yaml @@ -38,7 +38,7 @@ satisfied_properties: proof: 'The only non-identity monomorphism is $i : 0 \to 1$, which is the kernel of $\id_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)$.' + proof: 'The object $1$ is a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$. It is also an extremal generator since $\Hom(1, 0) = \{ p \}$ and $\Hom(1, 1) = \{ \id_1, ip \}$ are not bijective. The only other non-isomorphism to check is $ip : 1 \to 1$, where left multiplication by the non-unit $ip$ cannot induce a bijection on $\End(1)$.' - property: preadditive proof: 'We can define $\id_1 + \id_1 \coloneqq ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\Vect_{\IF_2}$ that consists only of the trivial vector space $\{0\}$ and $\IF_2$. Since $\Vect_{\IF_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \IF_2$, $p : \IF_2 \to \{0\}$, and the zero morphism $ip : \IF_2 \to \IF_2$. Clearly, $pi$ is the identity.' diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index db0c088a2..cb930b6f3 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -72,16 +72,20 @@ 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 +- id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set assumptions: - locally finite - - right cancellative + - left 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. + Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating set $S$. We then claim that + $$\Ob(\C) \to \IN^S, \, X \mapsto (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. Since $\C$ is semi-strongly connected, we may assume without loss of generality that there is a morphism $f : X \to Y$. Then since $f$ is a monomorphism, for each $G \in S$ we have + $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$ + is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism. This shows that the collection of isomorphism classes of objects of $X$ is in bijection with a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. is_equivalence: false diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index e9b6c275f..f516eb739 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -36,7 +36,7 @@ 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.' + proof: 'It is easy to see that a faithful functor $F$ reflects monomorphisms: If we have two morphisms $x_1, x_2 : U \rightrightarrows X$ and $f : X \to Y$ such that $f(x_1) = f(x_2)$, and $F(f)$ is a monomorphism, then $F(x_1) = F(x_2)$; therefore, $x_1 = x_2$, so $f$ is also a monomorphism. The dual argument shows that $F$ also reflects epimorphisms. Therefore, if $F(f)$ is an isomorphism, then $f$ is both a monomorphism and an epimorphism; by the assumption on the domain category, this implies that $f$ is an isomorphism.' is_equivalence: false - id: left-invertible_consequences diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index dace44c91..b3717bb9c 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -262,7 +262,7 @@ test('user can open and close a proof for a property of a category', async ({ pa test('user can open a proof for a deduced satisfied property of category', async ({ page }) => { - await page.goto('/category/Ring', { waitUntil: 'networkidle' }) + await page.goto('/category/Ring', { waitUntil: 'networkidle' }) const claim = page.locator('li', { has: page.getByText('has an extremal generator') }) From b903d41e527c0b5b5a23ffe1a3a136ab319b1f4a Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 21 Jul 2026 22:54:33 -0400 Subject: [PATCH 07/11] Another review comment addressed --- database/data/category-implications/connected.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/category-implications/connected.yaml b/database/data/category-implications/connected.yaml index b80169566..ed18e2ac6 100644 --- a/database/data/category-implications/connected.yaml +++ b/database/data/category-implications/connected.yaml @@ -65,7 +65,7 @@ - core-connected conclusions: - 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$. + proof: To see any object $G$ in a core-connected category $\C$ is an extremal generator, note that $\Hom(G, {-})$ can be factored into the Yoneda embedding into $[\C^{\op}, \Set^+]$ followed by evaluation at $G$. However, if $\C$ is core-connected, then $[\C^{\op}, \Set^+]$ is equivalent to $\End(G)^{\op}{-}\Set^+$, and under this equivalence, the functor of evaluation at $G$ corresponds to the forgetful functor $\End(G)^{\op}{-}\Set^+ \to \Set^+$. Since the Yoneda embedding is fully faithful and therefore also conservative, and the forgetful functor $\End(G)^{\op}{-}\Set^+ \to \Set^+$ is faithful and conservative, we conclude that their composition is also faithful and conservative. is_equivalence: false - id: trivial_is_core-connected From 32fa8194f4cbea9591c8345f712f5a87276454eb Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Wed, 22 Jul 2026 11:13:14 -0400 Subject: [PATCH 08/11] Condition on extremal generators in a thin category is actually an equivalence; use that to rework the proof that the walking span has an extremal cogenerator --- content/thin_extremal_generator.md | 12 +++++++----- database/data/categories/walking_span.yaml | 7 +------ 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md index 31f43484d..fd20f49e8 100644 --- a/content/thin_extremal_generator.md +++ b/content/thin_extremal_generator.md @@ -7,15 +7,17 @@ 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. +Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism. ::: -_Proof._ 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. +_Proof._ ($\Rightarrow$) Since the category is thin, $\Hom(G, X)$ is either a singleton or empty. In the first case, let $f \in \Hom(G, X)$. Then $f \circ {-} : \Hom(G, G) \to \Hom(G, X)$ is automatically a bijection since $\Hom(G, G) = \{ \id_G \}$ is also a singleton, implying that $f$ is an isomorphism. -In the second case, suppose we have a morphism $g : Y \to X$. Then $g \circ {-} : \Hom(G, Y) \to \Hom(G, X)$ is a function with empty codomain, so it is automatically a bijection, implying that $g$ is an isomorphism. $\square$ +In the second case, suppose we have a morphism $g : Y \to X$. Then $g \circ {-} : \Hom(G, Y) \to \Hom(G, X)$ is a function with empty codomain, so it is automatically a bijection, implying that $g$ is an isomorphism. + +($\Leftarrow$) Since the category is thin, any object is automatically a generator. Now suppose we have a morphism $f : X \to Y$ such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then by assumption, either $Y \cong G$ or every morphism with codomain $Y$ is an isomorphism. In the first case, $\Hom(G, Y)$ is non-empty, so $\Hom(G, X)$ is also non-empty. We also have $\Hom(Y, G)$ is non-empty. Therefore, $\Hom(Y, X)$ is non-empty, and the (necessarily unique) morphism $Y \to X$ is automatically an inverse to $f$. In the second case, $f$ is already a morphism with codomain $Y$ so it is an isomorphism. $\square$ ::: Corollary -A poset whose corresponding thin category has an extremal generator can contain at most one non-minimal element. +For a poset $P$, the corresponding thin category has an extremal generator if and only if $P$ is non-empty and it has at most one non-minimal element. In particular, if this is the case, then either the poset is discrete, in which case any element gives an extremal generator; or otherwise, there is exactly one non-minimal element which is the unique extremal generator. ::: -_Proof._ In a thin category coming from a poset, the second condition in the previous lemma is equivalent to the corresponding element of the poset being minimal. $\square$ +_Proof._ In a thin category coming from a poset, the condition in the previous lemma that every morphism with codomain $X$ is an isomorphism is equivalent to the corresponding element of the poset being minimal. $\square$ diff --git a/database/data/categories/walking_span.yaml b/database/data/categories/walking_span.yaml index c5838ff3c..265ec3184 100644 --- a/database/data/categories/walking_span.yaml +++ b/database/data/categories/walking_span.yaml @@ -35,12 +35,7 @@ satisfied_properties: 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. + proof: It follows from the corollary here that $0$, being the unique non-maximal element of the poset $\{ 0 < 1, 0 < 2 \}$, is an extremal cogenerator. unsatisfied_properties: - property: sifted From bc7d89136690d4b8215af2391d4fea6d12b13ffb Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Thu, 23 Jul 2026 09:41:06 -0400 Subject: [PATCH 09/11] Update database/data/categories/Vect.yaml Co-authored-by: Script Raccoon --- database/data/categories/Vect.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index c13d3947c..cac372ce2 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -29,7 +29,7 @@ satisfied_properties: proof: Take the algebraic theory of a vector space. - property: extremal generator - proof: The one-dimensional vector space $K$ is an extremal generator since it generates the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. + proof: The one-dimensional vector space $K$ is an extremal generator since it represents the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. check_redundancy: false - property: extremal cogenerator From 78d779eb2303518418a904cf60448d11af09fec4 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Thu, 23 Jul 2026 09:43:20 -0400 Subject: [PATCH 10/11] Update database/data/categories/PMet.yaml Co-authored-by: Script Raccoon --- database/data/categories/PMet.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index eb651043b..ce7df3528 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -36,7 +36,7 @@ satisfied_properties: proof: >- Let $Q$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric extending the usual metric on $\IR_{\ge 0}$ with $d(x, 0') = x$ for $x \in \IR_{\ge 0}$. Then $Q$ is an extremal cogenerator. - First, to see $Q$ is a cogenerator, note that the subspace $\{ 0, 0' \}$ is a cogenerator since every map into it is automatically nonexpansive and since $\{0,0'\}$ is a cogenerator in $\Set$. Therefore, since $\{ 0, 0' \} \hookrightarrow Q$ is a monomorphism, we have that $Q$ is also a cogenerator. + First, to see $Q$ is a cogenerator, note that the subspace $\{ 0, 0' \}$ is a cogenerator since every map into it is automatically non-expansive and since $\{0,0'\}$ is a cogenerator in $\Set$. Therefore, since $\{ 0, 0' \} \hookrightarrow Q$ is a monomorphism, we have that $Q$ is also a cogenerator. To see $Q$ is in fact an extremal cogenerator, suppose we have a non-expansive map $f : X \to Y$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection. First of all, any function $Y \to Q$ which factors through $\{ 0, 0' \}$ is automatically non-expansive; and the injectivity of $f^*$ on such maps implies that $f$ is surjective on underlying sets, since $\{ 0, 0' \}$ is a cogenerator of $\Set$. From this, we can conclude that $f^*$ in fact induces a bijection on the functions $Y\to Q$ and $X\to Q$, respectively, which factor through $\{ 0, 0' \}$. Since $\{ 0, 0' \}$ is in fact an extremal cogenerator of $\Set$, we conclude that in fact, $f$ is a bijection on underlying sets. From 5703aeebafede291c1b4a69d97213269d65d00d6 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Thu, 23 Jul 2026 09:43:42 -0400 Subject: [PATCH 11/11] Update database/data/categories/TorsFreeAb.yaml Co-authored-by: Script Raccoon --- database/data/categories/TorsFreeAb.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 0c9326557..c5a3465ab 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -36,7 +36,7 @@ satisfied_properties: 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 $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By 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. + We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \text{~prime}\}$ is an extremal cogenerating set, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By 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, note in general that an injective homomorphism $\alpha : G \to H$ of torsion-free groups is a regular monomorphism if and only if whenever $n > 0$ and $x \in G$ is such that $\alpha(x)$ is $n$-divisible in $H$, then $x$ is $n$-divisible in $G$. In fact, it suffices to restrict to prime values of $n$: then for general $n$ with prime factorization $n = p_1 p_2 \cdots p_k$, suppose $\alpha(x)$ is $n$-divisible in $H$. Then in particular, $\alpha(x)$ is $p_1$-divisible, so $x$ is $p_1$-divisible; thus, there exists $x_1 \in G$ such that $p_1 x_1 = x$. Now $\alpha(x_1)$ is $p_2$-divisible, so similarly we find $x_2 \in G$ such that $p_2 x_2 = x_1$, and therefore $p_1 p_2 x_2 = x$. Continuing in this way, we eventually find $x_k \in G$ such that $p_1 p_2 \cdots p_k x_k = x$, i.e. $n x_k = x$.