!4#4593

Stream: PR reviews

[Sam van G]

Hello! I hope this is the correct place to post this - feel free to move somewhere else if needed.

Together with @Anne Baanen , @Leo Mayer , @Brendan Seamas Murphy , we started formalizing the beginning of my talk at Banff. I just made a PR of the adjunction between frames and topological spaces. We would very much appreciate comments. Some thoughts:

• A glitch that is probably not yet dealt with in the best possible way is the lemma elim_exists_prop (here)

lemma elim_exists_prop (A : Prop → Prop) : (∃ p, (A p) ∧ p) ↔ (A True) := by aesop

which is used one time in the file, but seems (to me) like it should be a general principle somewhere in the library.

• It was suggested at Banff that we could map to bool instead of Prop. I personally don't have a strong opinion about this either way.
• It is very likely that I made some Mathlib4-beginner-mistakes in preparing this pull request, please feel free to point them out.
• I did not find a file with precise Mathlib4-from-scratch-contribution-instructions yet (like this one for Mathlib3), I think?

Thanks!

[Sam van G]

Also tagging @Yaël Dillies who previously expressed interest in formalizing the math that this PR begins to address (this PR is only a small step in the larger project of formalizing Stone-Priestley duality)

[Yaël Dillies]

Cool! How far are you currently? I have Birkhoff duality on branch#stone_duality, although I haven't yet packaged it up as an equivalence of categories.

[Sam van G]

In the PR we only have the (contravariant) adjunction between frames and spaces. @Brendan Seamas Murphy has some more general work about restricting an adjunction to its fixpoints to get a category. We’re hoping to then use that to get the various dual equivalences, along the lines of what I outlined in my Banff slides. I think Birkhoff duality (for finite DLs and finite posets) will be the crucial non-abstract-nonsense component of that.

[Sam van G]

So it’s great that you’ve done that already!

[Yaël Dillies]

Ah great! I was afraid we'd stepped on each other's toes. My code is still in Lean 3, but hopefully it can be ported easily once someone has taught me oneshot.

[Johan Commelin]

@Yaël Dillies did you see the recently updated instructions in the README of https://github.com/leanprover-community/mathport ?

[Yaël Dillies]

Exams = no time :frowning:

[Sam van G]

@Yaël Dillies No rush. We can perhaps organize a call after your exams are over to see how to sync. Best of luck with the exams!

[Sam van G]

Hi! I am hoping to revive and finish this PR #4593, on the adjunction between Top and Locales, that we started in June during Banff (and that I subsequently procrastinated on finishing, sorry...!)
I finally had time to look at @Yaël Dillies work on this. Thank you so much, I learned a lot from your golfing.
Yaël wrote in the Github discussion that

I haven't fixed the names. They are currently

1. Not capitalised properly
2. Dumped in the root namespace
   Not sure which way to fix them, so please offer suggestions!

I am not so familiar with the current requirements for merging into Mathlib4 so I am hoping I can ask for some help here. Apologies for the probably naive questions:

• Re (1), I'm not sure either what would be the correct capitalisation, how can I find out?
• Re (2), does this just mean I should encapsulate everything in a namespace?
• There is also a comment (l. 61) -- TODO: Merging those variable breaks , but I'm not sure what it means, or how to fix it.
• Finally, I also noticed a message "leanprover-community-mathlib4-bot added the merge-conflict label 3 weeks ago"... what can I do about that?
  Thanks!

[Dagur Asgeirsson]

Regarding your last point: the merge-conflict label means that there is a merge conflict with the current master. You need to merge master into your branch and resolve the conflicts manually to get rid of the label

[Jireh Loreaux]

Sam, see #naming for guidelines on naming conventions.

[Jireh Loreaux]

Another quick note: after glancing at the PR, I notice there's a bunch of stuff going on with coercions (e.g., in Order.Hom.Lattice), including cleaning up porting notes, that can easily be split off into a separate PR. That should be merged quickly and will make this one shorter and easier to review.

[Jireh Loreaux]

As for a namespace, I think something like CategoryTheory.Locale might make sense, but I'm not terribly familiar with the category theory end of the library, so maybe that doesn't quite match conventions there

[Sam van G]

Jireh Loreaux said:

Another quick note: after glancing at the PR, I notice there's a bunch of stuff going on with coercions (e.g., in Order.Hom.Lattice), including cleaning up porting notes, that can easily be split off into a separate PR. That should be merged quickly and will make this one shorter and easier to review.

I have tried to do this as a new PR #7796. I hope this is what you were after -- let me know if it looks OK or if anything needs to be changed there.

[Sam van G]

Jireh Loreaux said:

As for a namespace, I think something like CategoryTheory.Locale might make sense, but I'm not terribly familiar with the category theory end of the library, so maybe that doesn't quite match conventions there

I have attempted to fix the naming conventions and namespaces in #4593, the commit is here. If someone could have a look and tell me if this now indeed looks right, that would be helpful, as I wasn't 100% sure in all cases.

[Sam van G]

The split-off PR #7796 was just merged (thanks for being so fast, @Eric Wieser and @Oliver Nash).

[Sam van G]

I believe #4593 (which contains the new file FrameTopAdjunction) should be in good shape now too (I also fixed the "variable" problem mentioned above). Would someone be willing to give it a look to check it's all in order with naming conventions etc?

[Oliver Nash]

I have a busy morning but I'll take a look this afternoon if nobody else has reviewed it by then. Glancing now, it looks great, though I do see a lot of defs with no API [this might be fine].

[Eric Wieser]

I think a handful of the functions in that PR should be lowerCamel rather than UpperCamel case, but I'll leave that for someone else to review

[Sam van G]

Eric Wieser said:

I think a handful of the functions in that PR should be lowerCamel rather than UpperCamel case, but I'll leave that for someone else to review

me too.. Thanks for having a look

[Sam van G]

Oliver Nash said:

I have a busy morning but I'll take a look this afternoon if nobody else has reviewed it by then. Glancing now, it looks great, though I do see a lot of defs with no API [this might be fine].

Thanks Oliver. No rush at all.
Regarding your comment about defs, I was just able to remove three of these defs by inlining them instead (getting the def count down from 12 to 9).
When I try to remove more defs, I get in trouble with things that are no longer inferred.
For example, the unitCounit def on l. 118 seems silly since it looks like it is just a pair, but when I try to inline it in l. 123, Lean complains that there are two missing fields (the triangle equalities), and adding by infer_instance won't solve it.
Similar problems for the def Counit and def Unit.
I don't know how important it is to remove defs, I leave it for you to judge when you get around to reviewing it.

[Sam van G]

Thanks for your comment about elim_exists_prop, @Eric Wieser . It helped me realize that I could get rid of it by giving an existing lemma Prop.exists_iff to two simps in my main file.