Add extremal (co)generating sets and single extremal (co)generators

[dschepler]

My primary motivation in the short term is to get "has an extremal generating set" into the database for use in entering one of the equivalent conditions in the Giraud-type theorem for Grothendieck quasitopoi. The property is, of course, of broader interest.

Current status:
extremal generator: 1 unknown
extremal generating set: 1 unknown
extremal cogenerator: 4 unknown
extremal cogenerating set: 4 unknown

(And all of these except for the case of FreeAb are cases where we still didn't even know whether they had generating/cogenerating sets.)

[ScriptRaccoon]

FYI #283 means that the files have changed their location, so a (trivial) rebasing is required.

[ScriptRaccoon]

Remark: many proofs here show something stronger, or are close to that, namely that the set or object is a dense subcategory. This property is not here yet, but maybe we should add it soon. Not in this PR perhaps because it is already big, unless you think it clarifies the proofs much better. We can also have separate PRs then for the missing proofs.

Btw, should I stop looking at this PR as long is it is in draft mode?

[dschepler]

Btw, should I stop looking at this PR as long is it is in draft mode?

No, comments and suggestions in the mean time are very useful.

Incidentally, I've looked at the remaining unsettled cases, and they seem very tricky. I can maybe make more detailed comments later once I'm done with work for the day. (The exception is extremal cogenerator for Sp which seems like it should be doable if I could get my head around it better. Maybe something like the set of all quotients of $\Sigma_n$ is an extremal cogenerating set for $\Sigma_n-Set$, and then take products and finally the tuple of those products?)

So I should probably be able to take the PR out of draft status soon, and then we can decide on what questions to submit to MO and/or which categories we're OK with leaving unknown for the moment.

[dschepler]

Some comments on some of the remaining undecided cases:

For TorsFreeAb: Extremal cogenerator / cogenerating set would be equivalent. We could conjecture that the family of localizations of Z might work. But if it does, I haven't found a simple proof. A sample case to illustrate the difficulties (constructed partially with the aid of AI): the subgroup of Q^2 generated by Z^2 and $(1/2^k, 3/2^k)$ for k=1,2,... Since the category is coregular, the extremal monomorphisms are regular monomorphisms; so we are looking for a saturated embedding of that group into a product of localizations. The map G -> Z[1/2] x Z[1/2] x Z, $(x,y) \mapsto (x, y, 3x-y)$, appears to work for that case, but has a twist required to get it to work. It's easy to imagine more complex examples requiring more and more complex twists, and maybe even a possibility of constructing a counterexample where "too many twists are required" to be able to build a valid map.

For FreeAb: Given the difficulties with infinite products, and that infinite-dimensional free abelian groups probably can't be cut out as regular subobjects of the product in Ab, it seems likely that Z won't work as an extremal cogenerator. In fact, it seems unlikely for any small set of free abelian groups (with limited cardinalities of generating sets) to work as an extremal cogenerating set. But I haven't been able to find a proof of either assertion.

For the various metric space categories with non-expansive maps as morphisms: R doesn't work as an extremal cogenerator, for example because it can't detect the failure of (0,1) -> [0,1] to be an isomorphism. That suggests that any extremal cogenerating set would probably have to contain lots of objects to detect various forms of failure to be complete, perhaps too many to form a set. I haven't succeeded in finding a proof along those lines, though (beyond vague ideas such as considering spaces formed by a pushout of $\kappa$ copies of R joined at a single point, and the inclusion of the space with that point removed).

Then there's still the question whether the category of combinatorial species has a single extremal cogenerator, which I still haven't quite managed to get a good grasp on.

[dschepler]

Looking at the proof I added that TorsFreeAb has $Q \times \prod_p Z_p$ as an extremal cogenerator, I wonder how many other proofs I could simplify by applying the same pattern: prove the canonical map to a product is in fact a regular monomorphism, using already established descriptions of products and regular monomorphisms (and dually for generators of course). For example, looking at the proofs in Ban, I can definitely see that strategy applying there.

If you want, I can look into this; or, we can merge this for now and I can create another PR within a couple days to make those simplifications.

[ScriptRaccoon]

I need some time to fully review the PR which I haven't done so far. My comments were only after skimming through it.

[ScriptRaccoon]

This is the first part of my review. I will have a look at the rest later.

[ScriptRaccoon]

To make this more similar to $\Delta$, cannot we say again that it is even an extremal generator in PreOrd and then use the fact that I have mentioned there?

[ScriptRaccoon]

Suggested change

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.

[ScriptRaccoon]

Thanks for adding this result!

Nit:

Suggested change

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.'

[ScriptRaccoon]

Notice that the assumption "right cancellative" should be "left cancellative". (Luckily, this doesn't make a difference since the implication is only applied to On.)

I also made some other improvements below.

- id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set
  assumptions:
    - locally finite
    - left cancellative
    - semi-strongly connected
    - extremal generating set
  conclusions:
    - essentially small
  proof: >-
    Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating set $S$. We then claim that
    $$\Ob(\C) \to \IN^S, \, X \mapsto (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.

[ScriptRaccoon]

A couple more comments.

[ScriptRaccoon]

Let's use the Yoneda Lemma instead.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

This is not correct. The object [0] is a generator, but not an extremal generator.

[dschepler]

By the way, I think I've found proofs that $(0, \infty)$ is an extremal cogenerator for Met; similarly $(0, \infty]$ is an extremal cogenerator for $\mathbf{Met}_\infty$; and $[0, \infty) \sqcup { 0' }$ is an extremal cogenerator for PMet. Is it OK for me to add these now, or should I wait until after the current review is done so you don't have a moving target?

[ScriptRaccoon]

Is it OK for me to add these now

Yes, in a new commit is fine!

[ScriptRaccoon]

Another chunk of comments. (not the final one, 11 files are left to review)

[ScriptRaccoon]

Suggested change

	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 \}$.

[ScriptRaccoon]

Remark: I like this new and even stronger proof that no extremal generating set exists much more than the previous one that no small dense subcategory exists (which referenced https://math.stackexchange.com/questions/4097315/).

[ScriptRaccoon]

Suggested change

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.

[ScriptRaccoon]

Suggested change

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.

It is easily checked that the indiscrete two-point space is a cogenerator, using that the two-element set is a cogenerator in $\Set$. 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. That is, $f$ is a homeomorphism.

The definition of the Sierpinski space doesn't need to be repeated since it is already used anyway in various places (even here in Top.yaml); in doubt we can add a link to Wikipedia.

Also, this is an interesting characterization of homeomorphism which most texts on general topology do not mention, right?

Here is the easy proof + generalization: Let $f : X \to Y$ be a surjective map which induces a surjection on open sets via pullback. Let $U \subseteq X$ be open. By assumption there is an open subset $V \subseteq Y$ with $U = f^*(V)$. Then $f_*(U) = f_*(f^*(V)) = V$, the last step uses that $f$ is surjective. Thus, $f$ is an open map.

[ScriptRaccoon]

I am not 100% sure if we should remove this (even if it is redundant), since this is a very instructive proof which many people should know. WDYT?

We can definitely remove it for pointed spaces since this is just a boring variation of the proof for spaces.

[ScriptRaccoon]

Let's add a reference to the extremal cogenerator in Set_*.

[ScriptRaccoon]

(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$)

This repeats the proof of a general lemma. Let's find this lemma and cite it. I can also look in Lee's book if you want.

[ScriptRaccoon]

Let's write $\psi(p) \coloneqq \frac{1}{1 - \phi(f(p))}$ in display math ($$).

[ScriptRaccoon]

This is the final chunk of comments. I have now checked all the files.

[ScriptRaccoon]

Suggested change

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)$.'

[ScriptRaccoon]

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.

Why?

[ScriptRaccoon]

To see this, let $\{y_i : i \in I\}$ be a set

In the following, you write x_i.

Also, it would be good to specify that this is a subset of $G$.

[ScriptRaccoon]

Please write down a precise definition of $\varphi$ and in particular why it is well-defined.

I would do something like: Let $G/p^n G \to Z/p^n$ be the coordinate projection at $i_0$. These are compatible in $n$ (since the basis has been chosen uniformly), hence yield a homomorphism $G \to \lim_n G/p^n G \to \lim_n Z/p^n = Z_p$.

[ScriptRaccoon]

Looking at the proof I added that TorsFreeAb has Q × ∏ p Z p as an extremal cogenerator, I wonder how many other proofs I could simplify by applying the same pattern: prove the canonical map to a product is in fact a regular monomorphism, using already established descriptions of products and regular monomorphisms (and dually for generators of course). For example, looking at the proofs in Ban, I can definitely see that strategy applying there.

After having read through the whole PR, I now understand what you mean here. Yes, this is a good idea, but this is a good opportunity for a follow-up PR. Let's try to finish and merge the current state first. There are always improvements we can make, for example also using the already mentioned dense subcategories.

[ScriptRaccoon]

I don't know why the e2e test for "user can open a proof for a deduced satisfied property of category" is failing. The code looks fine, and it also works locally. I reran the test on GitHub, but it gives the same error. For now, I think you can ignore this issue. I need to make the tests more reliable (also on my side they sometimes fail randomly for obscure reasons). If it keeps failing and it blocks us from merging, just uncomment the test case and I try to fix it after merging.

[dschepler]

Ah, right, I incorporated the suggestion to make explicit assignments of "Set has an extremal generator" for use in full subcategories, which would have broken the expected text (and even the expectation that it's testing a deduced satisfied property). I could switch that test back to testing the "generator" property, with the text that it's deduced from having an extremal generator.

[ScriptRaccoon]

Ah, right, I incorporated the suggestion to make explicit assignments of "Set has an extremal generator" for use in full subcategories, which would have broken the expected text (and even the expectation that it's testing a deduced satisfied property). I could switch that test back to testing the "generator" property, with the text that it's deduced from having an extremal generator.

Oups, even though I was on your branch with the latest changes, I forgot to update the database. Now it also fails.

Let us just replace the category by, say, Ring.

await page.goto('/category/Ring', { waitUntil: 'networkidle' })

The rest of the test 'user can open a proof for a deduced satisfied property of category' can stay as is.

By the way, did you check out pnpm e2e:ui already? This is such a cool feature 😎

[ScriptRaccoon]

Suggested change

	- 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.
	- 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