Frames

Stream: general

[Yaël Dillies]

I'm thinking of defining frames and inserting them between docs#complete_lattice and docs#complete_distrib_lattice. Does anybody see something wrong with that?

[Yaël Dillies]

Do we need the order dual notion to frames? A frame has an inf-distributive Sup, so do we need the things with a sup-distributive Inf?
Above, Johan is claiming that locales are dual to frames, but this seems in the category theory understanding of duality.

[Johan Commelin]

Yes, it's the opposite category

[Jireh Loreaux]

Just be aware that there is a completely different notion of frame; at least, I think it's different, but sometimes I am surprised by category theory. In the finite dimensional setting, a frame is just a spanning set, but in the infinite dimensional setting there is a distinction.

[Johan Commelin]

Yeah, I think that's a genuinely different notion. I don't know of a connection.

[Yaël Dillies]

And then there are also coframes, which I hoped were the order dual of frames.

[Yaël Dillies]

@Andrew Yang, what are your plans regarding this?

[Andrew Yang]

I don't really have the relevant knowledge and the plans to do more topos theory unless I need to.

[Yaël Dillies]

I didn't know I was stepping into topos theory :rofl: I just want to play with orders.

[Yaël Dillies]

One thing I foresee is that we will want complete Heyting algebras, which are just frames again, but this time with the implication operator on top. So the situation is analogous to docs#complete_semilattice_Sup vs dosc#complete_lattice. Do you think I should repeat the design decisions there or instead have only one class which contains the maximum amount of info and a constructor to build it for you when needed?

[Yaël Dillies]

This second option means we can't insert frames below docs#complete_distrib_lattice unless we add the redundant Heyting implication info there too. Actually, that might be a good idea.

[Wojciech Nawrocki]

Hi @Yaël Dillies , I just started looking into adding Heyting algebras. I was going to rebase #5527 but it looks like a lot has changed since then so maybe better to start from scratch. Do you think it would be best to add frames first and then follow up with Heyting PR which redefines frame? Also, what do you mean by "redundant" -- that the implication could be defined a posteriori using joins and whatnot but one may still want to squish it into the typeclass definition?

[Yaël Dillies]

Hey! I defined Heyting algebras today! I was opening the PR right now.

[Yaël Dillies]

I took yet a slightly different approach to #5527

[Yaël Dillies]

Also, #11709 defines frames.

[Yaël Dillies]

Sorry, it seems like I did everything you wanted to do.

[Wojciech Nawrocki]

No no this is great! Actually I would like to define some examples of Heyting algebras, in particular the opens of a topology and subpresheaves of a given presheaf. Maybe you have some of these already?

[Yaël Dillies]

So far, I have Prop :rofl:

[Yaël Dillies]

The opens of a topology should be very straightforward. I have basically no idea what the second one is.

[Yaël Dillies]

I am doing all this for the sake of order theory, so don't expect much topology from me, at least for now.

[Wojciech Nawrocki]

Awesome, I will wait for your PR.

[Yaël Dillies]

Running out of time today! Will PR tomorrow.