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: 7 unknown
extremal cogenerating set: 7 unknown

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