Add total/cototal category properties

[dschepler]

Unknown categories decided for "total" property:
category of Z-functors

Unknown categories for "cototal" property:
category of commutative monoids
category of locally ringed spaces
category of Z-functors

[dschepler]

I have some rough ideas on some of the others: on Hausdorff spaces and semigroups, I think I should be able to use an idea similar to the one for Cat to keep control over the images of constant maps. For CMon, I think the "subdirectly irreducible" property might have to do with limiting the number of maps to it - though I'm not yet at all sure how to translate that into a contradiction. And on locally ringed spaces, I have a vague idea that I might be able to define a functor whose L(T) would have a number of maps from Spec k which grows faster than possible for any single locally ringed space.

Anyway, no rush on reviewing this - I was just working on this off and on over the past week, and wanted to get the progress so far pushed before resuming work on the quasitopos PR.

[ScriptRaccoon]

It would be cool if we can merge this soon. The few remaining cases don't have to be dealt with at this moment.

[dschepler]

OK, what does have to be resolved before we can merge it: There are several places where references are missing or incomplete. And the current proof that total -> complete needs to be finished, or replaced with a reference if for some reason finishing off the proof that the construction does give a limit is too complex.

[ScriptRaccoon]

OK, what does have to be resolved before we can merge it: There are several places where references are missing or incomplete. And the current proof that total -> complete needs to be finished, or replaced with a reference if for some reason finishing off the proof that the construction does give a limit is too complex.

Oups I forgot that the proofs are incomplete.

[dschepler]

@ScriptRaccoon I think this PR is ready for review now.

[ScriptRaccoon]

@ScriptRaccoon I think this PR is ready for review now.

Great! I will have a look in the next days.

[ScriptRaccoon]

Since #319 is now merged, can you also add the proof references that have been added here? For example, the proof for SemiGrp refers to the proof for Cat.

[ScriptRaccoon]

@dschepler Can you give me an update here? Do you plan to continue this PR at some point? If you prefer, I can also try to finish it (based on the comments I gave).

[dschepler]

@dschepler Can you give me an update here? Do you plan to continue this PR at some point? If you prefer, I can also try to finish it (based on the comments I gave).

I've been taking a bit of a break from the project.

Though unfortunately, I had gotten stuck on most of the significant comments that were left to address:

• I wasn't having much luck trying to come up with a good generalization of the lemma on certain large collections of simple objects precluding being total to the case of Ring. (And I couldn't come up with a good argument relating it to Rng, since as far as I recall, the natural reflector is in the wrong direction.)
• I was having trouble trying to put in the clarification that we were using the implication of hypercompleteness in several of the negative proofs, without making it too much of a distraction or too verbose. (Of course, if we implement Add some other properties related to "total" (and their duals) #308 then that becomes less of an issue; but this PR is already large enough without adding that in. And I guess implementing Add some other properties related to "total" (and their duals) #308 could also be an eventual clarification to some of the proofs such as Cat and Haus - as far as I know, being total isn't necessarily inherited by slice or coslice categories; but on the other hand, it seems clear that hypercompleteness should be inherited.)

So, even if I returned to this, I'm not sure I could resolve much more than marking the new dependencies. If you had clearer ideas on what you wanted to see as resolutions for those comments, feel free either to finish off this PR yourself as you suggested, or to post clarifications and I can try to get back to this and finish it off.

[ScriptRaccoon]

I see. Please don't let the wish to make everything perfect block you or hold up this PR. If my comments have given you that impression, I'm sorry. They are always meant merely as suggestions for directions we could take, not as requirements for this PR. If something is not feasible right now, that's perfectly fine. A TODO comment in the code is enough to flag it for later.

Specifically, for the first bullet point, I don't think we necessarily need a general lemma. As long as we understand how the proofs work in each relevant example, that is sufficient for now. A general lemma would be nice to have, but it is by no means necessary to finish this PR.

As for the second bullet point, the proofs can become distracting or verbose, as you say, if we leave TODO comments to remind ourselves to refactor them once the related properties are added. But if we already have the proofs, let's just write them down. They don't have to be perfect. (And honestly, no proof is ever perfect.)

[dschepler]

All right, I think I've taken care of most issues as far as I can, except that I'm still working on making the CAlg(R) proof self-contained instead of expecting the reader to "apply the patches to the lemma".

[ScriptRaccoon]

All right, I think I've taken care of most issues

Great!

except that I'm still working on making the CAlg(R) proof self-contained

Let me know when you think this is done (or if it should be postponed, which is also OK, just leave a TODO comment).

Then I will have another look at the PR and merge it.

[dschepler]

That last step should be done now. It should hopefully be ready for review, and then it will just need a rebase (probably by hand) before it can be merged.

[ScriptRaccoon]

Alright. I have some more minor adjustments and fixes. Please have a look. (Unfortunately the diff on GitHub is not very helpful.)

Can you try to rebase? I think we should only have a handful of commits in the end. Such as:

• add properties total and cototal (including Grp_total_explicit_proof.md)
• results on total categories
• decide total and cototal for various categories

[dschepler]

Alright. I have some more minor adjustments and fixes. Please have a look. (Unfortunately the diff on GitHub is not very helpful.)

Looked good to me.

Can you try to rebase? I think we should only have a handful of commits in the end. Such as: ...

That's done now.

[ScriptRaccoon]

Great! Thanks a lot for your work on this PR.