Enhancement: Compare properties

[derekelkins]

Given a two sets of adjectives, there could be a UI that shows which properties are true of only one or the other set. Here's an example.

If I choose "formally étale but not étale" and click Deduce, I see that such morphisms are not "locally of finite presentation". By comparing to "formally étale and étale", I can see that this differentiates formally étale morphisms from étale morphisms. However, both options would, e.g., be formally smooth.

In the UI I'm suggesting, comparing "formally étale but not étale" to "étale" would have two columns, one for "formally étale but not étale" and the other for "étale". In the first column would be morphism is not locally of finite presentation" and the second would have "morphism is locally of finite presentation". Neither column would have "morphism is formally smooth".

A bit more usable might be to be able to compare "formally étale" and "étale" and have it say something like "morphism is not necessarily locally of finite presentation" under the "formally étale" column and "morphism is necessarily locally of finite presentation" under the "étale" column.

The main use-case is probably understanding the difference between two concepts, e.g. why is a formally étale morphism not necessarily étale? It could also be used to see what needs to be checked to rule out a property. For example, if you have formally étale morphism that you think might be étale, this UI would give you a list of properties you could check to rule that out.

[jessetvogel]

@derekelkins Thank you for your suggestion! I spend some time yesterday building such a page, and this is what I found.

Let A and B be two adjectives (of the same type). Possibly it could be two sets of adjectives, but I do not have an idea of what the UI should look like to input such data. Then this comparison page could include:

• if A implies B, a proof
• if A not does imply B, examples of A which are not examples of B
• adjectives C which are implied by A but not by B
• (the same with A and B reversed, of course)

I think the first two are nice, but these use cases are already handled by the current 'Deduce' and 'Search'.

For the third use case, considering your example, I got quite a list of adjectives C which are implied by étale but not formally étale (locally of finite presentation, flat, unramified, G-unramified, smooth, syntomic, universally open, ...). Of course, the key difference is 'locally of finite presentation', but I found it hard to programmatically find a way to highlight this adjective / to distinguish it from e.g. universally open.

In this example, I think you can already find this key difference using the current interface: if you choose 'formally étale + not étale' and click 'Deduce', you indeed find 'not locally of finite presentation' including the reason: "étale is formally étale and locally of finite presentation". This theorem states precisely the difference between the two adjectives.

Let me know if you think I missed something.

[derekelkins]

Thank you for considering this. I did think it may not be obvious how to make a clear UI/UX for this. I think you're right that a better solution may be to make the proofs communicate the connections more.

For example, sticking with the "formally étale but not étale" example, let's say I'm wondering why a formally étale morphism isn't G-unramified. Right now, it just says "By the negation of definition G-unramified" and I have to navigate to the definition to see why and correlate it back with what was on the other page.

As an alternative, the definition could be inlined or appear in a pop-up when I hover over "definition G-unramified". In addition, the statements on the screen that (directly) support a morphism being G-unramified could have a green outline, while those that directly refute it have a red outline. In this case, the conclusion "morphism is not locally of finite presentation" would be outlined in red. If I then wondered why it wasn't locally of finite presentation, I could hover over its proof which would outline in the text above the table "formally étale" in green and "étale" in red.

Anyway, you can close this issue if you want. I may take a stab at a pull request doing what I just described in the next few weeks.