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.

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

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

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

[dschepler]

I think I've now addressed all the comments, except for a couple which need more input.