Add several negative properties of LRS_R deduced from those of Top

[dschepler]

Addresses: #227

[ScriptRaccoon]

Thanks a lot! I am glad that we can finally decide some of the properties of this category. It's also good to see that you could generalize your proof that previously only worked for special ground rings.

I have revised the content page, please check the three 3 commits that I added.

I still need to check the proofs in LRS_R.yaml. I will do this in the evening today.

[ScriptRaccoon]

I have some issues with this proof and the other ones (but no doubt that they are correct!). It is just said that "of the results here", but not making explicit which results are used for which claim. Also, I think that some of the proofs are even used. This suggests refactoring them.

Notice that for example the content page never mentions any functor from Top to LRS_R where R is a commutative ring which is not a field.

Maybe it is even better to add all these proofs to the content page itself. It can be a huge corollary like "The category LRS_R is (a) not X, (b) not Y, ... ".

Notice that this "outsourcing" has already been done for the cartesian closed property. The current approach is inconsistent.

Also consider adding stuff to the page cartesian-closed-results.md that I created for the more general results. Probably it then should also be renamed, since it is not about ccc anymore, but rather about coreflections. Then it can also be merged with subobject_classifiers_coreflection.md, and also with exact_filtered_colimits_descend.md.

In a later stage of this project, all of this will part of an extended deduction system where properties of categories can be deduced automatically from properties and results of (adjoint) functors. Namely, functor implications will then also have fields like target_conclusions and left_adjoint_assumptions.

[dschepler]

OK, I was thinking of the composition of the functor K : Top -> LRS_k and the forgetful functor LRS_k -> LRS_R. I suppose it would make sense to make that explicit.

I'm not clear on the exact reorganization that you're suggesting. Maybe something like subcategory_inheritance.md which is a catch-all for formal results like "if a subcategory of a regular category is finitely complete and has coequalizers, and the inclusion functor preserves finite limits and coequalizers and is conservative, then the subcategory is regular"? (Though for that particular one, I guess the result wouldn't necessarily need it to be a subcategory inclusion, or even faithful.)

If so, then it might make sense to make that reorganization into a separate PR. Though I guess I could certainly get a start with the general results needed for LRS_R.

Regarding the later stage: I suppose it would also need dependency tracking of the proofs to ensure we don't accidentally end up with circular arguments, right?

[ScriptRaccoon]

I was only referring to results about (co)reflective subcategories (not general subcategories) and which properties are inherited*. It doesn't need to be complete in any way, just gather the results we are currently using.

Separate PR: I can do this now where I combine subobject_classifiers_coreflection.md and exact_filtered_colimits_descend.md into, say, coreflective_subcategories.md. After merging this, you can rebase and add the results you need there.

Circular arguments will be prevented, yes, but this is simply done via primary keys in SQL (I think, I will check this more carefully of course). Unfortunately, circular arguments are potentially present already now because of all the "soft references" to other proofs. (Not only in CatDat, but in math as a whole.)

*EDIT: ok actually there is a result which is a bit more general, so yeah, it will be about subcategories in general

[ScriptRaccoon]

This what I meant: #237

[dschepler]

OK, that looks good.

Regarding the circular arguments: it does make sense that the automated deduction wouldn't create those. I guess what I was thinking there was along the lines of adding annotations to the "soft references" to make them into checkable references. (And the redundancy checker could then also take those into account.) So, something roughly along the lines of:

depends:
  - category: Top
    property: cartesian filtered colimits